The aim of this tutorial is to show how to use Manticore to automatically find bugs in smart contracts.
The first part introduces a set of the basic features of Manticore: running under Manticore and manipulating smart contracts through API, getting throwing path, adding constraints. The second part is exercise to solve.
Table of contents:
- Installation
- Introduction to symbolic execution: Brief introduction to symbolic execution
- Running under Manticore: How to use Manticore's API to run a contract
- Getting throwing paths: How to use Manticore's API to get specific paths
- Adding constraints: How to use Manticore's API to add paths' constraints
- Exercises
Join the team on Slack at: https://slack.empirehacking.nyc/ #ethereum, #manticore
Manticore requires >= python 3.6. It can be installed through pip or using docker.
docker pull trailofbits/eth-security-toolbox
docker run -it -v "$PWD":/home/training trailofbits/eth-security-toolbox
The last command runs eth-security-toolbox in a docker that has access to your current directory. You can change the files from your host, and run the tools on the files from the docker
Inside docker, run:
solc-select 0.5.11
cd /home/trufflecon/
pip3 install --user manticore
solc 0.5.11 is recommended.
To run a python script with python 3:
python3 script.py