| Almost all software must accept input from untrustworthy sources: web servers, file servers, databases, and web browsers all read data from a network that is usually shared with untrusted, and often malicious, third parties. Even in the absence of network threats, untrusted inputs are still a problem. Operating system kernels receive untrusted data as arguments to system calls and windowing systems handle requests from clients they may not trust and that may not trust each other. Code that handles these untrusted inputs is a natural avenue for attack because any bugs in that code may lead to a critical vulnerability.;In this dissertation, we describe new static analysis techniques for verifying that software safely handles its untrusted inputs. Static analysis is performed at compile time, so bugs are caught during the development cycle, before the software is deployed. Our approach is based on type-qualifier inference, a lightweight software verification technique that has many practical benefits. Type-qualifier inference is sound, which means that, up to certain limitations of the C programming language, if our verification tool reports that a program is vulnerability-free, then it really is immune to certain classes of attack.;We have implemented and tested our algorithms in CQUAL, a type-qualifier inference tool originally developed by Jeff Foster, et al. We then used our analysis tool to find dozens of bugs in the Linux kernel and to build the best format-string bug detector to date. Analysis of our experimental results revealed two simple rules for writing easy-to-analyze code and several problems that future research in static security analysis tools should address. |
