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.
Since these bugs were found during production prior to release, Windows 7 code did a good job is shown by the small number of bugs over the past 3 months in the NIST.GOV National Vulnerability Database, as of April 20, 2011:
Apple states that Mac OS X Snow Leopard is “The world’s most advanced OS”, it appears that one could conclude that as of April 20, 2011 OS X has some security issues. Especially since OS X is loosely based on Free BSD, which only has 6 security vulnerabiities.
Of course, no OS is secure, all operating systems have vulnerabilities, any assumption that your OS is secure is not a valid assumption. However, when you are designing, managing or maintaining software, don't you want your software to be secure? One of the ways you do this could be WhiteBox Fuzzing.
The way it works is that the Whitebox Fuzzer is a software program that runs dynamically while the program that is being tested is also run. The image below shows graphically how it works. Actually, it is a pretty poor schematic. Fuzz testing is form of blackbox testing, so called because in aerospace the aircraft use blackboxes and line technicians have to test them without opening them. In the case of WhiteBox Fuzzers, the system randomly mutates well-formed inputs and tests on the resulting data. Grammars are used to generate the well-formed inputs and encode application-specific knowledge and test heuristics. This could cause low code coverage is the input is a 32-bit input value. Using a concept titled systematic dynamic test generation which generally is based on a search algorithm utilizing collected constraints developed in earlier testing. This models a good human tester as they will repeat know tests that provide breaking scenarios over time. For all of this to make sense you would have to read the paper, which I suggest that you do.
If you want to learn more about Z3 or SMT, then take a look at this link, bear in mind that Microsoft is making this tool available but it is only uses the open source community language set, see the link:
SAGE performs a generational search by repeating four different types of tasks.
The reference paper is a tough read. So here it is in five sentences or less:
There, 5 sentences. But really read the paper it is worth the time.
And finally just in case I mentioned Alfred Thompson, or even thought about him while blogging, see his blog at http://blogs.msdn.com/alfredth
He had nothing to do with this blog if it goes badly.