Parallel Abstract Interpretation

Institution

The French Alternative Energies and Atomic Energy Commission (CEA) is a key player in research, development, and innovation. Drawing on the widely acknowledged expertise gained by its 16,000 staff spanned over 9 research centers with a budget of 4.1 billion Euros, CEA actively participates in more than 400 European collaborative projects with a large number of academic (notably as a member of Paris-Saclay University) and industrial partners. Within the CEA Technological Research Division, the CEA List institute addresses the challenges coming from smart digital systems.

Among other activities, CEA List’s Software Safety and Security Laboratory (LSL) research teams design and implement automated analysis in order to make software systems more trustworthy, to exhaustively detect their vulnerabilities, to guarantee conformity to their specifications, and to accelerate their certification. In particular, the Frama-C platform is dedicated to perform a wide range of analyses over C programs (with an experimental C++ front-end).

Scientific context

As software becomes increasingly prevalent in critical applications, concerns about safety and security are growing in importance. To address this concern, formal methods offer a mathematical framework for applying logical reasoning to programs, enabling rigorous proofs of their correctness and the absence of flaws. Among these methods, Abstract Interpretation (Wilhelm 2022) stands out as a theory well-suited for fast and automated program verification.

Eva (Bühler, Maroneze, and Perrelle 2024) is a Frama-C plugin based on Abstract Interpretation dedicated to the automatic inference of properties about C programs, such as finding all the possible values of variables or inferring arithmetic relations between variables. The primary goal of this analysis is to prove the absence of runtime execution errors (e.g. arithmetic overflows, invalid memory accesses, and other C undefined behaviors) that could be used by an attacker or cause safety issues. It is also used for code auditing and as a support for other analyses.

While abstract interpretation is among the fastest sound approaches to program verification, the analysis of complex software can take several hours or even days. This may be acceptable if the analysis only needs to be run once. However, typical usage involves iteratively refining analysis parameters to improve precision, often requiring multiple analysis runs. In such cases, long execution times quickly become a major bottleneck.

To address this challenge, several parallel frameworks for abstract interpretation have been proposed (Monniaux 2005; Dewey, Kashyap, and Hardekopf 2015; Kim, Venet, and Thakur 2019). In this internship, we propose to explore a complementary approach: achieving parallelism through data-flow. Specifically, the idea is to divide the analysis across independent memory regions, enabling concurrent interpretation of disjoint parts of the program state.

Internship objectives

The objective of this internship is to design a theoretical framework for parallelizing the abstract interpretation of programs based on their dataflow. This involves substantial theoretical work, followed by the implementation of a prototype parallel analyzer that will serve as a proof of concept for potential integration into Frama-C / Eva. The prototype will be evaluated using the Open-Source-Case-Studies–a curated collection of open-source C programs designed for Frama-C analysis.

The internship will be structured in two phases. The first phase will focus on defining suitable coverings of the dataflow graph and exploring how to integrate dependent analyses for each subgraph. The second phase will address the simultaneous computation of the data dependency analysis and the parallel analysis.

Qualifications

• Minimal

  • Master student in Computer Science or Computer Engineering (M1/M2)
  • Knowledge of OCaml
  • Ability to work in a team

• Preferred

  • A certain flair/affinity for mathematical matters
  • Some knowledge of imperative programming, preferably C

Characteristics

• Duration: 5-6 months

• Location: CEA Nano-INNOV, Paris-Saclay Campus, France (Work From Home possible up to 2-3 days/week)

• Compensation:

  • €1300 (Bac+4/M1), €1400 (Bac+5/M2) monthly stipend
  • Maximum €229 housing and travel expense monthly allowance (in case a relocation is needed)
  • CEA shuttle in Paris region and 75% refund of transit pass
  • Subsidized lunches

Application

If you are interested in this internship, please send to the contact persons an application containing:

• Your resume
• A cover letter indicating how your curriculum and experience match the qualifications expected and how you would plan to contribute to the project
• Your bachelor and master transcripts, if any

Applications are welcome until the position is filled. Please note that the administrative processing may take up to 3 months.

Contact persons

For further information or details about the internship before applying, please contact:

• Valentin Perrelle (valentin.perrelle@cea.fr)
• David Bühler (david.buhler@cea.fr)

References