Academic tools and real-life bug finding in Win32

Although computer-aided program verification and bug finding receives significant attention in academic circles, very little information on these efforts has been presented at conferences for security practicians; this talk intends to shed some light on the subject. Particularly, many security professionals believe that the academic tools cannot be used for practical tasks, while in fact some of the tools have been quite successful in some aspects.

It is crucial to make a distinction between "program verification" and "checking". The goal of the former is to prove that a given program is fully correct. Generally, this goal cannot be reached. One of the basic theorems of the computer science is "the halting problem", which states that there does not exist an algorithm to tell whether a Turing machine (which is an abstraction of a computer) terminates its calculation on a given input. Even intuitively, proving program correctness is harder than the halting problem; therefore, only in particular, simple cases one can attempt to prove program correctness. During the talk, a sample session of Caduceus tool will be presented, and some trivial C programs will be proven.

On the other hand, "program checking" does not attempt to prove full correctness, but rather to check whether selected properties hold. It is similar to a typical security audit, when an auditor tries to check that usage of potentially dangerous programming constructions is safe. "Program checking" is a best effort approach, as it does not guarantee completeness of any kind. However, automatic program checkers are able to find interesting bugs; the talk includes appropriate examples of bugs in Linux kernel, discovered by the MECA tool developed in Stanford University.

Because of many reasons, nowadays the security (or the lack thereof) of Win32 systems is important for security researchers. It would be very useful to have a tool capable of finding bugs in Win32 programs. As there is no publicly available source code, one has to work with assembly code, which presents another set of problems. Besides Halvar Flake's work, there is little related material available. During the talk, the New Jersey Machine-Code Toolkit will be presented, which allows a programmer to easily capture assembly instructions semantics.

Finally, a working prototype of a tool which checks for integer overflows in Win32 binaries will be presented. The choice to look for integer overflows is very compelling for at least three reasons: 1) This kind of vulnerability was the cause of major, recent problems in Windows security 2) Most probably, many similar bugs remain undiscovered 3) It is relatively easy to use a theorem prover to check for this type of vulnerability

Currently, the tool is unable to handle many programming constructions, which makes it unfeasible to use it for most binaries; however, for some programs it performs reasonably well. When applied to "nwwks.dll" binary, which implements a service addressed by a recent MS bulletin, the tool discovered seven cases of suspicious integer calculations; among them, three were real remotely exploitable bugs.