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
The reference paper is a tough read. So here it is in five sentences or less:
- 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′?
- Present three algorithms with different precision to statically check which old test summaries are still valid for a new program version.
- Create a simple impact analysis of code changes on the static control-flow and call graphs of the program
- More precise predicate-sensitive refined algorithm using verification-condition generation and automated theorem proving
- 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.