Frama-C The Frama-C GUI received a few quality-of-life improvements that have not been announced during the Magnesium release. This post presents some of them, along with general GUI tips. We focus on general-purpose UI improvements, while another post will discuss new Value-specific features, related to the new Values tab. These UI...
Read MoreThe Frama-C blog is back, with an extended set of writers and a different focus: small pieces of (informal) documentation and useful tips for Frama-C users. During its self-awareness period, the Frama-C blog realized that silence is a valid option, sometimes better than the alternatives. Still, we thought better to...
Read MoreA 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 MoreA buffer overflow has been discovered in recent versions of the HTTP server Nginx. Hacker News user jmnicolas pondered out loud: “I wonder if this discovery is a result of OpenBSD switching its focus from Apache to Nginx?” It took me one minute to understand what ey meant. I was...
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 More