Practical Binary Analysis

13PRACTICAL SYMBOLIC EXECUTION WITH TRITON

In Chapter 12, you became familiar with the principles of symbolic execution. Now let’s build real symbex tools with Triton, a popular open source symbolic execution engine. This chapter demonstrates how to build a backward slicing tool, increase code coverage, and automatically exploit a vulnerability with Triton.

There are a handful of symbolic execution engines in existence, and only a few of them can operate on binary programs. The best-known binary-level symbex engines are Triton, angr,¹ and S2E.² KLEE is another well-known symbex engine that operates on LLVM bitcode instead of binary code.³ I’ll use Triton because it integrates easily with Intel Pin and is slightly faster because of its C++ backend. ...