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.

What you will build

You will deploy a Compute Engine instance, install Docker, and run the course's Docker image that contains the manticore framework and geth pre-installed.

What you'll learn

What you'll need

Install Ubuntu 18.04 VM

Install Docker on the VM

sudo apt update
sudo apt install -y docker.io
sudo usermod -a -G docker $(whoami)
newgrp docker

Troubleshooting

Download and run the custom container (located on Docker Hub as wuchangfeng/manticore)

docker run --name=manticore -di wuchangfeng/manticore

Examine the running container and the container's image

docker ps
CONTAINER ID        IMAGE               COMMAND             CREATED             STATUS                     PORTS               NAMES
6aa4ff2c9ebe        ...manticore...     "/bin/bash"         6 minutes ago       Up 2 seconds                                   manticore
docker images
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

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 geth session that allows you to interact with contracts via Javascript. One can be used to navigate the container's file system. All sessions can be maintained by simply detaching from the tmux session when you are done and and reattaching to the tmux session via "tmux attach"

tmux tips and hotkeys

Here's some quick tips to use tmux easily.

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

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.

Troubleshooting

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.

Now, use 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: Ctrl-b+n and Ctrl-b+p

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.

personal.unlockAccount(eth.accounts[0])

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.

What we've covered