74 CoMMuniCations of the aCM | feBRuARy 2014 | voL. 57 | No. 2
aTTacKers commonLy eXpLoIT buggy programs to
break into computers. security-critical bugs pave the
way for attackers to install trojans, propagate worms,
and use victim computers to send spam and launch
denial-of-service attacks. A direct way, therefore,
to make computers more secure is to find security-
critical bugs before they are exploited by attackers.
Unfortunately, bugs are plentiful. For example, the
Ubuntu Linux bug-management database listed more
than 103,000 open bugs as of January 2013. specific
widely used programs (such as the Firefox Web browser
and the Linux 3.x kernel) list 7,597 and 1,293 open
bugs in their public bug trackers, respectively.a Other
projects, including those that are closed-source, likely
involve similar statistics. These are just the bugs we
know; there is always the persistent threat of zero-day
exploits, or attacks against previously unknown bugs.
Among the thousands of known bugs, which should
software developers fix first? Which are exploitable?
a All bug counts exclude bugs tagged as “wishlist,” “unknown,” “undecided,” or “trivial.”
How would you go about finding the un-
known exploitable ones that still lurk?
Given a program, the automatic exploit generation (AEG) research challenge is to both automatically find
bugs and generate working exploits.
The generated exploits unambiguously demonstrate a bug is security-critical. Successful AEG solutions provide concrete, actionable information
to help developers decide which bugs
to fix first.
Our research team and others cast
AEG as a program-verification task
but with a twist (see the sidebar “
History of AEG”). Traditional verification
takes a program and a specification of
safety as inputs and verifies the program satisfies the safety specification.
The twist is we replace typical safety
properties with an “exploitability”
property, and the “verification” process becomes one of finding a program path where the exploitability
property holds. Casting AEG in a verification framework ensures AEG techniques are based on a firm theoretic
foundation. The verification-based
approach guarantees sound analysis,
and automatically generating an exploit provides proof that the reported
bug is security-critical.
Verification involves many well-known scalability challenges, several
of which are exacerbated in AEG. Each
new branch potentially doubles the
number of possible program paths,
possibly leading to an explosion of
paths to check for exploitability. Traditional verification takes advantage
of source code, models, and other abstractions to help tackle the state explosion and scale. Unfortunately, ab-
The idea is to identify security-critical
software bugs so they can be fixed first.
By thanassis avGeRinos, sanG kiL Cha, aLexanDRe ReBeRt,
eDWaRD J. sCh WaRtZ, MaveRiCk Woo, anD DaviD BRuMLey
this research formalizes the notion of an
exploit, allowing for automated reasoning
the technology can be used to identify
and prioritize security-critical bugs.
improvements for verifying programs
safe may also lead to improvements for
automatically generating exploits. i i M