Given the extensive nature of static analysis, we are somewhat surprised that we have only found a couple of exploitable CQUAL type errors in our analysis. Some of the analyses are fairly new, so we may find more errors, but this is a bit of a surprise.
We are encouraged by one of the exploits that we did find. The Category 1 TOCTTOU exploit is one that would be difficult to find via runtime analysis. Typically, the association between the file descriptor and the file would not change, so benchmarks consisting of benign programs would not uncover this error. With static analysis, the inconsistency was clear.
Another aspect of the effectiveness of our approach is its ease of use, since most of the analysis process is automated. It is straightforward to apply the process to a modified kernel or new releases of the kernel. We tested this by running the tool against Linux version 2.4.18. After the kernel source tree is downloaded, and a few small changes are applied to the Makefile and two source files (see Section 3.2.1), the rest of the process requires little manual effort (except for identifying false positives). The time it takes to complete the process is also quite reasonable. As a matter of fact, most of the time is spent on kernel builds - our modified version of GCC collects information on controlled types while compiling the source code.
Here we present the times for the major steps. These numbers are only intended for a ballpark measure of the effort needed to perform analysis, so they should not be interpreted as representing the optimized performance of the tools. The test platform was a 667 MHz Pentium III machine with 128MB of memory. It took about 30 minutes to do the three clean kernel builds using our extended GCC to generate the annotation information. It should be possible to perform all this analysis in one kernel build, however. Most of that time is contributed by the GCC backend that generates machine code (whereas our GCC analysis code only works on the AST tree). We compared normal kernel build time with the build time that has our GCC analysis code enabled, and the difference is negligible. Annotation of the source by the Perl scripts took about 1 minute, And finally, it took about 10 minutes for CQUAL to perform the analysis. With the additional analysis overhead of a 15 minutes or less, we expect that an optimized process can be done sufficiently quickly for these tools to be useful for kernel programmers.