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:
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).
CEA-List’s formal software analysis know-how is exactly what France’s defense procurement agency, DGA, needs for its security code verification.”
