From b2893fc18c6eafcf3baa540a9eaa5c45f2533328 Mon Sep 17 00:00:00 2001 From: degrigis Date: Sun, 17 Dec 2023 17:43:25 -0800 Subject: [PATCH] added options Signed-off-by: degrigis --- docs/docs/advanced.md | 2 +- docs/docs/api.md | 0 docs/docs/options.md | 20 +++++++++++++++++++- docs/mkdocs.yml | 2 +- 4 files changed, 21 insertions(+), 3 deletions(-) create mode 100644 docs/docs/api.md diff --git a/docs/docs/advanced.md b/docs/docs/advanced.md index eb7948d..afa38b5 100644 --- a/docs/docs/advanced.md +++ b/docs/docs/advanced.md @@ -76,7 +76,7 @@ Practically, we handle the `SHA3` operation with a twofold strategy. First, duri **(1)** During symbolic execution, first we register all the information regarding the sha operation in the `sha_observed` attribute of a SimState (i.e., the snapshot of the state's memory at the SHA operation, the offset at which the input buffer is located, and the size of the requested operation). Then, in case the option `GREEDY_SHA` is active, we calculated (on the fly) the Keccak256 of fully concrete input buffers (or, symbolic buffers with one possible solution) and we assign this value to the result virtual registers. If no `GREEDY_SHA` is used (or the input buffer is not concrete), we return a fresh symbolic variable (e.g., ``). Lastly, for every observed sha (i.e., `state.sha_observed`) we [instantiate constraints](https://github.com/ucsb-seclab/greed/blob/main/greed/sha3.py#L44) that encode the equality of the sha fresh symbolic variables whenever the input buffers are the same (i.e., basically encoding that the result of different `SHA3` opcodes that operate on equal input buffers MUST be the same). -**(2)** Whenever an user requires to calculate solutions, e.g.: to synthethize the `CALLDATA` to reach a specific instruction, the first step is to "fix" the value for the input buffers for the observed shas (if any). TODO. +**(2)** Whenever an user requires to calculate solutions for some symbolic variables, e.g.: to synthethize the `CALLDATA` to reach a specific instruction, the first step is to "fix" the value for the input buffers of the observed SHAs (if any). To do that, we provide a "SHA resolution strategy" that fixes the observed SHAs chronologically. Namely, the strategy iterates over all the observed SHAs starting from the earliest, calculate a solution for its input buffer, calculate the correspondent Keccak256, and finally assign the result to the symbolic variable associated to this SHA. Then the process repeat until the latest SHA. Eventually, if it is possible to assign a concrete value to all the observed SHAs, the state is ready to be queried for the satisfiability of any other symbolic variables, e.g., the value the `CALLDATA` needs to assume to reach the current statement. Note that, if it is not possible to find a solution to resolve the SHAs, the state is to be considered unsat (we do not want to do this check ourselves during symbolic execution because this is an expensive check). ## Multi-Transactions Execution diff --git a/docs/docs/api.md b/docs/docs/api.md new file mode 100644 index 0000000..e69de29 diff --git a/docs/docs/options.md b/docs/docs/options.md index 11eec40..22266b1 100644 --- a/docs/docs/options.md +++ b/docs/docs/options.md @@ -3,4 +3,22 @@ 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. -<<<< GENREATE THIS AUTOMATICALL FROM THE OPTIONS.py >>>> \ No newline at end of file +| Option Name | Default | Description | +|----------------------------------------|---------|---------------------------------------------------------------------------------------------------------------------| +| `WEB3_PROVIDER` | http://0.0.0.0:8545 | Web3 provider URI. Used when initializing the partial concrete storage. | +| `LAZY_SOLVES` | False | Indicates whether to check for satisfiability at every fork, affecting exploration speed and state pruning. | +| `GREEDY_SHA` | False | Specifies whether to calculate SHA3 for concrete or single-solution buffers, potentially impacting exploration speed.| +| `SIMGRVIZ` | False | Activates the creation of a graph visualizing the exploration (the SimgrViz Exploration Technique must be also installed| +| `STATE_INSPECT` | False | Activates debugging capabilities through the SimStateInspect plugin (i.e., breakpoints). | +| `MAX_CALLDATA_SIZE` | 256 | Default CALLDATASIZE considered, can be overwritten by the entry_state constructor. | +| `MATH_CONCRETIZE_SYMBOLIC_EXP_EXP` | False | Specifies whether to concretize the exponent of an EXP instruction. | +| `MATH_CONCRETIZE_SYMBOLIC_EXP_BASE` | False | Specifies whether to concretize the base of an EXP instruction. | +| `MATH_MULTIPLY_EXP_THRESHOLD` | 10 | Maximum supported nested multiplications when there is a symbolic base and concrete exponent. | +| `OPTIMISTIC_CALL_RESULTS` | False | Indicates whether to always consider CALLS as succeeded or not. | +| `DEFAULT_EXTCODESIZE` | False | Specifies whether to use a default constant value for EXTCODESIZE. | +| `DEFAULT_CREATE_RESULT_ADDRESS` | False | Specifies whether to use a default constant address when using the CREATE opcode. | +| `DEFAULT_CREATE2_RESULT_ADDRESS` | False | Specifies whether to use a default constant address when using the CREATE2 opcode. | +| `STATE_STOP_AT_ADDCONSTRAINT` | False | Indicates whether to drop a debugging interface every time a constraint is added to the state.| +| `MAX_SHA_SIZE` | 512 | Maximum size of the SHA3 input buffer considered.| +| `SOLVER` | "YICES2" | Default solver (Yices2).| +| `SOLVER_TIMEOUT` | Inf. | Timeout setting for the solver. | diff --git a/docs/mkdocs.yml b/docs/mkdocs.yml index 33cc919..a9ae5bf 100644 --- a/docs/mkdocs.yml +++ b/docs/mkdocs.yml @@ -25,7 +25,7 @@ nav: - Advanced Topics: advanced.md - Options: options.md - Examples: examples.md + - API Reference: api.md - Credits: credits.md - - FAQ: faq.md