LCERTIFY translation validator: A Library for Certification of Compilation
Static analysis techniques and analysis tools (such as Astrée) for the certification of safety critical software target the source code. However, if the compiler is not correct, this source level certification is not sound anymore. Thus, field specific regulations such as DO-178-B in avionics recommend target code be considered instead.
Alternatively, it is also possible to certify the compilation itself. There are several approaches to do that, in particular:
- Translation validation : it consists in certifying each run of a compiler, using an automatic tool, that will prove that the source and the target code are semantically equivalent.
- Formal compiler verification : it consists in proving formally the compiler correct once and for all, so that each time the compiler is used, the result can be trusted.
The Lcertify project investigates translation validation techniques, in the case of imperative language like C or user-specific languages with similar traits. The tool inputs a source program and a binary (Power-PC, Elf with 32-bits format, conforming to the Embedded ABI), performs an automatic computation that may produce two results:
- Success of the translation validation, meaning the source and the binary are semantically equivalent.
- Failure of the translation validation, meaning the proof of semantical equivalence could not be completed ; as the problem is undecidable, this result does not mean the compilation was incorrect
Rather than a monolithic tool, it consists in a library-like system, which can be interfaced with various source front-ends (the same could be done for the binary front-end). Two front-ends were developped: a C front-end (conforming ANSI C), and a pseudo-code front-end, dedicated to a language used at Airbus (that development was part of the AsBaProd project).
- Translation validation approach:
- Validation project, at New York University
- Compiler verification approach:
- Symbolic Transfer Functions-based Approaches to Certified Compilation. Xavier Rival. In 31st Symposium on Principles of Programming Languages (POPL'2004), Venice, Jan. 2004 ACM. [.pdf]
- Traces Abstractions in Static Analysis and Program Transformations. Xavier Rival. PhD Thesis. [.pdf].