Tools that simply detect vulnerabilities in source code cannot ensure that there are no vulnerabilities in the code at all. This requires a different approach.
Frama-C, CEA-List’s formal verification tool, addresses this challenge by using mathematical proof to automatically verify the absence of a broad class of vulnerabilities like buffer overflows, which, due to insufficient precautions during programming, allow the amount of data to exceed the memory’s storage capacity. This kind of verification does come at a cost. However, it is much better to do it early in the development cycle when any vulnerabilities introduced into the code are still easy to correct. And, if developers are aware of the demands of early and automated formal verification, they can adapt their programming style accordingly—an added benefit. Ideally, Frama-C is used as part of a continuous integration process, a development practice in which code is tested and validated with each modification, right from the start of the project. However, for Frama-C to be effective in this context, its analysis time must be similar to the interval between two code modifications.
We introduced incremental analysis techniques into Frama-C to meet this requirement. Instead of redoing a full analysis after each code modification, the previous analysis is reused as much as possible to speed up the next analysis. The major challenge is to formally prove that the reuse of previous analysis results doesn’t compromise the correction of any vulnerabilities. In short, the incremental analysis must be as reliable as the full analysis.
We used two techniques to achieve this.
The first technique involves reusing code function summaries, which correspond to mathematical properties deduced from each function, produced by the first analysis. By comparing code versions and exploring their structure, we can determine which summaries can be reused for the new analysis of a function.
The second technique speeds up the search for loop invariants (logical properties of the code). Invariants discovered during a previous analysis are reused as starting points so that invariants can be found more quickly in the new version of the code. Initial experiments on open-source code with a public modification history showed that incremental code analysis with Frama-C reduces analysis time by a factor of 1.5x to 28x, with an average improvement of 7.83x. The experiments also revealed very little variation in the analysis results, with no negative impact on reliability. These techniques are, therefore, compatible with implementation in continuous integration workflows.
When used early in software development, Frama-C enables vulnerabilities to be detected while they are still easy to correct.
This research, conducted in partnership with Sorbonne University as part of the SecurEval project, part of the national PEPR Cybersecurity program funded by France 2030, resulted in one publication :