Logics for Low-Level Code and Proof-Preserving Program Transformations
Ando Saabas · 2008
The Proof-Carrying Code (PCC) paradigm has emerged as a way of instilling trust in the code user about the properties of the code that she is about to run. The underlying idea is simple: code is shipped with a proof which attests that it adheres to the requirements set at the user’s computer. Consequently, the user does not need to check the code itself, only its proof, which is a simple, fast and one-time procedure. A program proof can be thought of as a semantic checksum, attesting that the semantics of the program has not been tampered with. While the underlying idea of Proof-Carrying Code is simple, it offers many challenges in both scientific and engineering aspects. This thesis concentrates on two aspects relevant for Proof-Carrying Code. First of all, we describe a way of giving a compositional semantics and matching Hoare logic to low-level, “unstructured” languages with jumps. Our work is based on the insight that a phrase structure can be given to the seemingly non-modular code by defining the code to be either a single instruction, or a finite union of pieces of code. We show that this seemingly trivial phrase structure actually provides a convenient basis for compositional semantics and logic. The semantic and logic descriptions that we thus obtain are similar in sophistication to those of the standard While language. Notably, Hoare triples in our logic can be interpreted in the usual way. The second aspect we investigate concerns “proof compilation”: the problem of translating a program proof alongside the program in the context of compilation. While the problem is trivial in the case of a non-optimizing compiler, it becomes complicated when optimizations take place: a valid proof of a program is in general not valid for the optimized, semantically equivalent version of the same program. We propose a way of describing optimizations via type systems, where the type system specifies both the dataflow analysis underlying the optimization and the rewrite rules making use of the analysis information and carrying out the optimization. The type derivation of a program is then used to guide the transformation of the proof. We demonstrate that this approach works both for high-level programs and Hoare proofs and on control flow graph based program descriptions and flat, unstructured program proofs. We are able to address complicated, program structure changing optimizations such as partial redundancy elimination and also optimizations based on bidirectional analysis.