Tag Archives: value

Frama-C blog becomes self-aware, author unnecessary
Pascal Cuoq on 19 May 2014

A reader's challenge A couple of days ago, faithful reader David Gil sent in a challenge: The reference code for Keccak/SHA-3 has a correctness bug in the Optimized64 implementation. Can the value analysis plugin find it? My patch fixing that bug was accepted; I believe that the trunk is correct...

Read More

An interesting SSL implementation bug: CVE-2013-5914
Pascal Cuoq on 23 February 2014

SSL in the news SSL is a protocol for point-to-point confidential and authenticated communication over an insecure medium. It is the protocol behind HTTPS, among many other uses. In an Internet-connected system, the SSL implementation stands at the frontier between the system and the hostile outside world. For this reason,...

Read More

Pascal Cuoq on 4 February 2014

Jesse Ruderman on assertions and fuzzing Jesse Ruderman has published a blog post on assertions and how they complement fuzzing. Key quote: “Fuzzers make things go wrong. Assertions make sure we find out.” Readers of this blog are accustomed to me talking about differential testing where a reference result (say...

Read More

Post-conditions and names of arguments
Pascal Cuoq on 17 January 2014

In an ACSL post-condition, any reference to the name of one of the function's arguments is assumed to refer to the initial value of the argument. /* ensures arg == 1; */ void f(int arg) { arg = 1; } For instance, in function f above, Frama-C's value analysis plug-in...

Read More

Scenario of security leak using Aorai and Value
Virgile Prevosto on 17 September 2013

This demo shows the usage of Aoraï and Value to generate a scenario of a security leak in the driver of a serial port (Linux kernel 2.6). It stems from the Calmos project with LabSoC at TelecomParisTech/Eurecom C source files and the Frama-C script that launches the analysis are available...

Read More