CCMini: a prototype of certifying compiler based on annotated abstract syntax trees

Abstract

Certifying compilers use static information of a program to verify that it complies with certain security properties and to generate certified code. To do so, those compilers translate the source program into an annotated program written in some intermediate language. These annotations are used to verify the generated code. Given a source program, a certifying compiler will produce object code, annotations, and a proof that the code comply with the customer’s security specifications. Thus, certifying compilers can automatically produce the security evidence required to establish a Proof-Carrying Code (PCC) setting. In this work we present CCMini, a certifying compiler for a simple subset of the language C. This compiler guarantees that compiled programs do not read uninitialized variables and do not access to undefined array positions. The verification process is carried on abstract syntactic trees by using static analysis techniques; in particular, control analysis and data analysis are used.