Skip to content
Snippets Groups Projects
Commit 980d2a8c authored by Andre Maroneze's avatar Andre Maroneze
Browse files

add blog post on SATE 6 workshop

parent 2102f8e3
No related branches found
No related tags found
No related merge requests found
Pipeline #22935 passed
......@@ -4,3 +4,4 @@
*.tar.bz2 filter=lfs diff=lfs merge=lfs -text
*.svg filter=lfs diff=lfs merge=lfs -text
*.tar.gz filter=lfs diff=lfs merge=lfs -text
*.webp filter=lfs diff=lfs merge=lfs -text
---
layout: post
author: André Maroneze
date: 2019-10-02 16:00 +0200
categories: eva nist ockham sate sound value workshop
image: /assets/img/blog/measure.webp
title: "SATE VI Workshop: Frama-C satisfies the Ockham Criteria"
---
During the [SATE VI Workshop](https://samate.nist.gov/SATE6Workshop.html),
organized by the [NIST SAMATE](https://samate.nist.gov/) project,
Frama-C was confirmed as having satisfied
the [Ockham criteria](https://samate.nist.gov/SATE6OckhamCriteria.html) 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](http://blog.frama-c.com/index.php?post/2018/11/15/Frama-C/Eva-in-SATE-VI-with-Juliet-1.3) about our analysis of SATE VI's Juliet 1.3 test suite.
The code is [available on Github](https://github.com/Frama-C/SATE-VI), 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](https://cwe.mitre.org/data/definitions/1000.html), 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](https://github.com/Frama-C/open-source-case-studies/wiki/SATE-6-Classic-DARPA-CGC-report), 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](https://codesonar.grammatech.com/buginjector-white-paper-interest)
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](https://www.oasis-open.org/committees/tc_home.php?wg_abbrev=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](https://www.absint.com/astree/index.htm)
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.
assets/img/blog/measure.webp

131 B

  • Developer

    @alemesle : zut, le post n'apparaît pas dans l'index https://frama-c.frama-c.com/blog/index.html

    J'ai foiré quelque part sans doute ? Par exemple, est-ce qu'il faut rajouter des double quotes autour de mon nom dans author ?

0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment