Key Design Points
The most important design question for constructing the constraint formula is to figure out what instructions to include in the formula. We need to include all the instructions for an exploitable path for the solver to generate a candidate exploit. However, the number of exploitable paths is usually only a fraction of all paths to the new check. Should the formula cover all such execution paths, some of them, or just one? We consider three approaches to answering this question: a dynamic approach which considers only a single path at a time, a static approach which considers multiple paths in the CFG without enumerating them, and a combined dynamic and static approach.

This is a really good example of combining Static Analysis and Dynamic Analysis to find and verify security vulnerabilities. Come see my Summercon presentation for more on this topic.

Acidus wrote:

In the automatic patch-based exploit generation problem, we are given two versions of the same program P and P' where P' fixes an unknown vulnerability in P. The goal is to generate an exploit for P for the vulnerability fixed in P'. More formally, we are given a safety policy F, and the programs P and P'. The purpose of F is to encode what constitutes an exploit. Our goal is to generate an input x such that F(P(x)) = unsafe, but F(P′(x)) = safe.

... ... !!!

There is something humbling about seeing hours work (reading the Microsoft security bulletin, using IDA and BinDiff, discovering the security changes, performing the needed "magic" like unicode evasion, no null's etc) reduced to a math equation.

Well well well....I've seen this discussed before, but never in an academic paper. I believe this paper to be dubious at best for multiple reasons, but I'll only list a few here

1) As they state in their first paragraph, it doesn't cover all threats, and I believe it covers less than they think
Proprietary network protocols, amongst other things

2) The times of generic exploit writing are coming to an end. Exploitation will be on a more application to application base.
ASLR, stack cookies, NX.

3) A PoC/Crash ISN'T an exploit in my opinion.
Botnets aren't formed on the concept of crashing IE.

4) Modern threats such as the Slammer worm have empirically demonstrated that once an exploit is available, most vulnerable hosts can be compromised in minutes [27]
Hello 2003, my name is 2008, it sure is a pleasure to meet you

Acidus wrote:

In the automatic patch-based exploit generation problem, we are given two versions of the same program P and P' where P' fixes an unknown vulnerability in P. The goal is to generate an exploit for P for the vulnerability fixed in P'. More formally, we are given a safety policy F, and the programs P and P'. The purpose of F is to encode what constitutes an exploit. Our goal is to generate an input x such that F(P(x)) = unsafe, but F(P′(x)) = safe.

... ... !!!

There is something humbling about seeing hours work (reading the Microsoft security bulletin, using IDA and BinDiff, discovering the security changes, performing the needed "magic" like unicode evasion, no null's etc) reduced to a math equation.

This article seems to have stirred up a bit of drama. I finally got time to read it this evening. These people have developed a powerful toolset that can be used to achieve some very interesting results, but I also think that what they've demonstrated here falls far short of what their abstract claims.

Basically, you get the impression that they can take a patch diff, pop it in a black box, and pull a program out the other side that can be used to launch remote code execution attacks. They then go on to assume that attackers can use tools like this to instantly produce exploits from a patch, and discuss the implications of that for patch distribution strategies. But thats not what they've produced.

What they've produced takes a patch diff as well as either input sufficient to reach the vulnerable code, or information about the place in the binary where the specific input values that exploit the vulnerability are read in, and produces permutations of that input which would be rejected by the patched version of the code.

In my view the time spent determining what sort of input can reach the vulnerable code (what inputs not what values of those inputs), and more importantly the time spend actually exploiting the vulnerability to gain unauthorized code execution, contribute more to the time required to produce working exploits from patch diffs than the part of the problem that has been solved by this paper, and so their conclusions about the impact of this result on the time from patch distribution to exploit distribution is not correct.

This tool could be helpful in analyzing vulnerabilities where a great deal of permutation occurs to data before the vulnerable code is reached, but it does not result in automatic generation of anything from patches alone, and it does not generate what I would call an exploit.

The underlying toolset, however, is very interesting. Its basically a computer that reads assembly code. You can program it to answer questions about that code. There are many questions that one could ask about binary code that would be helpful in vulnerability research and analysis beyond those envisioned here. Its a shame that these tools seem to not be available to the public.