Secure Computing (irisCTF 2024)

bpf_emu.py

from z3 import *

# nop out ptrace() call and then run
# % seccomp-tools dump ./chal_patched -l 8 | grep -Pv "=======|CODE" > dis3.txt 

s = Solver()

def add_cons(v):
    # printable ascii
    s.add(And(v > ord(' '), v <= ord('~')))

mem = [0, ]*16
X = 0
A = 0
sys_number = 0x1337
arch = 0xc000003e   # AUDIT_ARCH_X86_64
# bpf is 32 bits
args = []       # low DWORD
args2 = []      # hight DWORDs


# args is lower DWORD
for x in range(6):
    v = BitVec("arg%d"%x, 32)
    args.append(v)
    # add constrain on individual bytes, maybe ?
    add_cons(Extract(7, 0, v))
    add_cons(Extract(15, 8, v))
    add_cons(Extract(23, 16, v))
    add_cons(Extract(31, 24, v))

# args2 is upper DWORD
for x in range(6):
    v = BitVec("arg_2%d"%x, 32)
    args2.append(v)
    # add constrain on individual bytes, maybe ?
    add_cons(Extract(7, 0, v))
    add_cons(Extract(7, 0, v))
    add_cons(Extract(15, 8, v))
    add_cons(Extract(23, 16, v))
    add_cons(Extract(31, 24, v))


i = -1
with open("dis3.txt") as fp:
    for line in fp:
        i += 1

        print(line)
        ins = line.split("  ")[1].strip()


        # ignore return
        if ins.startswith("return "):
            continue

        #
        # >>    // load high DWORD  (args -> args)
        #
        elif " >> " in ins:
            ins = ins[:11]
            ins = ins.replace("args", "args2")


        print("%4d >>> %s"%(i, ins))
        #
        # if    // add constrains to solver
        #
        if ins.startswith("if ("):
            val = ins.split()[3][:-1]
            if val.startswith("0x"):
                val = int(val[2:], 16)
            else:
                val = int(val)

            #print(A)
            #print(val)
            s.add(A == val)
            continue

        # lol
        exec(ins)

        # if still int, keep on 32bits
        if type(A) is int:
            A &= 0xffffffff
        

assert s.check() == sat
model = s.model()
out = b''
for x in range(len(args)):
    v = model[args[x]].as_long()
    out += bytes.fromhex(hex(v)[2:])[::-1]
    v = model[args2[x]].as_long()
    out += bytes.fromhex(hex(v)[2:])[::-1]
print(out)