BINSEC applies symbolic execution to binary code to reveal security issues.
Fixing all of the vulnerabilities in a program would be cost-prohibitive, so finding those most likely to be used by attackers is vital. The PyABD algorithm, a new feature in BINSEC, zeroes in on vulnerabilities tied to attacker-controlled inputs, as they are easier to take advantage of. Logical constraints designed to prevent vulnerabilities from being exploited are generated automatically by the BINSEC algorithm—proven correct, complete, and minimal—ensuring that each constraint generated reflects a bug’s severity. The algorithm is better than existing techniques at determining bug severity, and the results are easier for evaluators to interpret. The research was presented at the Symposium on Principles of Programming Languages (POPL) 2024.
BINSEC is also being used in the SecurEval, Rev, and DefMal challenges, part of France’s national cybersecurity program.
Common Criteria, recognized internationally, is the most demanding security certification framework for information systems. The two highest levels of certification, Evaluation Assurance Levels (EAL) 6 and 7, require the formal verification of data privacy, integrity, and availability.
It was only natural for CEA-List researchers, with their broad, deep knowledge of both software security and formal methods, to tackle EAL 6 and 7. Leading digital security solutions provider IDEMIA turned to CEA-List and our experts for support with Common Criteria certification, leveraging a formal model separate from the code to obtain EAL 6 certification in the Netherlands in 2023.
Thales, another leader in the security space, partnered with CEA-List on formal methods for security as early as 2015. One of the partnership’s most recent innovations was to combine WP and MetACSL, two Frama-C plugins, to verify properties like data privacy and integrity.
This led to ANSSI recognizing Frama-C as the third formal-methods-based tool capable of responding to the highest Common Criteria certification levels.
Using Frama-C, Thales was able to earn an EAL 6 certification for one of its products from ANSSI in 2021. EAL 7 certification was obtained in 2022. The fact that the proof is obtained directly from the product code makes the certification even more robust.
As these results show, formal proof has an important role to play in high-level security certification, and CEA-List is a key source of specialized methods and software.
Frama-C is also being used in the SecurEval project, part of the national cybersecurity program. ANSSI and the French Directorate General for Armament are working with CEA-List experts on advanced software evaluation using Frama-C and BINSEC.
Whether it is to detect vulnerabilities or provide formal proof of security properties, having tools that can provide a high degree of assurance is a must in cybersecurity.
