An ongoing challenge for Microsoft are security bugs in file parsers, for instance in IE, Office or Windows.
There are patches, but creating them is time-consuming and expensive (it is estimated that such a bug costs Microsoft 1 million dollar) Therefore they perform random fuzz testing, but this does not find all bugs.
A better solution is whitebox fuzz testing: This leverages symbolic execution on binary traces and constraint solving to construct new inputs to a program.
This talk is not about the technique, but about the specific problems of scaling this approach to large programs (like Word or Excel)
- Symbolic execution on long traces
- Fast constraint generation and solving
- Month-long searches
- Hundreds of test drivers & file formats
- Fault tolerance (during the running months, Windows or compilers might change)
Symbolic execution of an office app started with 1.145 billion instructions.After some pruning of instructions not related to file handling, it took 45 minutes to generate the constrains and only 15 minutes to find the answer. Wow!
One of the ideas to speed up the process is to analyze commonalities in source code. As there are many similar branches (most common branch appears 17761 times out of 290430 symbolic executions) This motivates the symbolic summarization.
- Constraint generation is as important as solving
- Telemetry data enables imrpovements
- Sharing is common between Windows programs and can be exploited
- Automatic control and configuration is needed to scale