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 -d

Example 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 png

The 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.

thoth local tests/json_files/cairo_0/cairo_array_sum.json -a

thoth local tests/json_files/cairo_0/cairo_array_sum.json -a erc20 erc721

thoth 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 analytics

thoth 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 --taint

The 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 png

The 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.server

First, 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):
end

Thoth 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.