This layer has evolved over forty years, continuously adjusting to the novel architectures and high-level programming language features. As it stands today, several of its aspects are poorly specified, and in extreme cases the sole documentation consists in the source code of the relevant libraries. This layer is pervaded by subtle bugs; most of the time these are unobservable only because redundant strategies to recover correct informations have been baked over the years into libraries and tools to circumvent the problems.
We propose to investigate some aspects of this complex interface and to develop tools to make programming more robust and better-understood.
Validation and Synthesis of DWARF Debugging Informations
Sorry, but last time was too f***ing painful. The whole
(and *only*) point of unwinders is to make debugging easy when a bug
occurs. But the f***ing dwarf unwinder had bugs itself, or our dwarf
information had bugs, and in either case it actually turned several
"trivial" bugs into a total undebuggable hell.
Linus Torvalds, Linux Kernel Mailing List, Oct. 2012 DWARF is a standardised debugging data format; it is part of the ELF and Mach-O binary formats, and as such it is widely used. DWARF is obviously relied upon by debuggers, but it plays an unexpected role in the runtime of high-level programming languages and in the implementation of program analysis tools. For instance the C++ runtime relies on DWARF's .debug_frame table to unwind the stack and implement C++ exceptions, while program analysis tools require the .debug_types table to reconstruct the initial state of a program from its binary. Generating the DWARF tables tends to be a burden for compiler authors, as each optimisation pass potentially invalidates several of them; keeping tables and code synchronised pass after pass requires a tedious and error prone logic to be added to the already twisty optimiser passes. In practice there are bugs in the generated tables: these hard to detect because DWARF informations never get any rigorous testing. A more insidious problem is due to the fact that DWARF tables include scripts expressed in a Turing complete bytecode: it has been shown that a malicious attacker, by injecting crafted DWARF tables in a binary, can create powerful and unsuspecting trojans. A first project is to develop a tool to cross-check binaries against their DWARF tables. The tool will thus validate the Dwarf informations, identifying all the hard-to-detected bugs in generated tables, and preventing DWARF injection attacks. The .debug_frame stack description tables are the ideal starting point: they are redundant with respect to the binary instructions and do not depend on source code semantics. Developing techniques to validate the .debug_line (correspondence of assembly instruction and source code), and .debug_info (type and layout informations, storage of local variables) tables can constitue a second project. This is challenging as it requires to establish a simulation relationships between the machine program and source program, mapping C sequence points to program counter values. Many important compilers (including HotSpot from OpenJDK, but until recently also Haskell and OCaml) do not generate DWARF tables at all. This annoying omission prevents debugging and program analysis with standard tools. However, if we can cross-check DWARF tables against instructions as in the previous task, then with similar techniques we can synthesise DWARF tables from instructions. A third project would aim to develop theories and tools to recover most, or all, DWARF information by reverse engineering a binary. Each of these projects has the potential to be routinely used to validate software and compilers and make an impact in the real world: Linus Torvalds would not complain about DWARF anymore! |
|
Last update:
|