From e70f271ec09efed0cafe711aaabdff9aa0e2fc60 Mon Sep 17 00:00:00 2001 From: Andre Maroneze Date: Thu, 3 Oct 2019 11:37:26 +0200 Subject: [PATCH 1/3] test blog post in markdown --- _posts/2019-10-02-sate-6-workshop.md | 66 ++++++++++++++++++++++++++++ 1 file changed, 66 insertions(+) create mode 100644 _posts/2019-10-02-sate-6-workshop.md diff --git a/_posts/2019-10-02-sate-6-workshop.md b/_posts/2019-10-02-sate-6-workshop.md new file mode 100644 index 00000000..04fd0eee --- /dev/null +++ b/_posts/2019-10-02-sate-6-workshop.md @@ -0,0 +1,66 @@ +## 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. -- GitLab From 98e3ede06e5d85b59f47272da697931ce795ef6b Mon Sep 17 00:00:00 2001 From: Augustin Lemesle Date: Thu, 3 Oct 2019 12:41:01 +0200 Subject: [PATCH 2/3] Update .gitlab-ci.yml --- .gitlab-ci.yml | 2 -- 1 file changed, 2 deletions(-) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 363e8d38..1f41f4aa 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -35,7 +35,5 @@ pages: paths: - public expire_in: 1 month - only: - - master tags: - docker -- GitLab From af4e8058a75f1988de141e63444795dc95da2f9b Mon Sep 17 00:00:00 2001 From: Augustin Lemesle Date: Thu, 3 Oct 2019 12:41:59 +0200 Subject: [PATCH 3/3] Update .gitlab-ci.yml --- .gitlab-ci.yml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 1f41f4aa..18ec680a 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -23,6 +23,8 @@ test: expire_in: 1 month except: - master + tags: + - docker pages: stage: deploy @@ -35,5 +37,7 @@ pages: paths: - public expire_in: 1 month + only: + - blog-post-markdown tags: - docker -- GitLab