Largest use of Whitebox Fuzzers finds GIANT number of security bugs in Windows 7

This was a draft that got released by accident, the earlier blog post is the corrected one with more explanations.  Apologies, but I am not going to pull this one as it is different and there is a comment attached to it now.

In a paper titled: Incremental Compositional Dynamic Test Generation, researchers from the University of Wisconsin, Madison, during the production phase of Windows 7, found one-third of all of the security bugs in Windows 7, using a process called Satisfiability Modulo Theories (SMT) solver or as it also known as: Z3

Most of the bugs found were Buffer Overruns, and this new technique dynamically tested BILLIONS of instructions using a WhiteBox fuzzer called the SAGE.

The reference paper is a tough read. So here it is in five sentences or less:

  1. Ask this question: Given a set S of symbolic test summaries for a program Prog and a new version Prog′ of Prog, which summaries in S are still valid must summaries for Prog′?
  2. Present three algorithms with different precision to statically check which old test summaries are still valid for a new program version.
  3. Create a simple impact analysis of code changes on the static control-flow and call graphs of the program
  4. More precise predicate-sensitive refined algorithm using verification-condition generation and automated theorem proving
  5. Checking the validity of a symbolic test summary against a program regardless of program changes

There, 5 sentences. But really read the paper it is worth the time.