Thoth (pronounced "taut" or "toss") is a Cairo/Starknet security toolkit including analyzers, disassemblers & decompilers written in Python 3. Thoth's features include the generation of the call graph, the control-flow graph (CFG) and the data-flow graph for a given Sierra file or Cairo/Starknet compilation artifact. It also includes some really advanced tools like a Symbolic execution engine and Symbolic bounded model checker.
Learn more about Thoth internals here: Demo video, StarkNetCC 2022 slides
- Remote & Local: Thoth can both analyze contracts deployed on Mainnet/Goerli and compiled locally on your machine.
- Decompiler: Thoth can convert assembly into decompiled code with SSA (Static Single Assignment)
- Call Flow analysis: Thoth can generate a Call Flow Graph
- Static analysis: Thoth can run various analyzers of different types (security/optimization/analytics) on the contract
- Symbolic execution: Thoth can use the symbolic execution to find the right variables values to get through a specific path in a function and also automatically generate test cases for a function.
- Data Flow analysis: Thoth can generate a Data Flow Graph (DFG) for each function
- Disassembler: Thoth can translate bytecode into assembly representation
- Control Flow analysis: Thoth can generate a Control Flow Graph (CFG)
- Cairo Fuzzer inputs generation: Thoth can generate inputs for the Cairo fuzzer
- Sierra files analysis : Thoth can analyze Sierra files
- Sierra files symbolic execution : Thoth allows symbolic execution on sierra files
- Symbolic bounded model checker : Thoth can be used as a Symbolic bounded model checker
sudo apt install graphviz
git clone https://github.com/FuzzingLabs/thoth && cd thoth
pip install .
thoth -h
# Remote contrat deployed on starknet (mainnet/goerli)
thoth remote --address 0x0323D18E2401DDe9aFFE1908e9863cbfE523791690F32a2ff6aa66959841D31D --network mainnet -d
# Local contract compiled locally (JSON file)
thoth local tests/json_files/cairo_0/cairo_test_addition_if.json -dExample 1 with strings:
source code
decompiler code
source code
decompiler code
The call flow graph represents calling relationships between functions of the contract. We tried to provide a maximum of information, such as the entry-point functions, the imports, decorators, etc.
thoth local tests/json_files/cairo_0/cairo_array_sum.json -call -view
# For a specific output format (pdf/svg/png):
thoth local tests/json_files/cairo_0/cairo_array_sum.json -call -view -format pngThe output file (pdf/svg/png) and the dot file are inside the output-callgraph folder.
If needed, you can also visualize dot files online using this website. The legend can be found here.
A more complexe callgraph:
The static analysis is performed using analyzers which can be either informative or security/optimization related.
| Analyzer | Command-Line argument | Description | Impact | Precision | Category | Bytecode | Sierra |
|---|---|---|---|---|---|---|---|
| ERC20 | erc20 |
Detect if a contract is an ERC20 Token | Informational | High | Analytics | ✔️ | ❌ |
| ERC721 | erc721 |
Detect if a contract is an ERC721 Token | Informational | High | Analytics | ✔️ | ❌ |
| Strings | strings |
Detect strings inside a contract | Informational | High | Analytics | ✔️ | ✔️ |
| Functions | functions |
Retrieve informations about the contract's functions | Informational | High | Analytics | ✔️ | ✔️ |
| Statistics | statistics |
General statistics about the contract | Informational | High | Analytics | ✔️ | ✔️ |
| Test cases generator | tests |
Automatically generate test cases for each function of the contract | Informational | High | Analytics | ✔️ | ❌ |
| Assignations | assignations |
List of variables assignations | Informational | High | Optimization | ✔️ | ❌ |
| Integer overflow | int_overflow |
Detect direct integer overflow/underflow | High (direct) / Medium (indirect) | Medium | Security | ✔️ | ✔️ |
| Function naming | function_naming |
Detect functions names that are not in snake case | Informational | High | Security | ✔️ | ❌ |
| Variable naming | variable_naming |
Detect variables names that are not in snake case | Informational | High | Security | ✔️ | ❌ |
| Delegate calls detector | delegate_call |
Detect delegate calls | Informational | High | Security | ❌ | ✔️ |
| Dead code detector | dead_code |
Detect dead code | Informational | High | Security | ❌ | ✔️ |
| Unused arguments detector | unused_arguments |
Detect unused arguments | Informational | High | Security | ❌ | ✔️ |
| User defined function call detector | user_defined |
Detect calls of user defined functions | Informational | High | Security | ❌ | ✔️ |
thoth local tests/json_files/cairo_0/cairo_array_sum.json -athoth local tests/json_files/cairo_0/cairo_array_sum.json -a erc20 erc721thoth local tests/json_files/cairo_0/cairo_array_sum.json -a security
thoth local tests/json_files/cairo_0/cairo_array_sum.json -a optimization
thoth local tests/json_files/cairo_0/cairo_array_sum.json -a analyticsthoth local tests/json_files/cairo_0/cairo_array_sum.json --analyzers-help
You can find a detailed documentation for the symbolic execution here.
thoth local tests/json_files/cairo_0/cairo_double_function_and_if.json -dfg -view
# For a specific output format (pdf/svg/png):
thoth local tests/json_files/cairo_0/cairo_double_function_and_if.json -dfg -view -format png
# For tainting visualization:
thoth remote --address 0x069e40D2c88F479c86aB3E379Da958c75724eC1d5b7285E14e7bA44FD2f746A8 -n mainnet -dfg -view --taintThe output file (pdf/svg/png) and the dot file are inside the output-dfg folder.
# Remote contrat deployed on starknet (mainnet/goerli)
thoth remote --address 0x0323D18E2401DDe9aFFE1908e9863cbfE523791690F32a2ff6aa66959841D31D --network mainnet -b
# Local contract compiled locally (JSON file)
thoth local tests/json_files/cairo_0/cairo_array_sum.json -b
# To get a pretty colored version:
thoth local tests/json_files/cairo_0/cairo_array_sum.json -b -color
# To get a verbose version with more details about decoded bytecodes:
thoth local tests/json_files/cairo_0/cairo_array_sum.json -vvv
thoth local tests/json_files/cairo_0/cairo_double_function_and_if.json -cfg -view
# For a specific function:
thoth local tests/json_files/cairo_0/cairo_double_function_and_if.json -cfg -view -function "__main__.main"
# For a specific output format (pdf/svg/png):
thoth local tests/json_files/cairo_0/cairo_double_function_and_if.json -cfg -view -format pngThe output file (pdf/svg/png) and the dot file are inside the output-cfg folder.
You can generate inputs for the Cairo fuzzer using this command
thoth local ./tests/json_files/cairo_0/cairo_test_symbolic_execution_2.json -a fuzzer
Thoth supports cairo and starknet compilation artifact (json file) generated after compilation using cairo-compile or starknet-compile. Thoth also supports the json file returned by: starknet get_full_contract.
python3 tests/test.py
# Install sphinx
apt-get install python3-sphinx
#Create the docs folder
mkdir docs & cd docs
#Init the folder
sphinx-quickstart docs
#Modify the `conf.py` file by adding
import thoth
#Generate the .rst files before the .html files
sphinx-apidoc -f -o . ..
#Generate the .html files
make html
#Run a python http server
cd _build/html; python3 -m http.serverFirst, verify that your JSON is correct and that it contains a data section. Second, verify that your JSON is not a contract interface. Finally, it is possible that your contract does not generate bytecodes, for example:
%lang starknet
from starkware.cairo.common.cairo_builtins import HashBuiltin
@storage_var
func balance() -> (res : felt):
endThoth is inspired by a lot of different security tools developed by friends such as: Octopus, Slither, Mythril, etc.
Thoth is licensed and distributed under the AGPLv3 license. Contact us if you're looking for an exception to the terms.