Blog

Debugging Frama-C analyses: better privacy with C-Reduce
André Maroneze on 2 April 2020

Frama-C has a somewhat obscure plug-in called Obfuscator, whose original purpose was to help industrial users give the Frama-C developers enough information about confidential use cases, for debugging and optimizations. However, sharing proprietary code is never easy: is the obfuscation good enough? Are there legal issues involved? Is it worth...

Read More

SATE VI Workshop: Frama-C satisfies the Ockham Criteria
André Maroneze on 2 October 2019

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...

Read More

Habemus Frama-C in Fenestris (Frama-C on Windows, with WSL)
André Maroneze on 7 June 2019

We have successfully compiled and tested the beta release of Frama-C 19 (Potassium) in the WSL (Windows Subsystem for Linux), using Debian. Installation is not trivial, especially for the graphical interface, but in the future this should provide a more robust way to run Frama-C on Windows, than relying on...

Read More

Finding unexpected bugs in the DARPA CGC corpus
André Maroneze on 26 February 2019

Recently, we’ve been running Frama-C/Eva on the DARPA challenges from the SATE VI Classic track tool evaluation, organized by NIST. The C programs come from a Linux-compatible port of the DARPA Cyber Grand Challenge. The port was made by Trail of Bits and used as one of the evaluation sets...

Read More

Setting up an analysis with the help of frama-c-script
André Maroneze on 16 January 2019

Frama-C 18 (Argon) includes a new command, frama-c-script, which contains a set of helpful scripts for setting up new analyses. The available commands will likely expand in the future. We present here a quick overview of how to use them efficiently for a very fast setup. Presentation of frama-c-script frama-c-script...

Read More