Symbolic execution toolkit for Ethereum smart-contracts
Project description
# Optik
Optik is a set of symbolic execution tools that assist smart contract fuzzers, letting them run in a _hybrid_ mode. Optik couples [Echidna](https://github.com/crytic/echidna), our smart contract fuzzer, with the [Maat](https://github.com/trailofbits/maat) symbolic executor that replays the fuzzing corpus and extends it with new inputs that increase coverage.
#### Current limitations
Optik is a work in progress and should not be used for real audits yet. Current limitations include:
Symbolic KECCAK hashes are not supported
CREATE2, CALLCODE, and DELEGATECALL are not yet supported
Gas is not taken into account
Some echidna options are not yet supported (see hybrid-echidna -h)
## Hybrid Echidna
<p align=”center” > <img width=”80%” src=”.resources/hybrid_echidna.png”/> <br> </p>
Optik allows to run the [Echidna](https://github.com/crytic/echidna) smart-contract fuzzer in _hybrid_ mode. It basically couples Echidna with the [Maat](https://github.com/trailofbits/maat) symbolic executor that replays the Echidna corpus and extends it with new inputs that increase coverage.
hybrid-echidna starts with several <i>incremental seeding</i> steps, where it seeds the corpus with short transactions sequences obtained by [Slither](https://github.com/crytic/slither)’s dataflow analysis, and uses symbolic execution more intensely to solve new inputs. The sequence length is incremented at each seeding step. Once it reaches a certain length threshold, hybrid-echidna falls back into its normal mode, starts to limit the number of symbolic inputs to solve, and stops using dataflow analysis for seeding the corpus.
### Usage
Hybrid echidna can be used seamlessly in place of regular Echidna by replacing echidna-test with hybrid-echidna in your Echidna command line. For example:
` hybrid-echidna MyContract.sol --test-mode assertion --corpus-dir /tmp/test --contract MyContract `
Additionnal options are available in hybrid mode to control hybrid-echidna’s behaviour:
–max-iters: maximum number of fuzzing iterations to perform (one iteration is one Echidna campaign + one symbolic executor run on the corpus)
–solver-timeout: maximum time in milliseconds to spend solving each possible new input
–incremental-threshold: number of initial incremental seeding steps to perform
–no-incremental: skip initial incremental seeding
–cov-mode: type of coverage to increase when solving new inputs. Most coverage modes are implemented for experimental purposes. Unless you are developing/hacking on Optik, we recommend to keep the default mode
Debugging, logging and terminal display:
–debug: add debugging information to the log output
–logs: write logs to a given file (or stdout)
–no-display: disable the graphical terminal display
## Installation
For a quick installation, run:
`console python3 -m pip install optik-tools `
To keep up with the latest features and fixes, install Optik from its master branch:
`console git clone https://github.com/crytic/optik && cd optik python3 -m pip install . `
You can also run it from Docker:
`console git clone https://github.com/crytic/optik && cd optik docker build -t crytic/optik . docker run -it --rm --mount type=bind,source="$(pwd)",target=/workdir crytic/optik # This runs the Docker container, mounting the local directory into /workdir `
Project details
Release history Release notifications | RSS feed
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.
Source Distribution
Built Distribution
Hashes for optik_tools-0.0.2-py3-none-any.whl
Algorithm | Hash digest | |
---|---|---|
SHA256 | c245bfdfb4bb7c3f16a19e4b4e4c33ebeafbe5858f67f9c708e96c9c73d08a72 |
|
MD5 | a793a41f840279e79c5a6508a4bd460d |
|
BLAKE2b-256 | 884482354cf7cac740f51d018b5b478e94063dfb6058c824e0c447e33a7e501f |