Lcertify translation validator: A Library for Certification
of Compilation
Principle
Static analysis techniques and analysis tools (such as
Astrée)
for the certification of safety critical softwares
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).
Related projects
- Translation validation approach:
- Compiler verification approach:
Related publications