not-baby-parallelism

overengineering.md

DiceCTF not-baby-parallelism

totally overengineered solution

1. Generate an execution trace with qemu magic

#!/bin/bash

CALLS=(
    # loop1
    3448    # get operand2
    3461    # get operand1
    346f    # call r12  // op to apply
    3486    # store op
    # loop2
    35f1    # get operand2
    360a    # get operand1
    3618    # call r12  // op to apply
    3635    # store op
)

# dummy input with same length than original flag (wc -l flag.out)
# num_char ch1 ch2 chr3 ...
echo "51 48 49 50 51 52 53 54 55 56 57 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79" > in.txt

# https://en.wikibooks.org/wiki/QEMU/Invocation
#qemu-x86_64 -singlestep -d nochain,cpu,in_asm ./pppp -n 1 -i in.txt -o out3.txt 2> trace2.txt
qemu-x86_64 -singlestep -d nochain,cpu ./pppp -n 1 -i in.txt -o out3.txt 2> trace2.txt

reg="$(echo ${CALLS[@]} | tr " " "|")"
reg="RIP=000000400000($reg) "

egrep -B4 "$reg" trace2.txt > trace.txt

it looks like that:

RAX=0000004002809050 RBX=0000000000000001 RCX=0000000000000001 RDX=0000000000000000
RSI=0000000000000000 RDI=0000004002809050 RBP=000000400355fe10 RSP=000000400355fda0
R8 =0000000000000000 R9 =00000040035606c0 R10=0000004002a815f8 R11=0000004002aad100
R12=000000400000333a R13=0000000000000000 R14=0000004002808ca0 R15=0000004002d60000
RIP=0000004000003448 RFL=00000246 [---Z-P-] CPL=3 II=0 A20=1 SMM=0 HLT=0
--
RAX=0000004002809050 RBX=0000000000000030 RCX=0000000000000001 RDX=0000000000000001
RSI=0000000000000001 RDI=0000004002809050 RBP=000000400355fe10 RSP=000000400355fda0
R8 =0000000000000000 R9 =00000040035606c0 R10=0000004002a815f8 R11=0000004002aad100
R12=000000400000333a R13=0000000000000000 R14=0000004002808ca0 R15=0000004002d60000
RIP=0000004000003461 RFL=00000206 [-----P-] CPL=3 II=0 A20=1 SMM=0 HLT=0
--
RAX=0000000000000031 RBX=0000000000000030 RCX=0000000000000001 RDX=0000000000000008
RSI=0000000000000030 RDI=0000000000000031 RBP=000000400355fe10 RSP=000000400355fda0
R8 =0000000000000000 R9 =00000040035606c0 R10=0000004002a815f8 R11=0000004002aad100
R12=000000400000333a R13=0000000000000000 R14=0000004002808ca0 R15=0000004002d60000
RIP=000000400000346f RFL=00000202 [-------] CPL=3 II=0 A20=1 SMM=0 HLT=0
--
RAX=0000004002809050 RBX=0000000000000001 RCX=0000000000000001 RDX=0000000000000001
RSI=0000000000000001 RDI=0000004002809050 RBP=000000400355fe10 RSP=000000400355fda0
R8 =0000000000000000 R9 =00000040035606c0 R10=0000004002a815f8 R11=0000004002aad100
R12=000000400000333a R13=0000000000000000 R14=0000004002808ca0 R15=0000004002d60000
RIP=0000004000003486 RFL=00000202 [-------] CPL=3 II=0 A20=1 SMM=0 HLT=0
--

2. parse trace to something we can live with

#!/usr/bin/env python3

class Insn:
    pass

class TraceParser:
    # registers i need
    # check FS reg for thread id ?
    regs = ["RSI", "RDI", "R12", "RIP"]

    def __init__(self, filename):
        self.insns = []

        with open(filename, "r") as fp:
            buff = []
            for line in fp:
                line = line.strip()
                if line != "--":
                    buff.append(line)
                else:
                    self.parse_insn(buff)
                    buff = []
            self.parse_insn(buff)

    def parse_insn(self, buff):
        insn = Insn()
        for line in buff:
            line = line.replace(" =", "=")  # 
            line = line.split()
            for reg_val in line:
                reg_val = reg_val.split("=")
                if len(reg_val) == 2:
                    reg_name = reg_val[0]
                    # only save the registers we want
                    if reg_name in TraceParser.regs:
                        value = int(reg_val[1], 16)
                        setattr(insn, reg_name.lower(), value)
        self.insns.append(insn)

    def dump(self):
        handlers = {
                # loop1
                0x4000003448: self.op_get_two,
                0x4000003461: self.op_get_one,
                0x400000346f: self.op_compute,
                0x4000003486: self.op_store_res,
                # loop2
                0x40000035f1: self.op_get_two,
                0x400000360a: self.op_get_one,
                0x4000003618: self.op_compute,
                0x4000003635: self.op_store_res
                }

        for insn in self.insns:
            handlers[insn.rip](insn)


    #
    # handlers
    #
    def op_get_one(self, op):
        print("get_1 %d"%op.rsi)
    
    def op_get_two(self, op):
        print("get_2 %d"%op.rsi)
    
    def op_compute(self, op):
        # r12 has a function pointer to the op
        op_list = {
                0x400000330a: "add",
                0x4000003323: "mul",
                0x400000333a: "xor"
                }
        
        comp = op_list[op.r12]
        print(comp)

    
    def op_store_res(self, op):
        print("store %d"%op.rsi)
    

if __name__ == "__main__":
    t = TraceParser("trace.txt")
    t.dump()

we get something like:

get_2 0
get_1 1
xor
store 1
get_2 2
get_1 3
xor
store 3
get_2 4
get_1 5
xor
store 5
get_2 6
get_1 7
xor
store 7
get_2 8
get_1 9
xor
store 9
get_2 10
get_1 11
xor
store 11
get_2 12
get_1 13
xor
store 13
get_2 14
get_1 15
xor
store 15

3. solve the actual shit

#!/usr/bin/env python3 

from z3 import *
import sys

FLAG_LEN = 51

# result
result = [int(_.strip()) for _ in open("flag.out", "r").readlines()]

# initialize flag
flag = []
meh = []
for x in range(FLAG_LEN):
    zz = BitVec("f%d"%x, 8)
    flag.append(zz)
    meh.append(zz)  # yeah i suck


# parse trace and build symbolic flag

with open(sys.argv[1], "r") as fp:
    for line in fp:
        line = line.strip().split()
        
        if line[0] == "get_2":
            v2 = flag[int(line[1])]
        elif line[0] == "get_1":
            v1 = flag[int(line[1])]
        elif line[0] == "store":
            flag[int(line[1])] = res
        elif line[0] == "xor":
            res = v1 ^ v2
        elif line[0] == "add":
            res = v1 + v2
        elif line[0] == "mul":
            res = v1 * v2


# solve shit

s = Solver()
for idx, fl in enumerate(flag):
    s.add(And(meh[idx] >= 32, meh[idx] <= 126))
    s.add(fl == result[idx])

if s.check() != sat:
    print("meh :(")
    sys.exit(1)

model = s.model()
bingo = ''

for c in meh:
    bingo += chr(model[c].as_long())

print(bingo)

dice{p4r411el_pref1x_sc4ns_w0rk_efficient_but_sl0w}

thank you for your service.