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 an Ethereum light node (geth), the manticore framework, and files for enabling the symbolic execution of smart contracts from the SI CTF.

What you'll learn

What you'll need

Install Ubuntu 18.04 VM

Setup VM

sudo add-apt-repository -y ppa:ethereum/ethereum
sudo apt update -y
sudo apt install -y ethereum z3
git clone https://github.com/wu4f/cs410b-src
mkdir -p ~/solidity_versions/0.4.24/
curl -L https://github.com/ethereum/solidity/releases/download/v0.4.24/solc-static-linux > ~/solidity_versions/0.4.24/solc 
chmod a+x ~/solidity_versions/0.4.24/solc
echo 'export PATH=$PATH:~/solidity_versions/0.4.24/' >> ~/.bashrc
source ~/.bashrc
git clone -b 0.2.4 https://github.com/trailofbits/manticore.git
cd manticore
python3 setup.py build
sudo python3 setup.py install

tmux

Within the VM, 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 file system. All sessions can be maintained by simply detaching from the tmux session when you are done and reattaching to the tmux session via "tmux attach". Here's some quick tips to use tmux easily.

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 node's data contained in ~/.ethereum).. We want to use the latest version as well. To do this, in a tmux session, perform the following to bring up a go-ethereum light node on the Ropsten test network:

geth  --allow-insecure-unlock --syncmode light --ropsten --rpcapi admin,eth,net,web3,personal --nousb --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 Metamask 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:

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')

You can unlock the account using the password you just set for a particular duration (e.g. 1 hour) as shown below:.

personal.unlockAccount(eth.accounts[0], '<password>', 3600)

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 by performing

This will put you into the original shell on the VM.. We can then safely exit the VM shell and the tmux session will remain running. You can then exit from the Ubuntu 18.04 VM.

To reconnect to your session, ssh back into your VM instance on Compute Engine, then 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