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 an Ethereum light node (
manticore framework, and files for enabling the symbolic execution of smart contracts from the SI CTF.
tmuxto keep sessions persistent in the VM instance
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
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
tmux session when you are done and reattaching to the tmux session via "
tmux attach". Here's some quick tips to use tmux easily.
tmuxfrom the bash shell
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.
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.
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:
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, '<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.