Based on Pin, BAP converts assembly instructions to IL. Uses Z3.

It has taint references support? What does it mean?

1 Mayhem—system for finding exploitable bugs in binary programs. Every bug accompained by an exploit. Is it just an input? It is based on AEG's ideas. They combine online symbolic execution (S²E) and offline symbolic execution (concolic, SAGE). They have experiments proved that re-execution in offline mode can be very expensive. 2 Hybrid engine saves current execution state (PC), thread is restored by restoring the formula, concretely running the program up to the previous execution state, and then continuing. Main features:

1. Hybrid execution.
2. Index-based memory modeling.
3. Binary-only exploit generation.

3 They are looking for exploitable errors so they need low-level details (return addresses, stack pointers). They want to execute as much instructions concretely as possible. There are CEC (concrete executor client to run on CPU) and SES (symbolic executor server). CEC instruments the code and performs dynamic taint analysis. When CEC encounters a tainted branch condition, 4 it calls SES. SES receives a stream of tainted instructions from the CEC (it runs in parallel and produce concrete values) and jits the instructions to an IL. SES maintains path formula and exploitability formula. On tainted branch point SES queries SMT solver. For each tainted branch? If fork is needed, all the new forks are sent to the path selector to be prioritized. All new forks? There are many of them? If there is no more memory, checkpoint manager starts generating checkpoints instead of forking. During the execution, SES switches context between executors. CEC maintains a virtualization layer. They use BAP to convert x86 assembly to an BAP IL. Mayhem alternate between online and offline modes.

They said SAGE is concolic (= offline symbolic execution) and it has two steps: (1) concretely execute and record a trace; (2) 5 symbolically execute the instructions in the recorded trace. Is it their description of concolic? Online: S²E, KLEE, AEG. KLEE has an immutable state representation and S²E shares common state between snapshots of physical memory and disks. Checkpoints are SE state: path predicate, statistics, replay information. When for offline it is just seed. To restore concrete state Mayhem concretely executes the program until target instruction. So, it has reexecution anyway. But only when memory exhausted. 6 They said, standard concolic execution do symbolically re-execution.

CEC performs taint analysis and SES performs symbolic execution. Once more, taint analysis and symbolic execution are different things. If basic block is tainted it is sent to the SES for symbolic execution. Symbolic execution only for taint BB! During online execution CEC handles multiple concrete execution states. Concrete execution state: current registers, memory, OS state (files, network, kernel state). So, there are coppies of the one file. The virtualization layer mediates all system calls. States saving is incremental.

SES caps the number of symbolic executors. When memory is exhausted, it stops generating new interpreters and produces checkpoints. So, it goes online while it has memory, after ti generates checkpoints and does new runs.

Three heuristic ranking rules:

• execute new code or execute known code more times,
• memory accesses,
• symbolic instruction pointers with highest priority (?).

Optimizations:

• independent formula (as such in KLEE, but it keeps a map from input variables to formulas at all times),
• algebraic simplifications,
• taint analysis.

7 It has index-based memory model for symbolic memory handling. Memory model is a map: (32-indices) → (expressions). They said, symbolic index is very frequent in binary code. 40 % of the examples require to handle symbolic memory. In Mayhem writes are always concretized, but symbolic reads are allowed to be modeled symbolically.

Two simple approaches:

(1) Concretize index. Can miss paths. Common for offline executors, such as SAGE and BitBlaze. (2) Allow memory to be fully symbolic. Low performance. In McVeto, BAP, BitBlaze.

9 Exploit generation for:

• symbolic (tainted) instruction pointer,
• symbolic format string.

Add info.

13 Mayhem is on average 3.4× slower than AEG (based on source code), because it has no adventage of operating at a high-level abstraction. Wow!

Sergey Vartanov, 2007–2020