12PRINCIPLES OF SYMBOLIC EXECUTION
Symbolic execution tracks metadata about the program state, just as taint analysis does. But unlike taint information, which only lets you infer that part of the program state affects another, symbolic execution allows you to reason about how the program state came to be and how to reach different program states. As you’ll see, symbolic execution enables many powerful analyses not possible with other techniques.
I’ll start this chapter with an overview of the basics of symbolic execution. Then, you’ll learn more about constraint solving (specifically, SMT solving ), which is a fundamental building block of symbolic execution. In Chapter 13, you’ll use Triton, a binary-level symbolic execution library, to build ...
Get Practical Binary Analysis now with the O’Reilly learning platform.
O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.
