Month: November 2013

  • C-Reduce and Frama-C

    Yesterday Pascal wrote a nice article addressing practical issues in automated testcase reduction. One issue is that C-Reduce tends to give you what you asked for instead of what you really wanted. Of course, this problem is a common one when performing algorithmic searches. Beyond computer science, the same problem comes up in basically every…

  • Informative Assertion Failures

    The other day a student was asking me how to make assertion failures in software more informative. I told him there are two pretty easy ways to do this. First, define a customized assert that takes two arguments: the predicate and also a description. For example, in the Botan crypto library we see lines like…

  • Safe, Efficient, and Portable Rotate in C/C++

    Rotating a computer integer is just like shifting, except that when a bit falls off one end of the register, it is used to fill the vacated bit position at the other end. Rotate is used in encryption and decryption, so we want it to be fast. The obvious C/C++ code for left rotate is:…

  • Integer Undefined Behaviors in Open Source Crypto Libraries

    Crypto libraries should be beyond reproach. This post investigates integer-related undefined behaviors found in crypto code written in C/C++. Undefined behavior (UB) is bad because according to the standards, it destroys the meaning of any program that executes it. In practice, over the last decade compilers have become pretty smart about exploiting integer undefined behaviors…

  • A New Compiler Fuzzing Paper

    Google Scholar’s recommendation engine has turned out to be a great resource for learning about new papers. Recently this paper about compiler fuzzing turned up in my feed and I was hooked after noticing that they claim to find a lot more compiler bugs during a 12-hour fuzzing run than Csmith can find. The work…

  • Producing Good Software From Academia

    Writing and maintaining good software from academia isn’t easy. I’ve been thinking about this because last week my student Yang Chen defended his thesis. While I’m of course very happy for him, I’m also depressed since Yang’s departure will somewhat decimate the capacity of my group to rapidly produce good code. Yang looked over my…

  • Trust, But Verify

    CompCert is an optimizing C compiler whose output provably has the same semantics as its input, at least when the input programs are conforming. Of course this high-level view sweeps a huge number of details under the rug. If we want to gain confidence in CompCert’s correctness we’ll need to either dig into these details…