Advanced Modular Static Analysis by Integration of Codex into Frama-C

Context: CEA List, Software Safety and Security Lab

CEA List is located at the heart of Université Paris-Saclay, Europe’s largest hub for public and private research. Within CEA List, the Software Safety and Security Lab pursues an ambitious mission: to help designers, developers, and validation experts deliver high-confidence systems and software. As systems grow increasingly complex, we leverage formal reasoning to demonstrate their trustworthiness, designing methods and tools that ensure compliance with the highest safety and security standards. Our work bridges academia and industry, collaborating with leading experts worldwide.

Our structure is straightforward: those who innovate are those who implement. Your contributions will directly shape the future of formal verification.

---

Work Description

Our team develops Frama-C, a widely recognized and mature code analysis platform for C programs that provides several analyzers as plug-ins. Written in OCaml, Frama-C allows users to annotate C programs with formal specifications in ACSL (ANSI/ISO C Specification Language). Using techniques like abstract interpretation, weakest precondition calculus, and runtime assertion checking, Frama-C verifies that programs meet their specifications.

Eva [FCBook’24] 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.

Over the recent years, we have also developped Codex, a cutting-edge modular static analyzer that builds on recent advances in SSA-based and value-based abstract interpretation [POPL’23,PLDI’24]. Within this new analyzer, we have also worked on numerical domains, automatic trace refinement and shape analysis in the recent years.

The main goal of this position is to share more algorithms and technological bricks between these two abstract interpretation based analyzers, so that each tool can benefit from the advanced features and continuous development of the other.

Another goal is to better integrate Codex into Frama-C, combining experimental breakthroughs with industrial-grade reliability. This integration will empower Frama-C users with Codex’s advanced capabilities while preserving the robustness and scalability that define Frama-C.

Your responsibilities will include: - share common modules between Eva and Codex, and identify features specific to one analyzer that could be shared between both. - design the library of shared abstract domains such that it can be used by Eva and Codex. - integrating Codex into Frama-C, using case studies, testsuites and benchmarks to demonstrate its effectiveness, particularly for modular (per-function) analysis. - improving the user interface for both Codex and Eva.

---

Qualifications

Requirements:

• Hands-on experience with significant OCaml developments - other languages are fine too, but you’ll need to convince us you can adapt in a snap.
• Background in abstract interpretation or theory of programming languages.
• Self-organized, with an ability to prioritize effectively.
• Team-minded.

Pluses:

• PhD in formal methods or experience in a research-intensive environment.
• Strong understanding of C.

---

Application

This position will be filled as soon as possible; yet a 3+-months procedure for administrative and security purposes is required.

• Matthieu Lemerre
• David Bühler
• Valentin Perrelle
• Allan Blanchard

---

References

• [FCBook’24] Abstract Interpretation with the Eva Plug-in. (D. Bühler, A. Maroneze, and V. Perrelle)
• [POPL’23] SSA Translation Is an Abstract Interpretation (M. Lemerre)
• [PLDI’24] Compiling with Abstract Interpretation (D. Lesbre, M. Lemerre)