The collaborative CEEC project aims to produce a new software development methodology to accelerate the certification of products that require very high levels of security.
During this project, the partners intend to create a new software development environment, based on Prove & Run innovative technology, that will include a fully-proven generation and compilation toolchain. By integrating security concerns within the development process of critical systems, this environment will enable the creation of quality software with guaranteed security properties and will reduce the cost of high-level evaluation and certification, such as those that follow the Common Criteria methodology.
Technological and Scientific Innovations
The goal of this project is to enable the following workflow and to validate that it does reduces the Time-to-market of sensitive software components:
- The conception language designed by Prove & Run enables developers to specify the actual behavior of a program, but also the security properties it must respect,
- The development environment designed by Prove & Run can formally verify such a program and translate it into C source code,
- Thanks to CompCert – a formally-verified C compiler that will be upgraded to target ARM platforms – this source code is compiled into a trustworthy executable binary,
- Connections between the Prove & Run IDE and the Esterel Technologies environment allow the security concerns of the avionics domain to be taken into account at the model level,
- At every step of this transformation process, this toolchain generates the evidence required by the Common Criteria methodology for high evaluation levels.
In order to demonstrate its flexibility, the tool chain supporting this new methodology will be applied to two representative examples drawn from the following environments:
- Trusted execution environments for smartphones,
- Commercial avionics.
The results of this project will be disseminated through conferences and other means of communication.