Certificate Translator Prototype
Certificate translation is a method that transforms certificates of source programs into certificates of their compilation. It provides
strong guarantees on low-level code, and is useful for eliminating trust
in the compiler (for high assurance code) and in the code producer for
mobile code security. The theory of certificate translation has been developed in earlier work, but no implementation exists. As a result, it has
been difficult to evaluate its practicality, and in particular the impact of
certificate translation on the size of certificates.
The tool takes as input a high-level program, defined in a
small subset of the C programming language, and a logical specification
a la ACSL, and computes a set of verification conditions for the Coq proof
assistant. Once proof obligations are discharged, the tool compiles the
source program into an intermediate RTL (i.e., three-address code) representation, and then performs a sequence of compiler optimizations. At
each step, certificates are transformed automatically to produce a proof
for the transformed programs. For optimizations that rely on arithmetic
reasoning, such as constant propagation and common subexpression, the
tool implements a new certificate translation strategy that minimizes
certificate growth.
Download it: