Skip to content

Commit

Permalink
Document state options, add appendices for state options and claripy ops
Browse files Browse the repository at this point in the history
  • Loading branch information
@rhelmot
rhelmot committed Aug 29, 2017
1 parent e66cd1d commit fa3d78f
Show file tree
Hide file tree
Showing 5 changed files with 226 additions and 76 deletions.
3 changes: 3 additions & 0 deletions SUMMARY.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -29,5 +29,8 @@
* [TODO: Adding Support for New Platforms](docs/angr-bf.md)
* [Examples](docs/examples.md)
* [FAQ](docs/faq.md)
* Appendix
* [List of Claripy operations](docs/appendices/ops.md)
* [List of state options](docs/appendices/options.md)
* [Changelog](CHANGELOG.md)
* [Migrating from angr 6](MIGRATION.md)
42 changes: 42 additions & 0 deletions docs/appendices/ops.md
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,42 @@
# List of Claripy Operations

#### Arithmetic and Logic

| Name | Description | Example |
|------|-------------|---------|
| LShR | Logically shifts an expression to the right. (the default shifts are arithmetic) | `x.LShR(10)` |
| RotateLeft | Rotates an expression left | `x.RotateLeft(8)` |
| RotateRight | Rotates an expression right | `x.RotateRight(8)` |
| And | Logical And (on boolean expressions) | `solver.And(x == y, x > 0)` |
| Or | Logical Or (on boolean expressions) | `solver.Or(x == y, y < 10)` |
| Not | Logical Not (on a boolean expression) | `solver.Not(x == y)` is the same as `x != y` |
| If | An If-then-else | Choose the maximum of two expressions: `solver.If(x > y, x, y)` |
| ULE | Unsigned less than or equal to | Check if x is less than or equal to y: `x.ULE(y)` |
| ULT | Unsigned less than | Check if x is less than y: `x.ULT(y)` |
| UGE | Unsigned greater than or equal to | Check if x is greater than or equal to y: `x.UGE(y)` |
| UGT | Unsigned greater than | Check if x is greater than y: `x.UGT(y)` |
| SLE | Signed less than or equal to | Check if x is less than or equal to y: `x.SLE(y)` |
| SLT | Signed less than | Check if x is less than y: `x.SLT(y)` |
| SGE | Signed greater than or equal to | Check if x is greater than or equal to y: `x.SGE(y)` |
| SGT | Signed greater than | Check if x is greater than y: `x.SGT(y)` |

TODO: Add the floating point ops

#### Bitvector Manipulation

| Name | Description | Example |
|------|-------------|---------|
| SignExt | Pad a bitvector on the left with `n` sign bits | `x.sign_extend(n)` |
| ZeroExt | Pad a bitvector on the left with `n` zero bits | `x.zero_extend(n)` |
| Extract | Extracts the given bits (zero-indexed from the *right*, inclusive) from an expression. | Extract the least significant byte of x: `x[7:0]` |
| Concat | Concatenates any number of expressions together into a new expression. | `x.concat(y, ...)` |

#### Extra Functionality

There's a bunch of prepackaged behavior that you *could* implement by analyzing the ASTs and composing sets of operations, but here's an easier way to do it:

- You can chop a bitvector into a list of chunks of `n` bits with `val.chop(n)`
- You can endian-reverse a bitvector with `x.reversed`
- You can get the width of a bitvector in bits with `val.length`
- You can test if an AST has any symbolic components with `val.symbolic`
- You can get a set of the names of all the symbolic variables implicated in the construction of an AST with `val.variables`
141 changes: 141 additions & 0 deletions docs/appendices/options.md
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,141 @@
# List of State Options

#### State Modes

These may be enabled by passing `mode=xxx` to a state constructor.

| Mode name | Description |
|-----------|-------------|
| `symbolic` | The default mode. Useful for most emulation and analysis tasks. |
| `symbolic_approximating` | Symbolic mode, but enables approximations for constraint solving. |
| `static` | A preset useful for static analysis. The memory model becomes an abstract region-mapping system, "fake return" successors skipping calls are added, and more.
| `fastpath` | A preset for extremely lightweight static analysis. Executing will skip all intensive processing to give a quick view of the behavior of code.
| `tracing` | A preset for attempting to execute concretely through a program with a given input. Enables unicorn, enables resilience options, and will attempt to emulate access violations correctly.

#### Option Sets

These are sets of options, found as `angr.options.xxx`.

| Set name | Description |
|----------|-------------|
| `common_options` | Options necessary for basic execution |
| `symbolic` | Options necessary for basic symbolic execution |
| `resilience` | Options that harden angr's emulation against unsupported operations, attempting to carry on by treating the result as an unconstrained symbolic value and logging the occasion to `state.history.events`. |
| `refs` | Options that cause angr to keep a log of all the memory, register, and temporary references complete with dependency information in `history.actions`. This option consumes a lot of memory, so be careful! |
| `approximation` | Options that enable approximations of constraint solves via value-set analysis instead of calling into z3 |
| `simplification` | Options that cause data to be run through z3's simplifiers before it reaches memory or register storage |
| `unicorn` | Options that enable the unicorn engine for executing on concrete data |

#### Options

These are individual option objects, found as `angr.options.XXX`.

| Option name | Description | Sets | Modes | Implicit adds |
|-------------|-------------|-------|------|---------------|
| `ABSTRACT_MEMORY` | Use `SimAbstractMemory` to model memory as discrete regions | | `static` | |
| `ABSTRACT_SOLVER` | Allow splitting constraint sets during simplification | | `static` | |
| `ACTION_DEPS` | Track dependencies in SimActions | | | |
| `APPROXIMATE_GUARDS` | Use VSA when evaluating guard conditions | | | |
| `APPROXIMATE_MEMORY_INDICES` | Use VSA when evaluating memory indices | `approximation` | `symbolic_approximating` | |
| `APPROXIMATE_MEMORY_SIZES` | Use VSA when evaluating memory load/store sizes | `approximation` | `symbolic_approximating` | |
| `APPROXIMATE_SATISFIABILITY` | Use VSA when evaluating state satisfiability | `approximation` | `symbolic_approximating` | |
| `AST_DEPS` | Enables dependency tracking for all claripy ASTs | | | During execution |
| `AUTO_REFS` | An internal option used to track dependencies in SimProcedures | | | During execution |
| `AVOID_MULTIVALUED_READS` | Return a symbolic value without touching memory for any read that has a symbolic address | | `fastpath` | |
| `AVOID_MULTIVALUED_WRITES` | Do not perfrom any write that has a symbolic address | | `fastpath` | |
| `BEST_EFFORT_MEMORY_STORING` | Handle huge writes of symbolic size by pretending they are actually smaller | | `static`, `fastpath` | |
| `BLOCK_SCOPE_CONSTRAINTS` | Clear the constraint list at the end of each block | | `static` | |
| `BREAK_SIRSB_END` | Debug: trigger a breakpoint at the end of each block | | | |
| `BREAK_SIRSB_START` | Debug: trigger a breakpoint at the start of each block | | | |
| `BREAK_SIRSTMT_END` | Debug: trigger a breakpoint at the end of each IR statement | | | |
| `BREAK_SIRSTMT_START` | Debug: trigger a breakpoint at the start of each IR statement | | | |
| `BYPASS_ERRORED_IRCCALL` | Treat clean helpers that fail with errors as returning unconstrained symbolic values | `resilience` | `fastpath`, `tracing` | |
| `BYPASS_ERRORED_IROP` | Treat operations that fail with errors as returning unconstrained symbolic values | `resilience` | `fastpath`, `tracing` | |
| `BYPASS_UNSUPPORTED_IRCCALL` | Treat unsupported clean helpers as returning unconstrained symbolic values | `resilience` | `fastpath`, `tracing` | |
| `BYPASS_UNSUPPORTED_IRDIRTY` | Treat unsupported dirty helpers as returning unconstrained symbolic values | `resilience` | `fastpath`, `tracing` | |
| `BYPASS_UNSUPPORTED_IREXPR` | Treat unsupported IR expressions as returning unconstrained symbolic values | `resilience` | `fastpath`, `tracing` | |
| `BYPASS_UNSUPPORTED_IROP` | Treat unsupported operations as returning unconstrained symbolic values | `resilience` | `fastpath`, `tracing` | |
| `BYPASS_UNSUPPORTED_IRSTMT` | Treat unsupported IR statements as returning unconstrained symbolic values | `resilience` | `fastpath`, `tracing` | |
| `BYPASS_UNSUPPORTED_SYSCALL` | Treat unsupported syscalls as returning unconstrained symbolic values | `resilience` | `fastpath`, `tracing` | |
| `BYPASS_VERITESTING_EXCEPTIONS` | Discard emulation errors during veritesting | `resilience` | `fastpath`, `tracing` | |
| `CACHELESS_SOLVER` | enable `SolverCacheless` | | | |
| `CALLLESS` | Emulate call instructions as an unconstraining of the return value register | | | |
| `CGC_ENFORCE_FD` | CGC: make sure all reads and writes go to stdin and stdout, respectively | | | |
| `CGC_NON_BLOCKING_FDS` | CGC: always report "data available" in fdwait | | | |
| `CGC_NO_SYMBOLIC_RECEIVE_LENGTH` | CGC: always read the maximum amount of data requested in the receive syscall | | | |
| `COMPOSITE_SOLVER` | Enable `SolverComposite` for independent constraint set optimization | `symbolic` | all except `static` | |
| `CONCRETIZE` | Concretize all symbolic expressions encountered during emulation | | | |
| `CONCRETIZE_SYMBOLIC_FILE_READ_SIZES` | Concreteize the sizes of file reads | | | |
| `CONCRETIZE_SYMBOLIC_WRITE_SIZES` | Concretize the sizes of symbolic writes to memory | | | |
| `CONSERVATIVE_READ_STRATEGY` | Do not use SimConcretizationStrategyAny for reads; in case of read address concretization failures, return an unconstrained symbolic value | | | |
| `CONSERVATIVE_WRITE_STRATEGY` | Do not use SimConcretizationStrategyAny for writes; in case of write address concretization failures, treat the store as a no-op | | | |
| `CONSTRAINT_TRACKING_IN_SOLVER` | Set `track=True` for making claripy Solvers; enable use of `unsat_core` | | | |
| `COW_STATES` | Copy states instead of mutating the initial state directly | `common_options` | all | |
| `DOWNSIZE_Z3` | Downsize the claripy solver whenever possible to save memory | | | |
| `DO_CCALLS` | Perform IR clean calls | `symbolic` | all except `fastpath` | |
| `DO_GETS` | Perform IR register reads | `common_options` | all | |
| `DO_LOADS` | Perform IR memory loads | `common_options` | all | |
| `DO_OPS` | Perform IR computation operations | `common_options` | all | |
| `DO_PUTS` | Perform IR register writes | `common_options` | all | |
| `DO_RET_EMULATION` | For each `Ijk_Call` successor, add a corresponding `Ijk_FakeRet` successor | | `static`, `fastpath` | |
| `DO_STORES` | Perform IR memory stores | `common_options` | all | |
| `EFFICIENT_STATE_MERGING` | Keep in memory any state that might be a common ancestor in a merge | | | Veritesting |
| `ENABLE_NX` | When in conjunction with `STRICT_PAGE_ACCESS`, raise a SimSegfaultException on executing non-executable memory | | | Automatically if supported |
| `EXCEPTION_HANDLING` | Ask all SimExceptions raised during execution to be handled by the SimOS | | `tracing` | |
| `FAST_MEMORY` | Use `SimFastMemory` for memory storage | | | |
| `FAST_REGISTERS` | Use `SimFastMemory` for register storage | | `fastpath` | |
| `INITIALIZE_ZERO_REGISTERS` | Treat the initial value of registers as zero instead of unconstrained symbolic | `unicorn` | `tracing` | |
| `INSTRUCTION_SCOPE_CONSTRAINTS` | Clear the constraint list at the end of each instruction | | | |
| `KEEP_IP_SYMBOLIC` | Don't try to concretize successor states with symbolic instruction pointers | | | |
| `KEEP_MEMORY_READS_DISCRETE` | In abstract memory, handle failed loads by returning a DCIS? | | | |
| `LAZY_SOLVES` | Don't check satisfiability until absolutely necessary | | | |
| `MEMORY_SYMBOLIC_BYTES_MAP` | Maintain a mapping of symbolic variable to which memory address it "really" corresponds to, at the paged memory level? | | | |
| `NO_SYMBOLIC_JUMP_RESOLUTION` | Do not attempt to flatten symbolic-ip successors into discrete targets | | `fastpath` | |
| `NO_SYMBOLIC_SYSCALL_RESOLUTION` | Do not attempt to flatten symbolic-syscall-number successors into discrete targets | | `fastpath` | |
| `OPTIMIZE_IR` | Use LibVEX's optimization | `common_options` | all | |
| `REGION_MAPPING` | Maintain a mapping of symbolic variable to which memory region it corresponds to, at the abstract memory level | | `static` | |
| `REPLACEMENT_SOLVER` | Enable `SolverReplacement` | | | |
| `REVERSE_MEMORY_HASH_MAP` | Maintain a mapping from AST hash to which addresses it is present in | | | |
| `REVERSE_MEMORY_NAME_MAP` | Maintain a mapping from symbolic variable name to which addresses it is present in, required for `memory.replace_all` | | `static` | |
| `SIMPLIFY_CONSTRAINTS` | Run added constraints through z3's simplifcation | | | |
| `SIMPLIFY_EXIT_GUARD` | Run branch guards through z3's simplification | | | |
| `SIMPLIFY_EXIT_STATE` | Perform simplification on all successor states generated | | | |
| `SIMPLIFY_EXIT_TARGET` | Run jump/call/branch targets through z3's simplification | | | |
| `SIMPLIFY_EXPRS` | Run the results of IR expressions through z3's simplification | | | |
| `SIMPLIFY_MEMORY_READS` | Run the results of memory reads through z3's simplification | | | |
| `SIMPLIFY_MEMORY_WRITES` | Run values stored to memory through z3's simplification | `simplification`, `common_options` | `symbolic`, `symbolic_approximating`, `tracing` | |
| `SIMPLIFY_REGISTER_READS` | Run values read from registers through z3's simplification | | | |
| `SIMPLIFY_REGISTER_WRITES` | Run values written to registers through z3's simplification | `simplification`, `common_options` | `symbolic`, `symbolic_approximating`, `tracing` | |
| `SIMPLIFY_RETS` | Run values returned from SimProcedures through z3's simplification | | | |
| `STRICT_PAGE_ACCESS` | Raise a SimSegfaultException when attempting to interact with memory in a way not permitted by the current permissions | | `tracing` | |
| `SUPER_FASTPATH` | Only execute the last four instructions of each block | | | |
| `SUPPORT_FLOATING_POINT` | When disabled, throw an UnsupportedIROpError when encountering floating point operations | `common_options` | all | |
| `SYMBOLIC` | Enable constraint solving? | `symbolic` | `symbolic`, `symbolic_approximating`, `fastpath` | |
| `SYMBOLIC_INITIAL_VALUES` | make `state.solver.Unconstrained` return a symbolic value instead of zero | `symbolic` | all | |
| `SYMBOLIC_TEMPS` | Treat each IR temporary as a symbolic variable; treat stores to them as constraint addition | | | |
| `SYMBOLIC_WRITE_ADDRESSES` | Allow writes with symbolic addresses to be processed by concretization strategies; when disabled, only allow for variables annotated with the "multiwrite" annotation | | | |
| `TRACK_CONSTRAINTS` | When disabled, don't keep any constraints added to the state | `symbolic` | all | |
| `TRACK_CONSTRAINT_ACTIONS` | Keep a SimAction for each constraint added | `refs` | | |
| `TRACK_JMP_ACTIONS` | Keep a SimAction for each jump or branch | `refs` | | |
| `TRACK_MEMORY_ACTIONS` | Keep a SimAction for each memory read and write | `refs` | | |
| `TRACK_MEMORY_MAPPING` | Keep track of which pages are mapped into memory and which are not | `common_options` | all | |
| `TRACK_OP_ACTIONS` | Keep a SimAction for each IR operation | | `fastpath` | |
| `TRACK_REGISTER_ACTIONS` | Keep a SimAction for each register read and write | `refs` | | |
| `TRACK_SOLVER_VARIABLES` | Maintain a listing of all the variables in all the constraints in the solver | | | |
| `TRACK_TMP_ACTIONS` | Keep a SimAction for each temporary variable read and write | `refs` | | |
| `TRUE_RET_EMULATION_GUARD` | With `DO_RET_EMULATION`, add fake returns with guard condition true instead of false | | `static` | |
| `UNDER_CONSTRAINED_SYMEXEC` | Enable under-constrained symbolic execution | | | |
| `UNICORN` | Use unicorn engine to execute symbolically when data is concrete | `unicorn` | `tracing` | Oppologist |
| `UNICORN_AGGRESSIVE_CONCRETIZATION` | Concretize any register variable unicorn tries to access | | | Oppologist |
| `UNICORN_HANDLE_TRANSMIT_SYSCALL` | CGC: handle the transmit syscall without leaving unicorn | `unicorn` | `tracing` | |
| `UNICORN_SYM_REGS_SUPPORT` | Attempt to stay in unicorn even in the presence of symbolic registers by checking that the tainted registers are unused at every step | `unicorn` | `tracing` | |
| `UNICORN_THRESHOLD_CONCRETIZATION` | Concretize variables if they prevent unicorn from executing too often | | | |
| `UNICORN_TRACK_BBL_ADDRS` | Keep `state.history.bbl_addrs` up to date when using unicorn | `unicorn` | `tracing` | |
| `UNICORN_TRACK_STACK_POINTERS` | Track a list of the stack pointer's value at each block in `state.scratch.stack_pointer_list` | `unicorn` | | |
| `UNICORN_ZEROPAGE_GUARD` | Prevent unicorn from mapping the zero page into memory | | | |
| `UNINITIALIZED_ACCESS_AWARENESS` | Broken/unused? | | | |
| `UNSUPPORTED_BYPASS_ZERO_DEFAULT` | When using the resilience options, return zero instead of an unconstrained symbol | | | |
| `USE_SIMPLIFIED_CCALLS` | Use a "simplified" set of ccalls optimized for specific cases | | `static` | |
| `USE_SYSTEM_TIMES` | In library functions and syscalls and hardware instructions accessing clock data, retrieve the real value from the host system. | | `tracing` | |
| `VALIDATE_APPROXIMATIONS` | Debug: When performing approximations, ensure that the approximation is sound by calling into z3 | | | |
| `ZERO_FILL_UNCONSTRAINED_MEMORY` | Make the value of memory read from an uninitialized address zero instead of an unconstrained symbol | | `tracing` | |
Loading

0 comments on commit fa3d78f

Please sign in to comment.