Category: Software Correctness

  • Buying Into Open Source Security

    If you were given the opportunity to spend USD 100 million over five years to maximally improve the security of open source software, what would you do? Let’s just assume that the money comes with adequate administrative staff to manage awards and contracts so you can focus on technical issues. A few ideas: Bug bounties,…

  • Testing with Pictures

    Testing code is fun and hard and looking at the problem in different ways is always good. Here’s a picture representing the behavior of a saturating subtraction operation, where the horizontal axes represent the inputs and the output is vertical: And here are some of the functions handed in by my students in the fall:…

  • Fun with Shellshock

    [I don’t seem to be getting blog entries written lately. The semester has turned out to be surprisingly busy and, also, I’m working on a few longer pieces that have ended up being harder to write than I’d hoped. Anyhow, the piece below isn’t the sort of thing I usually post, you can think of…

  • Proposal for a Friendly Dialect of C

    [This post is jointly authored by Pascal Cuoq, Matthew Flatt, and John Regehr.] In this post, we will assume that you are comfortable with the material in all three parts of John’s undefined behavior writeup and also with all three parts of Chris Lattner’s writeup about undefined behavior. Additionally, this paper is excellent background reading.…

  • Non-Transparent Memory Safety

    [This paper contains more detail about the work described in this post.] Instrumenting C/C++ programs to trap memory safety bugs is a popular and important research topic. In general, a memory safety solution has three goals: efficiency, transparency, and compatibility. Efficiency is obvious. Transparency means that we can turn on memory safety with a switch,…

  • ALIVe: Automatic LLVM InstCombine Verifier

    [This post was jointly written by Nuno Lopes, David Menendez, Santosh Nagarakatte, and John Regehr.] A modern compiler is a big, complex machine that contains a lot of moving parts, including many different kinds of optimizations. One important class of optimization is peephole optimizations, each of which translates a short sequence of instructions into a…

  • Finding Compiler Bugs by Removing Dead Code

    I was pretty bummed to miss PLDI this year, it has been my favorite conference recently. One of the talks I was most interested in seeing was Compiler Validation via Equivalence Modulo Inputs by some folks at UC Davis. Although I had been aware of this paper (which I’ll call “the EMI paper” from now…

  • We Need Hardware Traps for Integer Overflow

    Processors should support integer math instructions that optionally trap on overflow. Because popular architectures lack this feature, otherwise excellent modern systems programming languages, such as Rust, Go, and D, have default integer types that wrap. This is bad because unexpected wrapping causes programs to produce incorrect results, although of course integer overflow in a safe…

  • A Guide to Better Scripty Code for Academics

    [Suresh suggested that I write a piece about unit testing for scripty academic software, but the focus changed somewhat while I was writing it.] Several kinds of software are produced at universities. At one extreme we have systems like Racket and ACL2 and HotCRP that are higher quality than most commercial software. Also see the…

  • This Is Not a Defect

    In several previous blog entries I’ve mentioned that in some recent versions of C and C++, left-shifting a 1 bit into the high-order bit of a signed integer is an undefined behavior. In other words, if you have code that computes INT_MIN by evaluating 1