Description
When proving that programs adhere to various safety and security properties, it is often useful to work with binary code instead of the high-level source code from which it was compiled. Proving safety for binary code means that we need not trust the compiler and that end users can check the safety property without access to the source code. But most of today's safety tools operate only on source code, where analysis and program transformation are easier. We need a way to take safety results that have been established for source code and propagate them to the binary level. This dissertation proposes such a system for certified assembly code, and shows how it can be used with three source-code safety tools that operate on existing C programs: CCured, Deputy, and Cqual.
A key feature of this system is a novel dependent type system suitable for assembly code. It is difficult to use dependent types safely in languages where heap values can be modified, because modifying a value can change the type of some other memory location. We address this problem by limiting in-memory dependent types so that they only refer to other fields of the same object. We show that it is possible to safely update such an object by allowing memory to temporarily be in a "bad" state until enough fields have been written so that the object is again internally consistent. And we show examples from CCured and Deputy where such a type system is necessary.
The second key contribution of this dissertation is a type inference system for assembly code that has been generated by a "black box" compiler. This algorithm discovers the (possibly dependent) types of registers at each program point, and therefore reconstructs the invariants that were shown to hold during source-code verification. We use abstract interpretation of symbolic expressions for this inference, and discuss how to deal with pointer arithmetic.
Finally, we have an implementation of our verifier for CCured and Cqual. This verifier parses x86 assembly code generated by GCC and ensures that the program was correctly analyzed and instrumented by CCured or Cqual prior to being compiled, and that the object code has not been tampered with in a way that would affect type safety. We present experimental results for our verifier which show that verification can be done in an efficient manner, but certain C constructs such as complicated array index expressions are difficult to analyze.