Description
This thesis develops new methods for addressing the problem of software security bugs, shows that these methods scale to large commodity software, and lays the foundation for a service that makes automatic, effective security testing available at a modest cost per bug found. We make the following contributions:
We introduce a new search algorithm for systematic test generation that is optimized for large applications with large input files and exhibiting long execution traces where the search is bound to be incomplete (Chapter 2).
We introduce optimizations for checking multiple properties of a program simultaneously using dynamic test generation, and we formalize the notion of active property checking (Chapter 3).
We describe the implementation of tools that implement dynamic test generation of large binary programs for Windows and for Linux: SAGE and SmartFuzz. We explain the engineering choices behind their symbolic execution algorithm and the key optimization techniques enabling both tools to scale to program traces with hundreds of millions of instructions (Chapters 2 and 4).
We develop methods for coordinating large scale experiments with fuzz testing techniques, including methods to address the defect triage problem (Chapter 4).