Debugging Debug Information - Francesco Zappa Nardelli
Workshop on Software Correctness and Reliability 2017
The spectacular results achieved by computer science in the recent years rely on hidden, obscure, and badly specified components that lurk at the very heart of our computing infrastructure. Consider debugging informations. Debugging informations are obviously relied upon by debuggers and play a key role in the in the implementation of program analysis tools, but, more surprisingly, debugging informations can be relied upon by the runtime of high-level programming languages (e.g. to unwind the stack and implement C++ exceptions). Unfortunately debugging informations themselves can be pervaded by subtle bugs. Linus Torvalds wrote around 2012:
"The whole (and only) point of unwinders is to make debugging easy when a bug occurs. But the *** DWARF unwinder had bugs itself, or our DWARF information had bugs, and in either case it actually turned several trivia bugs into a total undebuggable hell...If you can mathematically prove that the unwinder is correct -- even in the presence of bogus and actively incorrect unwinding information -- and never ever follows a bad pointer, I'll reconsider.''
I will describe an approach and a tool to perform validation and synthesis of the DWARF stack unwinding debug tables, hoping to make Linus Torvalds reconsider. I will also report on possible approaches to validate the whole of DWARF informations, a far more ambitious plan.