Automatic Exploit Generation

The link is blurbtastic but points off to the meat, which is here: http://security.ece.cmu.edu/aeg/.

Leading paragraph on the abstract:

The automatic exploit generation challenge we address is given a program, automatically find security-critical bugs and generate exploits. Our approach uses a novel formal verification technique called preconditioned symbolic execution to make automatic exploit generation more scalable to real-world programs than without it. We implemented our techniques in a system called AEG, which we use to automatically generate 16 exploits for 14 open-source projects. Two of the generated exploits are against previously unknown vulnerabilities.

They have a pretty sweet video of some runs.

Another great example of how one can seek opportunities where others don't look -- because people misapply fundamental laws and principles. In years past, many people would have told you such a program is a fruitless endeavor, because of the Halting Problem. (One would have been a CS professor of mine!) The Halting Problem only shows that such programs can't be perfect, not that imperfect but tremendously useful examples can't exist.

A priori knowledge and fundamental principles are valuable, but they are often widely misapplied. This is a great "rock to look under," as such principles are often very powerful, yet a great many are mistakenly scared away and don't bother to look closely.

http://www.paulgraham.com/say.html