I'm kicking off my day with "Bug Finding by Solving Constraints in the Cloud" given by David Molnar.
Security bugs are costly, and there is a bug cycle...
Classic technique fro finding bugs is Fuzz Testing where you feed malformed files, strings and commands to your application and see whether it crashes. Interestingly, despite this being a fairly basic technique, it finds lots of bugs. But fuzz testing doesn't work well with unlikely paths, the edge cases. The fix being talking about today is fuzz testing plus dynamic test generation.
Trace the dynamic execution of the program, capture the symbolic path conditions, create symbolic formula for new path, solve new oath conditions and generate a new test case from solution.
Does this scale? The first generation of tools, like EGT, were exciting but only tested cases where the program was less than 2KLOC of code.
He's now talking about two tools. SAGE, which he worked on at Microsoft and is still internal, and SmartFuzz. You can actually get SmartFuzz, and it scales to larger code by running it in the cloud on Amazon EC2 instances.