A Type System For Certified Runtime Type Analysis

Abstract : Modern programming paradigms are increasingly giving rise to applications that require type information at runtime. For example, services like garbage collection, marshalling, and serialization need to analyze type information at runtime. When compiling code which uses runtime type inspections, most existing compilers use untyped intermediate languages and discard type information at an early stage. Unfortunately, such an approach is incompatible with type-based certifying compilation. 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 focused only on simple memory and control-flow safety.