False-Positive-Free Testing with Frama-C
Frama-C is an extensible framework for source code analysis. Pascal Cuoq, co-initiator of the Frama-C project and chief scientist and co-founder of TrustInSoft, a company that uses the Frama-C platform to guarantee software has no flaws, will receive a grant to build an open source TIS Interpreter, including all the extensions necessary to support the false-positive-free operation on OpenSSL. This work is based on TIS Analyzer, a commercial software analysis tool based on Frama-C, the extensible open-source framework for source code analysis. One issue impairing TIS Analyzer's widespread adoption is that it occasionally produces false positives: it can report security errors that are actually false alarms.
Cuoq's new project supports a new flavor of TIS Analyzer named “TIS Interpreter” and a methodology that detects bugs with no false positives. Thus, any bug that is reported actually needs to be fixed. American Fuzzy Lop fuzzer will be used to automatically generate new test cases for OpenSSL from which TIS interpreter can detect bugs.
TIS Interpreter, expected to be released as open source software in early 2016, will use existing test cases to detect bugs with no false positives, which saves developers’ time. CII is investing in this work, which combines existing technologies to test this new technique on OpenSSL, so that, if successful, it can be extended to other open source software to help developers better identify potential bugs and improve security.