SATE VI Workshop: Frama-C satisfies the Ockham Criteria

During the SATE VI Workshop, organized by the NIST SAMATE project, Frama-C was confirmed as having satisfied the Ockham criteria for sound analysis tools. Frama-C previously satisfied the SATE V Ockham criteria (2013-2016) and found hundreds of errors in the test material.

We reported in this blog about our analysis of SATE VI’s Juliet 1.3 test suite. The code is available on Github, so that anyone can install Frama-C and reproduce the results.

In this post, we summarize some of the discussions that took place during the workshop, including future directions for SATE VII.

The SATE VI Workshop took place at MITRE who are responsible, among other things, for the Common Weakness Enumeration, and focused mostly on the Classic track, which had the most tools participating in. With Frama-C, we briefly examined part of the DARPA CGC test suite, one of the code bases available for SATE 6 Classic, finding some unintentional bugs.

The official report is still being finalized, but a few interesting points could be observed from the presentations and discussions:

• The Wireshark code base was a bit too large for some tools, while the SQLite code base seemed to hit a sweet spot between code size and bug complexity.
• The bugs injected via GrammaTech’s Bug Injector tool were not as diverse as one might expect, but nevertheless it managed to insert bugs that were able to discriminate sufficiently between tools. That is, if the bugs were “trivial” or “impossibly hard”, then either all or none of the tools would have found them; instead, there was a wide distribution between tools.
• Some tools had issues mapping the results to the locations expected in the test oracles, either because some oracles were no longer up-to-date, or because each tool’s definition of sinks and sources (the lines in the code where bugs manifest themselves, and those in which the bug is actually present) were not necessarily identical to the expected ones.
• Several tools ended up finding more bugs than the injected ones, which is not surprising given the size of the code bases.
• The SARIF format will be the default (and likely only) format for SATE VII. This should minimize the time necessary for NIST to process the results. All present tool developers were either already SARIF-compatible, or intended to become in the nearby future (including Frama-C).
• Besides Frama-C, Astrée participated in the Ockham track, and also satisfied the criteria. A few other tools also participated, but some details were still being discussed. Overall, at least 4 tools participated in the Ockham track, which is a progression from the previous edition. We see this as a positive evolution of the importance of sound analyses.

Overall, the tool exposition workshop was very informative, and we thank NIST for meeting the challenges of organizing it, including very extensive and helpful feedback.

The visibility offered by SATE helps tool developers to showcase their work, and allows users to obtain important feedback about them. Incorporating a static analysis tool in a development toolchain has a cost, but may bring considerable benefits; being able to better estimate this trade-off is an important outcome of NIST team’s work.