Entry Cadar:2008:EAG from tissec.bib

Last update: Sun Oct 15 02:58:48 MDT 2017                Valid HTML 3.2!

Index sections

Top | Symbols | Numbers | Math | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z

BibTeX entry

@Article{Cadar:2008:EAG,
  author =       "Cristian Cadar and Vijay Ganesh and Peter M. Pawlowski
                 and David L. Dill and Dawson R. Engler",
  title =        "{EXE}: Automatically Generating Inputs of Death",
  journal =      j-TISSEC,
  volume =       "12",
  number =       "2",
  pages =        "10:1--10:??",
  month =        dec,
  year =         "2008",
  CODEN =        "ATISBQ",
  DOI =          "https://doi.org/10.1145/1455518.1455522",
  ISSN =         "1094-9224 (print), 1557-7406 (electronic)",
  ISSN-L =       "1094-9224",
  bibdate =      "Tue Dec 23 11:58:14 MST 2008",
  bibsource =    "http://portal.acm.org/;
                 http://www.math.utah.edu/pub/tex/bib/tissec.bib",
  abstract =     "This article presents EXE, an effective bug-finding
                 tool that automatically generates inputs that crash
                 real code. Instead of running code on manually or
                 randomly constructed input, EXE runs it on symbolic
                 input initially allowed to be anything. As checked code
                 runs, EXE tracks the constraints on each symbolic
                 (i.e., input-derived) memory location. If a statement
                 uses a symbolic value, EXE does not run it, but instead
                 adds it as an input-constraint; all other statements
                 run as usual. If code conditionally checks a symbolic
                 expression, EXE forks execution, constraining the
                 expression to be true on the true branch and false on
                 the other. Because EXE reasons about all possible
                 values on a path, it has much more power than a
                 traditional runtime tool: (1) it can force execution
                 down any feasible program path and (2) at dangerous
                 operations (e.g., a pointer dereference), it detects if
                 the current path constraints allow {\em any\/} value
                 that causes a bug. When a path terminates or hits a
                 bug, EXE automatically generates a test case by solving
                 the current path constraints to find concrete values
                 using its own co-designed constraint solver, STP.
                 Because EXE's constraints have no approximations,
                 feeding this concrete input to an uninstrumented
                 version of the checked code will cause it to follow the
                 same path and hit the same bug (assuming deterministic
                 code).\par

                 EXE works well on real code, finding bugs along with
                 inputs that trigger them in: the BSD and Linux packet
                 filter implementations, the dhcpd DHCP server, the pcre
                 regular expression library, and three Linux file
                 systems.",
  acknowledgement = ack-nhfb,
  articleno =    "10",
  fjournal =     "ACM Transactions on Information and System Security",
  journal-URL =  "http://portal.acm.org/browse_dl.cfm?idx=J789",
  keywords =     "attack generation; bug finding; constraint solving;
                 dynamic analysis; symbolic execution; test case
                 generation",
}

Related entries