Mastering the code used in a system
How would you present DECODER?
The DECODER project aims at providing powerful tools for developers to get thorough understanding of a given piece of software. This is crucial when attempting to reuse legacy code and/or integrate third-party libraries, for which the official documentation might not provide sufficient and up-to-date details to ensure that it will behave as expected by the developer.
More specifically, DECODER seeks to provide a database storing any kind of code-related artifacts (source code, formal specifications, comments, semi-formal models, documentation, forum discussions, issue tracker items,...), as well as establish bindings between them, notably by generating formal specification from informal requirements or semi-formal models from source code. Additionally, several industrial use-cases will assess the capabilities of the DECODER toolset to cope with real-life examples.
What is your role in the project?
Since we intend to tackle many different aspects of software development and verification, DECODER gathers partners with pretty different backgrounds. As technical leader, my role is to ensure, along with the project coordinator, that we all share the same vision of the project and that the tools we build work smoothly together.
Furthermore, as a developer of the Frama-C software verification platform, I'll investigate how it can benefit from information gathered by other tools, notably through generation of formal specifications, and how its results can help refining the information known about the software under analysis. This will mainly take place in WP1 (Persistent Knowledge Monitor) and WP3 (Activities for the Reviewer) and in addition use results from WP2 (Activities for the Developer) while providing inputs for WP4 (Activities for Maintainer). As with all tool developing activities in DECODER, we will work together with WP5 (Methodology) and WP6 (Use-cases) and use their feedback to guide our developments.
What key innovation do you bring or help to develop?
Due to the growing size and complexity of software, mastering the code used in a system is nowadays an extremely complicated task. This is a major issue, as improper usage of a third-party function can quickly lead to severe safety or cyber-security issues. Formal verification can provide very strong guarantees on the software under analysis, but usually requires an important effort from the user, in particular in the form of a formal specification of what each function is supposed to do and what are the appropriate states in which it can be called. This is a huge barrier to the wider adoption of formal methods beyond the most critical domains (e.g. aeronautics industry). DECODER will greatly help developers in these formal specification tasks, making it much easier to use these tools, thus enhancing the robustness of software systems.
A word about yourself and your organization
I have been working since more than 10 years in the Software Safety and Security Lab (LSL) at List, an institute of CEA Tech based in the Saclay area, about 20km south of Paris. The team develops tools and methods to verify safety and security properties on software, with a strong emphasis on formal methods. The three main tools of the lab are:
- Unisim, a simulator for many embedded hardware chips, allowing a very precise inspection of the behavior of a program on a given platform
- BinSec, a tool for analyzing binary code
- Frama-C, a tool for analyzing C source code
I'm one of the core developers of Frama-C, involved in particular in the kernel of the platform and extensions to handle higher-level properties than the ACSL specification language understood natively by Frama-C, which is very close to the code and not suitable for expressing more abstract requirements.
From the LSL point of view, DECODER concerns the Frama-C tool. Our overall goal is to integrate Frama-C into the DECODER environment in order to let our users take advantage of new, advanced ways for expressing the properties they want to verify with Frama-C on their code.
Virgile Prevosto holds an Engineering degree from École Polytechnique and a PhD in CS from Université Paris 6. After a post-doc at Max-Planck Institute for Informatics in Saarbrücken and a stay at Inria Rocquencourt, he joined CEA List in 2006, and has been since then a core developer of the Frama-C platform and acted as CEA's principal investigator for various collaborative projects, including the coordination of the French-German DEVICE-Soft and ANR U3CAT projects.