Together, DGA and CEA-List move security code analysis forward

CEA-List’s partnership with the agency is focussed on extending the formal analysis software applications Frama-C (C source-code) and BINSEC (binary code) to new, security-specific code structures and features as needed by the agency and its suppliers. The partnership has produced two BINSEC demonstrators:

• A tool to verify the secure deletion of confidential data (passwords, encryption keys, etc.) after a program is run;
• A binary-to-C decompiler, which checks binary code embedded in C code.

For Frama-C, the research has focused its plug-in used to verify that a program complies with its specifications. Mixed modeling of the memory has been used to analyze, in detail, low-level operations without the total analysis time being prohibitive. Two code operation models are used in the analysis: a high-level model of usual operations, and a low-level model of complex operations that act directly on the program’s working memory [1]. Two feasibility studies on Frama-C confirmed that there was no leakage of confidential data or indeterminate memory access behavior.

The conclusive results led to two new projects: integration of the results into Frama-C, and a BINSEC plug-in to detect hidden channel flaws in post-quantum cryptographic primitives (i.e security algorithms protecting against attacks by a quantum computer).

[1] Jérémy Damour, Allan Blanchard, Loïc Correnson, Frédéric Loulergue. Formalization of a region analysis for Frama-C/WP. 36es Journées Francophones des Langages Applicatifs (JFLA 2025), Jan 2025, Roiffé, France. ffhal-04859489

Contributed to the article

• Allan Blanchard, research engineer and head of the Frama-C team
• Sébastien Bardin, research engineer and head of the BINSEC team