From 03c6098e2198aff2518bf8409ab026c2072331b3 Mon Sep 17 00:00:00 2001 From: degrigis Date: Sat, 16 Dec 2023 15:59:52 -0800 Subject: [PATCH] few more things Signed-off-by: degrigis --- docs/docs/advanced.md | 7 +++++-- docs/docs/core.md | 27 +++++++++++++++++++++++++-- docs/docs/options.md | 22 ++++++++++++++++++++++ 3 files changed, 52 insertions(+), 4 deletions(-) diff --git a/docs/docs/advanced.md b/docs/docs/advanced.md index 76f062d..fbe42a6 100644 --- a/docs/docs/advanced.md +++ b/docs/docs/advanced.md @@ -1,14 +1,17 @@ # 🚀 Advanced Topics +# State Plugins # Memory Model +# Partial Concrete Storage +# Multi-Transactions Execution -# Chain Together Contracts Execution +# Keccak256 +# External Calls -# State Plugins \ No newline at end of file diff --git a/docs/docs/core.md b/docs/docs/core.md index 5bb9105..93bc7ba 100644 --- a/docs/docs/core.md +++ b/docs/docs/core.md @@ -127,9 +127,32 @@ A state offers many API for its inspection: Symbolic execution is the process of progressing SimState(s) and propagating the symbolic variables according to the program's execution. Imagine, for instance, that the condition of a `JUMPI` contains a symbolic variable X. If the condition checks for `X != 0`, and the constraints over the variable X make it possible for `X != 0` and `X == 0`, greed will create two different State(s), one at the location specified by the JUMPI (adding a constraint of `X != 0` to the state), and one at the fallthrough (adding a constraint of `X == 0`). - +To begin symbolic execution you need to instantiate a `Simulation Manager`. ### Simulation Manager -The simulation manager is a concept borrowed from angr. It is the starting point for beginning symbolic execution and orchestrates the progression of the SimState(s) according to the specified `Exploration Techniques`. +The simulation manager is a concept borrowed from angr. It is the starting point for beginning symbolic execution and it is used to orchestrate the progression of the SimState(s) according to the employed `Exploration Techniques`. +Exploration Techniques are used to specify a strategy to explore the states of the program. For instance, an exploration technique can be the classic BFS, or a DFS, or more complicated strategies such as Directed Search etc... + +You can instantiate a simulation manager via the Factory in this way: + +```python +>>> simgr = proj.factory.simgr(entry_state=entry_state) +``` + +By default, the employed exploration technique will be B(reath)F(irst)S(earch). You can change this behavior by installing a new exploration technique that follows the `Exploration Technique` object interface. e.g., : + +```python +>>> from greed.exploration_techniques import ExplorationTechnique, DirectedSearch +>>> directed_search = DirectedSearch(proj.statement_at['0x1e']) +>>> simgr.use_technique(directed_search) +``` + +Finally, to start the exploration: + +```python +>>> simgr.run() +``` + +The simulation manager operates using `stashes`. A stash is a "bucket" of SimStates generated by the simulation manager during symbolic execution. ### Solver diff --git a/docs/docs/options.md b/docs/docs/options.md index e69de29..9734783 100644 --- a/docs/docs/options.md +++ b/docs/docs/options.md @@ -0,0 +1,22 @@ +# 🕹ī¸ Options + +greed supports many option to tweak the behavior of symbolic execution. +These global options should be activated or de-activated before creating an entry state. + +| Option Name | Default | Desc | +|-------------------|----------|----------| +| options.GREEDY_SHA | False | calculate the result of the `KECCAK256` whenever the input buffer is fully concrete and has one solution | +| options.LAZY_SOLVES | False | check_sat() every time a new SimState is generated | + + + +options.GREEDY_SHA = True +options.LAZY_SOLVES = False +options.STATE_INSPECT = False +options.MAX_SHA_SIZE = 300 +options.OPTIMISTIC_CALL_RESULTS = True +options.DEFAULT_EXTCODESIZE = True +options.DEFAULT_CREATE2_RESULT_ADDRESS = True +options.DEFAULT_CREATE_RESULT_ADDRESS = True +options.MATH_CONCRETIZE_SYMBOLIC_EXP_EXP = True +options.MATH_CONCRETIZE_SYMBOLIC_EXP_BASE = True \ No newline at end of file