Symbolic execution is an essential tool in modern program analysis and vulnerability discovery. Symbolic execution of smart contracts is a developing field, but will most likely be a useful tool for smart contract auditing and vulnerability testing. In this codelab, you will start by setting up
geth, an implementation of an ethereum node as well as Manticore, a Python package supporting the symbolic execution of smart contracts.
You will deploy a Compute Engine instance, install Docker, and run the course's Docker image that contains the
manticore framework and
tmuxto keep sessions persistent in the container and VM instance
sudo apt update sudo apt install -y docker.io sudo usermod -a -G docker $(whoami) newgrp docker
Download and run the custom container (located on Docker Hub as
manticore, along with the Security Innovations CTF levels and skeleton manticore scripts for solving them.
--name=manticoreflag to name your running container (otherwise you'll get a Docker-generated name)
-diflag to start in detached mode
docker run --name=manticore -di wuchangfeng/manticore
Examine the running container and the container's image
CONTAINER ID IMAGE COMMAND CREATED STATUS PORTS NAMES 6aa4ff2c9ebe ...manticore... "/bin/bash" 6 minutes ago Up 2 seconds manticore
REPOSITORY TAG IMAGE ID CREATED SIZE ...manticore... latest a94482ca9403 4 days ago 1.45GB
Stop the container via its name. Note that docker supports command completion that will automatically fill in the name of the container. As we called our container "
manticore", the command is
docker stop manticore
See that it is no longer running via "
docker ps" with the "
-a" flag to list stopped containers
docker ps -a
docker rm manticore". Note that while this removes the container, it does not remove the local container image it was derived from (i.e.
docker rmi wuchangfeng/manticore" after stopping the container
Start the container again via its name, the command is
docker start manticore
Now, execute an interactive shell on the container
docker exec -it manticore /bin/bash
Within the shell running in the container, it may be handy to have multiple sessions. This can be done via
tmux. Click here for a tutorial. You will want to create a tmux session with several terminals. One can be used to run the light node via
geth. One can be used to run an interactive
tmux session when you are done and and reattaching to the tmux session via "
tmuxtips and hotkeys
Here's some quick tips to use tmux easily.
docker exec -it <CONTAINER ID> tmux
docker exec -it <CONTAINER ID> tmux a
docker start <CONTAINER ID>
If you don't exactly remember your container id, you can list all of them with
docker ps -a
To interact with the blockchain, we will instantiate and sync a
geth light node with the ropsten network. The first time this happens, it takes about an hour, but will be much faster on subsequent syncs (assuming you do not delete the container). We want to use the latest version as well. To do this, in the container, perform the following to pull and checkout a recent stable version of
cd go-ethereum git pull git checkout v1.9.6 make
Then, bring up the node:
./build/bin/geth --allow-insecure-unlock --syncmode light --testnet --rpcapi eth,web3,personal --rpc --rpcaddr 127.0.0.1
After this has completed (age counts down to zero and stops importing new blocks) you're ready to deploy your exploit. Detach from the tmux session and come back later if you wish.
If the command hangs or you receive an error such as:
Synchronisation failed, retrying err="peer is unknown or unhealthy"
Terminate the command (
Control+c). Delete the
~/.ethereum folder and try again
We can then interact with the blockchain through it using our wallet. To do so, we first have to import our private key from Metamask into the
geth node we've just set up. Navigate through the metamask app to find your private key. Don't share this with anyone as they will have full control of your CTF account and potentially solve all your levels for you.
Ctrl-b+c in tmux to get a new bash window (need to keep the
geth node running while we connect to it.) All of your windows will show up as a list in the bottom left, with an asterisk next to the one you're currently viewing. You can navigate through your tmux windows with:
Connect to your running
geth node with:
./build/bin/geth attach http://127.0.0.1:8545/
Now you're ready to import your private key with:
personal.importRawKey('put the key you copied from metamask here', 'add a password here')
Now you just have to enter your private key to unlock it.
We must wait until we are caught up before sending a transaction.
It is important that you keep the tmux sessions you've just set up running throughout the rest of the quarter in order to keep syncing the blockchain state and to save yourself time when performing the labs.
To do so, disconnect from the tmux session within the container by performing
This will put you into the container shell. We can then safely exit the container shell and the
tmux session will remain running. After exiting the container, you will then be back into the Ubuntu 18.04 VM which you can then exit from.
To reconnect to your session, ssh back into your VM instance on Compute Engine, then perform a "
docker exec -it manticore /bin/bash" to get a shell in the container. Finally, within the container shell, perform a "
tmux attach" to re-establish your sessions.
You have now set up an Ethereum node using
geth that you can now use to interact with the blockchain directly (rather than going to nodes hosted by companies such as Infura). We will need access to this node for running our symbolic execution exercises with Manticore.