Last modified: Wed Nov 25 05:59:27 2015 GMT.
A certifying compiler generates not only the code but also a proof that the code obeys a security policy. Therefore, one need not trust the correctness of a compiler generating certified code, instead one can verify the correctness of the generated code. This allows a code consumer to accept code from untrusted sources which is specially advantageous in a networked environment. In practice, most certifying compilers use a type system for generating and encoding the proofs. These systems are called type-based certifying compilers.
This dissertation describes a type system that can be used for supporting runtime type analysis in type-based certifying compilers. The type system has two novel features.
First, type analysis can be applied to the type of any runtime value. In particular quantified types such as polymorphic and existential types can also be analyzed, yet type-checking remains decidable. This allows the system to be used for applications such as a copying garbage collector. Type analysis plays the key role in formalizing the contract between the mutator and the collector.
Second, the system integrates runtime type analysis with the explicit representation of proofs and propositions. Essentially, it integrates an entire proof language into the type system for a compiler intermediate language. Existing certifying compilers have focussed only on simple memory and control-flow safety. This system can be used for certifying more advanced properties while still retaining decidable type-checking.