1 Binary analysis is important. Problem: you cannot compare different tools. angr goal is to intergrate many of the state-of-the-art binary analysis techniques. 2 angr has both static and dynamic techniques. They do vulnerability discovery, exploit replaying and generation, compilation of ROP shellcode, exploit hardening. 3 SA has false positives, DA is not scalable, has path explosion problem.

pages 4—7, sections III—V skipped: backgrounds

7 angr is cross-architecture, cross-platform, 8 support different analysis paradigms, uses Python and IPython. The goal is to have framework on top of which you can reproduce any analysis technique in a week. They use VEX for multiple architectures support. For binary loading (.so, .dll) CLE (CLE Loads Everything) is used. It uses elftools for Linux and pefile for Windows. SimuVEX collects program state: registers, memory, POSIX, etc. 9 SimuVEX allows user to provide a powerful way to instrument blocks with Python code. Claripy module creates expression trees. Claripy has a set of frontends for tracking constraints, solving, several formulae optimizations, using VSA, etc. angr itself provides DSE and CFG recovery (could we correct CFG from SA using DA?). Two interfaces for full-program analysis: Path Group (any DSE—split pathes or terminate) and Analyses (any SA, it has KB).

10 For CFG recovery SA is uses: two algorithms CFGAccurate and CFGFast. CFGAccurate: forced execution, lightweight backward slicing (for context-sensitiveness), SE, VSA. Binary should not be obfuscated (for speed).

pages 11—12 to section IX skipped

13 Their DSE is based on Mayhem (memory model and path prioritization). Veritesting uses it as a base. So, they uses Veritesting or they implement it? Claripy populates the symbolic memory model using SimuVEX. Path object tracks actions, contains PC. PathGroup is for splitting, merging, and filtering of paths. Advanced state merging: statically and selectively merging paths.

They use under-constrained symbolic execution (UCSE). UCSE is a DSE where execution is performed on each function separately. Analysis is not accurate and suffers from FP. They add global memory under-constraining, path limiters (no more 64 paths for each function), false positive filtering (something about checking constraints, I don't understand). It is implemented as SimState plugin. 14 It can be performed using the same PathGroup paradigm as DSE.

Symbolic-assisted fuzzing is Driller. So, it is AFL as foundation and angr as symbolic tracer. Driller's symbolic component is implemented using angr's SE engine. At each step of the PathGroup (from concrete input from AFL), every branch is checked if it is unknown to AFL. Look, it is not concrete branch address for inversion. New input from solver is fed back to AFL.

Crash reproduction. Approach from Replayer.

Skipped

17 Veritesting has better results but found less vulneragilities than DSE alone. Veritesting uses efficient path merging and can go deeper before path explosion, but path merging introduces complex expressions (to support different values on merged paths), and solver stucks.

18 UCSE found a lot of vulnerabilities but with high false positives rate.

Sergey Vartanov, 2007–2020