Billions and Billions of Constraints: Whitebox Fuzz Testing in Production

  • Ella Bounimova ,
  • Patrice Godefroid ,
  • David Molnar

MSR-TR-2012-55 |

We report experiences with constraint-based whitebox fuzz testing in production across hundreds of large Windows applications, multiple Microsoft product releases, and over 400 machine years of computations from 2007 to 2012. Whitebox fuzzing leverages symbolic execution on binary traces and constraint solving to construct new inputs to a program. These inputs execute previously uncovered paths or trigger security vulnerabilities. Whitebox fuzzing has found one-third of all file fuzzing bugs during the development of Windows 7, saving millions of dollars in potential security vulnerabilities. We present two new systems developed to manage our deployments: SAGAN, which collects data from every single fuzzing run for further analysis, and JobCenter, which controls deployment of our whitebox fuzzing infrastructure across commodity virtual machines. Since June 2010, SAGAN has recorded over 3.4 billion constraints solved, millions of symbolic executions, and tens of millions of test cases generated. Our work represents the largest scale deployment of whitebox fuzzing, including the largest computational usage ever for a Satisfiability Modulo Theories (SMT) solver, to date. We highlight specific improvements to whitebox fuzzing driven by our data collection and open problems that remain.