Description of the project
Computer software pervades our life but far too much of it contains programming errors (bugs). Software is more and more complex and such errors are unavoidable if programmers are not accompanied with some tools that help auditing software codes. Static analysis is an increasingly popular technique that aims at automatically compute properties of software. These properties then help finding bugs, or proving absence of them. Industrial static analysers are flourishing. Facebook, Google, Microsoft develop their own static analysis tools to help maintaining their huge code base. Critical software industry (aircraft, railways, nuclear, etc.) has embraced the use of advanced static analysis tool as Astree to companion and sometimes, ligthen their traditional software validation campaigns based on meticulous testing and reviews. Unfortunately, designing advanced static analyses like Astree requires a very rare expertise in Abstract Interpretation, a foundational landmark in the research area, and implementing these ideas efficiently and correctly is specially tricky.
The VESTA project will propose guidance and tool-support to the designers of static analysis, in order to build advanced but reliable static analysis tools. We focus on analyzing low-level softwares written in C, leveraging on the CompCert verified compiler. This compiler toolchain is fully verified in the Coq proof assistant.
Verasco is a verified static analyser that I have architected. It analyses C programs and follows many of the advanced abstract interpretation technique developped for Astree, but it is formally verified. The outcome of the VESTA project will be a platform that help designing other verified advanced abstract interpreters like Verasco, without starting from a white page. We will apply this technique to develop security analyses for C programs. The platform will be open-source and will help the adoption of abstract interpretation techniques.
Publications
- Lucas Franceschino, David Pichardie, Jean-Pierre Talpin: Verified Functional Programming of an Abstract Interpreter. SAS 2021: 124-143 (2021).
- Gilles Barthe, Sandrine Blazy, Remi Hutin, David Pichardie: Secure Compilation of Constant-Resource Programs. Proc. of CSF 2021: 1-12 (2021).
- Aurele Barriere, Sandrine Blazy, Olivier Fluckiger, David Pichardie, Jan Vitek: Formally verified speculation and deoptimization in a JIT compiler. Proc. ACM Program. Lang. 5(POPL): 1-26 (2021)
- Gilles Barthe, Sandrine Blazy, Benjamin Gregoire, Remi Hutin, Vincent Laporte, David Pichardie, Alix Trieu: Formal verification of a constant-time preserving C compiler. Proc. ACM Program. Lang. 4(POPL): 7:1-7:30 (2020)
- Jean-Christophe Lechenet, Sandrine Blazy, David Pichardie: A Fast Verified Liveness Analysis in SSA Form. Proc. of IJCAR 2020: 324-340
- Sandrine Blazy, David Pichardie, Alix Trieu: Verifying constant-time implementations by abstract interpretation. In J. Comput. Secur. 27(1): 137-163 (2019)