Frama-C 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 MoreSSL 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 MoreJesse 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 MoreIn 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 MoreThis 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