Scalable certification for typed assembly language

1 Background A certifying compiler takes high-level source code and produces target code with a certificate that ensures that the target code respects a desired safety or security policy. To date, certifying compilers have primarily concentrated on producing certificates of type safety. For example, Sun's javac compiler maps Java source code to statically typed Java Virtual Machine Language (JVML) code. The JVML code includes type annotations that a verifier based on dataflow analysis can use to ensure that the code is type-safe