Frama-C technolog ymeets NIST high assurance standards

How is it possible to protect smart phones, information systems and computers from cyber threats? How is it possible to have good quality software able to resist common cyber threats? To answer these questions the National Institute of Standards and Technology (NIST) launched the Static Analysis Tool Exposition (SATE). This exposition is designed to compare static analysis tools that find security-relevant defects in source code. This year, for the first time, the NIST has introduced the SATE V Ockham Sound Analysis Criteria. This criteria is made for tools which never report incorrect findings. The Frama-C technology was the only technology to attempt to meet Ockham criteria requirements running on the Juliet 1.2 test suite from NIST. The Frama-C technology satisfies the Ockham criteria for all five classes of weaknesses covered.

Technology behind the success

Over the last 10 years, Frama-C has been designed by CEA LIST and INRIA using funding from aeronautics and nuclear industries. This technology allows for mathematical guarantees on real software implementations. Frama-C is able to achieve this level of quality because it relies on advanced collaboration mechanisms between formal methods. Collaboration between these state-of-the-art algorithms brings formal methods to a new dimension. Frama-C is industrially supported by TrustInSoft, and now TrustInSoft brings the reliability of critical systems to the IT industry. For instance, several open source modules have been validated thanks to Frama-C and are now immune to common cyber threats

So, what will change?

Formal methods are now able to assess the immunity of widely used pieces of software against the most common threats. This means that any organization in charge of designing or integrating software should make sure state-of-the-art static analysis methods have been used. This habit will significantly reduce the impact of cyber threats.

About TrustInSoft

TrustInSoft is a French cyber-security startup born in 2013. TrustInSoft is a software publisher that provides tools and methods to validate software source code. TrustInSoft solutions enable to remove flaws in software with guarantees. For this reason TrustInSoft solutions are used for mission critical software in IT and embedded systems. TrustInSoft sells licenses of TrustInSoft Analyzer: the industrial version of the Open Source Software analysis platform Frama-C. TrustInSoft also sells “Validation Kits”: each Validation Kit is a detailed report on the security of well-known Open Source Software. This new kind of product gives TrustInSoft’s customers affordable access to state-of-the-art formal methods based security assessments. Thanks to Validation Kits, integrating Open Source stacks is faster and more secure than ever.

Contact :

Fabrice Derepas

fabrice.derepas@trust-in-soft.com

+1 202 657-5661

About CEA LIST

Within the CEA Technological Research Division, the CEA LIST institute carries out research on intelligent digital systems. Its R&D programs, all with potentially major economic and social implications, focus on advanced manufacturing (robotics, virtual & augmented reality, non destructive testing, vision), embedded systems (computing architectures, software and systems engineering, security & safety), and ambient intelligence (sensors, instrumentation & metrology, communication & sensory interfaces, data processing & multimedia). By developing cutting-edge technological research with applications in the industrial markets of transports, defense and security, manufacturing, energy and health, the CEA LIST helps its partners to enhance their industrial competitiveness thanks to innovation and technology transfer.

Contact :

Florent Kirchner

florent.kirchner@cea.fr

+33 (0) 1 69 08 00 10

French Alternative Energies and Atomic Energy Commission 1