: Brian ChessVenue
: IEEE Symposium on Security and Privacy Date
Defect Type: Buffer overflows, race conditions
Uses Annotations: Yes
Requires Annotations: Yes
This paper presents a technique for reasoning about bug presence in C programs. The method works by processing the C source code in two successive stages to produce verification conditions, which it feeds into a theorem prover. The first stage translates the C source code into a new language based on Dijkstra’s Guarded Command language and augments the command with function specifications written by the programmer in a language based on ESC/Modula-3’s specification language. The second stage takes the guarded commands and translates them into verification conditions, which it then feeds to the theorem prover to determine if the code contains bugs.
The author validates his work by comparing his tool’s (called Eau Clair) results against two known bugs: a buffer overflow vulnerability in an RSA encryption library and a race condition in Red Hat’s lpr utility. The results for both vulnerabilities were nearly perfect: the tool flagged the vulnerability and only reported one false positive in each case, which was fixed by making a small specification change. Red Hat had previously attempted to fix the race condition but Eau Clair revealed that it was still present. The author noted that Eau Clair also took about 25 times as long as compiling to finish, and suggests Eau Clair be part of a pre-release process rather than a compile-time process. Eau Clair’s performance is outstanding on the test cases that the author used. Even though the test cases were decently sized programs, two test cases are not enough to conclude that the tool is useful in general.