Balsn CTF 2019 - simple sol aeg

Balsn CTF 2019 - simple sol aeg writeup.md

Solidity Automatic Exploit Generation?
try it:
nc aab2596ac4a422a9f803ed317089c399b818bb72.balsnctf.com 30731

Be a King

* Give you a contract bytecode, give me transaction data to be a king.
* Timeout = 10 seconds per challenge.
* You can call isKing() to verify it.
* pragma solidity 0.4.25


This challenge requires Proof-of-Work (PoW). We have already finished the code for you. Please see pow.balsnctf.com . 
Author: ysc

The problem is simple. It will give you a contract bytecode, you need to analysis which function call will let isKing() to return true.

We only use three contract templates (three level).

The level 1 sample contract is:

pragma solidity 0.4.25;
contract King {
    bool king = false;
    function setKing_mbruyevcop() public{   // function signature is random
        king = true;
    }
    function isKing() view public returns (bool){
        return king;
    }
}

In level 2, We have multiple setKing_%(random)s() functions which like:

pragma solidity 0.4.25;
contract King {
    bool king = false;
    function setKing_iprjllplvn() public{
        king = false;
    }
    function setKing_duyfevifta() public{
        king = false;
    }
    // ... multiple function to set king to false, only one function to set true.
    function setKing_jheajcokms() public{
        king = true;
    }
    function isKing() view public returns (bool){
        return king;
    }
}

In level 3, you should call a function with an argument to trigger integer overflow. A level 3 sample contract is:

pragma solidity 0.4.25;
contract King {
    bool king = false;
    uint private sb = 100;

    function setKing_utsgesanbm(uint value) public{
        sb -= value;
        if (sb > 409792) {
            if (sb < 409800) {
                king = true;
            }
            else {
                king = false;
            }
        }
    }
    function isKing() view public returns (bool){
        return king;
    }
}

Of course, you only get the bytecode from this challenge.

There are two intended solutions to solve:

1. Analysis these contract bytecode, parse them and get the function signature (and calculate an argument in level 3).
2. Use symbolic execution tools.

You can analysis bytecode by yourself which like PPP's writeup and perfectblue's writeup. They did a great job!

Or you can use symbolic execution tool: manticore. You can get more information from mephi42's writeup. Well done!

My symbolic execution script is below. If you know symbolic execution and learn how2use manticore, you even don't need to parse these bytecode!

It's fun to learn symbolic execution and learn how2hack this challenge. I hope you enjoy ;)

exp.py

#!/usr/bin/env python3

import binascii
import hashlib
import re
import socket
import sys

from manticore.ethereum import ABI, ManticoreEVM

ADDRESS = 'aab2596ac4a422a9f803ed317089c399b818bb72.balsnctf.com'
PORT = 30731
CHALL_NUM = 10


class Netcat:
    def __init__(self, ip, port):
        self.buff = b""
        self.socket = socket.socket(socket.AF_INET, socket.SOCK_STREAM)
        self.socket.connect((ip, port))

    def _ret_buff(self, pos):
        rval = self.buff[:pos]
        self.buff = self.buff[pos:]
        return rval

    def read(self, length=1024):
        self.buff += self.socket.recv(length)
        return self._ret_buff(length)

    def read_until(self, data):
        while data not in self.buff:
            self.buff += self.socket.recv(1024)

        pos = self.buff.find(data)
        return self._ret_buff(pos + len(data))

    def write(self, data):
        self.socket.send(data)

    def close(self):
        self.socket.close()


def PoW(nc):
    r = nc.read_until(b'??? = ')
    print(r.decode())
    prefix = re.findall(b'sha256\((.*) \+ \?\?\?\)', r)[0]
    difficulty = int(re.findall(b'== 0+\((\d+)\)', r)[0])
    zeros = '0' * difficulty

    def is_valid(digest):
        if sys.version_info.major == 2:
            digest = [ord(i) for i in digest]
        bits = ''.join(bin(i)[2:].zfill(8) for i in digest)
        return bits[:difficulty] == zeros

    pow_answer = 0
    while True:
        pow_answer += 1
        s = prefix + str(pow_answer).encode()
        if is_valid(hashlib.sha256(s).digest()):
            print(repr(pow_answer))
            break
    nc.write(str(pow_answer).encode() + b'\n')


def send_symbolic(user_account, contract_account):
    symbolic_data = m.make_symbolic_buffer(320)
    symbolic_value = m.make_symbolic_value()

    m.transaction(
        caller=user_account,
        address=contract_account,
        value=symbolic_value,
        data=symbolic_data,
    )


def send_abi_isKing(user_account, contract_account):
    calldata = ABI.function_call("isKing()")
    m.transaction(
        caller=user_account,
        address=contract_account,
        data=calldata,
        value=0,
        gas=10000000,
    )


nc = Netcat(ADDRESS, PORT)

PoW(nc)

print(nc.read_until(b'\n').decode())

for i in range(CHALL_NUM):
    r = nc.read_until(b'your tx data: ')
    print(r.decode())
    bytecode = r.split(b'\n')[-2]

    m = ManticoreEVM()

    user_account = m.create_account(balance=1000)
    init_bytecode = binascii.unhexlify(bytecode)
    contract_account = m.create_contract(init=init_bytecode,
                                         owner=user_account)

    send_symbolic(user_account, contract_account)
    send_abi_isKing(user_account, contract_account)

    for state in m.ready_states:
        result = state.platform.all_transactions[-1].return_data
        is_king = state.can_be_true(result == b'\x01'.rjust(32, b'\x00'))
        if is_king:
            data = state.platform.all_transactions[-2].data
            ans = state.solve_one(data)
            ans = binascii.hexlify(ans)
            break
    else:
        print('answer not found')
        exit()

    print(f'ans: {ans}')
    nc.write(ans + b'\n')
    r = nc.read_until(b'\n')
    print(r.decode())
    if r != b'Solved!\n':
        exit()

print(nc.read(65536).decode())