How is it possible to protect smart phones, information systems, and computers from cyber threats? How is it possible to develop high-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 introduced the SATE V Ockham Sound Analysis Criteria.
These criteria are meant to rule out tools that report even a single incorrect finding. Frama-C was the only technology to attempt to meet Ockham criteria requirements running on the Juliet 1.2 test suite from NIST. Moreover, Frama-C succeeded in satisfying the Ockham criteria for all five of NIST’s classes of weaknesses.
In the last 10 years, Frama-C was designed by CEA LIST and INRIA using funding from aeronautics and nuclear industries. The technology allows for comprehensive mathematical security 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 creates a new dimension in formal methods.
Now, Frama-C allows TrustInSoft to bring the reliability of critical systems software 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.
Collaborative formal methods are now able to ensure 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 must deploy such state-of-the-art static analysis methods. This habit will significantly reduce the impact of cyber threats.
See also: No more heartbleed.
See also: PolarSSL verification kit.
For any information on products or services, please contact us at: firstname.lastname@example.org