Thoth, the Cairo/Starknet security toolkit (analyzer, disassembler and decompiler)

[!IMPORTANT]
This repository is no longer maintained. If you have any questions or need further assistance, please contact FuzzingLabs.

<img src ="https://img.shields.io/badge/python-3.10-blue.svg"/>

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

Features

• 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
• Use it with a Scarb project : Thoth can be used in a project created with the Scarb toolchain

Installation

sudo apt install graphviz
git clone https://github.com/FuzzingLabs/thoth && cd thoth
pip install .
thoth -h

Decompile the contract's compilation artifact (JSON)

# 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:

<p align="center"> <b> source code </b></br> <img src="/doc/images/thoth/thoth_decompile_sourcecode.png"/></br> <b> decompiler code </b></br> <img src="/doc/images/thoth/thoth_decompile.png"/></br> </p> Example 2 with function call: <p align="center"> <b> source code </b></br> <img src="/doc/images/thoth/thoth_decompile_sourcecode_2.png"/></br> <b> decompiler code </b></br> <img src="/doc/images/thoth/thoth_decompile_2.png"/></br> </p>

Print the contract's call graph

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.

<p align="center"> <img src="/doc/images/thoth/thoth_callgraph_simple.png"/> </p>

A more complexe callgraph:

<p align="center"> <img src="/doc/images/thoth/starknet_get_full_contract_l2_dai_bridge.gv.png"/> </p>

Run the static analysis

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|❌|✔️|

Run all the analyzers

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

Selects which analyzers to run

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

Only run a specific category of analyzers

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

Print a list of all the available analyzers

thoth local tests/json_files/cairo_0/cairo_array_sum.json --analyzers-help

Use the symbolic execution

You can find a detailed documentation for the symbolic execution here.

Print the contract's data-flow graph (DFG)

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.

<p align="center"> <img src="/doc/images/thoth/thoth_dataflow_graph.png"/> </p> <p align="center"> <img src="/doc/images/thoth/thoth_dfg_tainting.png"/> </p>

Disassemble the contract's compilation artifact (JSON)

# 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

<p align="center"> <img src="/doc/images/thoth/thoth_disas_color.png"/> </p>

Print the contract's control-flow graph (CFG)

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.

<p align="center"> <img src="/doc/images/thoth/cairo_double_function_and_if_cfg.png"/> </p>

Generate inputs for the Cairo fuzzer

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

Use it with a Scarb project

Add these lines to your Scarb.toml :

[[target.starknet-contract]]
sierra = true
casm = true

Then build the project using Scarb :

scarb build

You can now run Thoth with the --scarb flag :

// Run the disassembler
thoth local --scarb -b

// Run the analyzer
thoth local --scarb -a

// Generate the control-flow graph
thoth local --scarb --cfg

// Gene