Paper:   Automatic Exploit Generation, T. Avgerinos, et. al.
Date:    September 14, 2015
My name: Mark Greenstreet

1. What problem does the paper address?
     Large software projects (e.g. linux distros) have thousands of known
     bugs.  We need a way to identify those bugs that are most vulnerable
     for creating security exploits.

2. What is the key insight/idea in the paper's solution to this problem?
     The paper uses symbolic execution to find exploit-examples.  They
     introduce several techniques such as "preconditioned symbolic execution"
     and "buggy path first" to try to focus the search on traces that are
     most likely to have exploits.

3. What did the authors do to demonstrate their claims? (e.g. implement a tool,
   present a proof, run simulations, etc.)
     They have implemented an open source tool, Mayhem.  They described its
     operation showing how it found an exploit in the acpi_listen utility.
     They stated that they've found exploitable bugs in several applications
     for streaming media and for networking.

4. Is the support for the claims convincing? Why or why not?
     The authors have used Mayhem to find zero-day exploits in code that is
     in widespread use.  That's pretty compelling.  OTOH, I would have liked
     to have seen a comparison that gave a more compelling justification for
     their design choices.  For example, they use "buggy path first" -- can
     they compare this with randomized path selection in KLEE [0] or
     "generational search" in [20]?

5. What are your questions or other comments about the paper?
     I like the paper as intro to exploit generation, and the role of formal
     analysis techniques for generating exploits.  The paper is definitely
     aimed at a general, computer science audience, and left many slightly
     deeper "But what about...?" questions unanswered.  On the other hand,
     the references are *very* good.  I enjoyed skimming 4 or 5 of the
     references when I was curious about "return-oriented programming" [33],
     reading about modeling the x86 shl instruction in SAGE [4], etc.