Cybersecurity and Safety analysis with Frama-C / Eva

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.

Internship objectives

We are constantly working on improving the usability and applicability of the analysis towards security-related properties. We are currently seeking students for both development and research internships.

Research internships

AST diff for incremental analyses.

Recent advancements by the team have allowed Frama-C / Eva to support incremental analyses (Razafintsialonina et al. 2025). The core idea is to leverage the results of a prior analysis to accelerate the processing of subsequent analyses on slightly modified source code.

This is a crucial feature for integrating Frama-C into continuous development workflows, ensuring code safety at all times. Incremental analysis relies on algorithms that compute the differences between two versions of a source code. While traditional code diff algorithms are widely available, they are typically optimized for human readability—focusing on line-by-line comparisons.

However, for differential analysis, we need comparisons that operate at the level of program structures, such as functions, blocks, or loops. Furthermore, we need to detect semantic changes—like variable renaming—that may result in many textual differences but conceptually represent a single change.

The objective of this internship is to design, implement, and evaluate an AST-diff algorithm specifically tailored to the needs of incremental analysis.

Specification Language for Abstract Interpreters.

The ANSI/ISO C Specification Language (ACSL) (Baudin et al., n.d.) is used in Frama-C as a specification language shared between developers, users, and Frama-C plugins. It allows the specification of what a function does, should do, or must do. For the Eva plugin, ACSL plays a critical role when analyzing incomplete code—such as code that relies on third-party libraries (without available source), inline assembly, or mixed-language components—by providing formal specifications to replace missing code segments.

Despite its usefulness, ACSL is not always well suited for abstract interpretation. Its declarative style can be challenging for interpreters to handle precisely, and writing accurate, detailed annotations is often time-consuming. An alternative approach would be to introduce an imperative specification language—syntactically close to C but extended with constructs for non-determinism—better aligned with the needs of abstract interpretation.

The objective of this internship is to design such a language, implement a corresponding compiler within the Frama-C platform (specifically for use with the Eva plugin), and evaluate its effectiveness by specifying parts of the C standard library.

Software Development internship

Parallel analyses in Frama-C / Eva.

While abstract interpretation is among the fastest sound approaches to program verification, the analysis of complex software can still take several hours or even days to complete. 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). Moreover, with the introduction of domains in OCaml 5, there is now an opportunity to enhance Frama-C with native parallelism.

The goal of this internship is to implement parallel execution capabilities for Eva analyses within Frama-C. This will involve extending the Frama-C kernel and adapting internal data structures—particularly hash-consed data structures—to be compatible with parallel computation. The proposed implementation will be evaluated first on independent analysis tasks, and later on the analysis of concurrent programs (Monat and Miné 2017), where the same code must be analyzed from the perspective of multiple threads.

Intermediate Representation for Frama-C / Eva’s Analysis Results.

The results of abstract interpretation can almost always be expressed as mathematical formulas—for example, x ∈ [0, 10] or x + y = 10, where x and y are program variables (local or global). In Frama-C, these results serve two main purposes: they are either presented to users via the terminal or graphical interface, or consumed by other plugins as formal facts to support further analysis. Depending on the context, up to five different output formats may be required.

Abstract interpreters typically consist of multiple abstract domains, each specialized in inferring a specific class of formulas. Eva, for example, incorporates around a dozen such domains. Exporting analysis results requires a dedicated implementation for each domain. As a result, not all domains currently support result export, and those that do often provide only limited, textual output.

The goal of this internship is to design and implement a unified intermediate representation (IR) for analysis results. This IR will be constructed by each abstract domain and then translated into the required output formats. It will capture both logical formulas and memory models, providing a standardized and extensible way to represent abstract interpretation results.

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 with the Frama-C platform
  • 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