Skip to content

{ Category Archives } Software Correctness

A New Development for Coverity and Heartbleed

As a consequence of my last post, I spent some time on the phone Friday with Andy Chou, Coverity’s CTO and former member of Dawson Engler’s research group at Stanford, from which Coverity spun off over a decade ago. Andy confirmed that Coverity does not spot the heartbleed flaw and said that it remained stubborn […]

Heartbleed and Static Analysis

Today in my Writing Solid Code class we went through some of the 151 defects that Coverity Scan reports for OpenSSL. I can’t link to these results but take my word for it that they are a pleasure to read — the interface clearly explains each flaw and the reasoning that leads up to it, […]

Automated Reasoning About LLVM Optimizations and Undefined Behavior

Following up on last week’s toy use of Z3 and my LLVM superoptimizer post from a few weeks ago, I wanted to try to prove things about optimizations that involve undefined behavior. We’ll be working with the following example: Clang’s -O0 output for this code is cluttered but after running mem2reg we get a nice […]

Writing Solid Code Weeks 7 and 8

The students continued with their compressor/decompressor development. Coverity continued to find plenty of issues for the students to fix. I’m about to start doing a bit of differential testing of their code, using voting to determine who is correct and who is wrong. I lectured on paranoid programming and on building a fuzzer, for sort […]

Paranoid Programming

A lot of software defects stem from developers who lack a proper sense of paranoia. While paranoia can of course be taken to idiotic extremes, a healthy respect for Murphy’s Law is useful in programming. This post is a list of useful paranoid techniques that I hope to use as the basis for a lecture […]

Writing Solid Code Weeks 5 and 6 — The Plot Thickens

Last week was pretty relaxed, I lectured on doing code reviews — pretty much the standard pitch. This week we spent Tuesday doing a code review, I think it went pretty well. I had chosen a team whose code was strong so that our first code review would be a positive one. Today I announced […]

Assertions Are Pessimistic, Assumptions Are Optimistic

We assert a condition when we believe it to be true in every non-buggy execution of our program, but we want to be notified if this isn’t the case. In contrast, we assume a condition when our belief in its truth is so strong that we don’t care what happens if it is ever false. […]

Scary Compiler Code Motion

I ran across this blog post about reader-writer locks and thought it would be fun to present them to the Advanced Operating Systems class that I’m running this spring. Here’s my version of the code, which needed to be adapted a bit to work with GCC: At first I was suspicious that some sort of […]

Use of Assertions

Assertions are great because they: support better testing, make debugging easier by reducing the distance between the execution of a bug and the manifestation of its effects, serve as executable comments about preconditions and postconditions, can act as a gateway drug to formal methods. Assertions are less than great because they: slow down our code, […]

Writing Solid Code Week 4

This week most of the students in the class (but not everyone, since we ran out of time) presented their arguments about the quality of various UNIX utility programs. This was a bit more interesting than it might otherwise have been since some of the utilities running on our student lab machines are hilariously old […]