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

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

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