Design and Implementation of a Certifying Compiler for Type-Based Annotation

The certifying compiler for type-based annotation, which is a key component of the safety infrastructure, can translate programs, written in a type safe subset of the C programming language, into highly optimized Intel x86/linux assembly language programs, and also can produce the assembly language programs with annotation based on type-safety policy. The experiment shows that: ① it is reliable to translate a type-safe subset of C programming language into annotated Intel x86 assembly language; ② the certifying compiler is freely able to apply many standard local optimizations; and ③ it can signal a fatal error for the run-time array bound checking. Since the proof system of the safety policy is based on the annotated target code, the certifying compiler thus may be useful in a system for safe mobile code.