Thales came to CEA-List with a request to certify a product with particularly tight cybersecurity requirements: a smart card. Specifically, the company needed formal proof of the security of a JavaCard OS implementation on a smart card. Smart card security methods, which vary from one card to another, are closely-guarded industrial secrets.
Due to the size of the software being certified, the formal models and the associated proofs required for certification can be in the tens of thousands of lines of code, making it difficult to apply formal modeling and proof tools like CEA-List’s Frama-C, Coq, or Atelier B. At CEA-List we have developed automated methods to effectively scale up formal approaches to larger software applications, making the work of software security engineers much easier. Add-ons to our Frama-C software enable the systematic and automated application of high level formal properties to each line of code to produce tens of thousands of unit proofs.
Thales had obtained Common Criteria Evaluation Assurance Level (EAL) 6 certification in 2022. These new formal verification capabilities enabled the company to obtain EAL7 certification, the highest level of certification attesting to the formal verification of an asset.
An expert’s eye is no longer enough to ensure software is secure. You need machine-verified proof
This successful partnership positions CEA-List to bring certification methods to use cases with stringent cybersecurity requirements in response to the needs of secure product market leaders. The research we conducted to effectively address these challenges produced scientific and technological advances that we integrated into our tools for the future benefit of projects in other industries.
