SECCON Quals 2017 "printf machine" Writeup

_writeup.md

The binary is reading format strings one by one from provided file and prints them in /dev/null.

This fprintf receives a lot of parameters, which actually are 16 bytes of memory, 16 bytes of flag, and pointers to said bytes. That are 64 parameters in total. Because of using %hhn specifiers, format strings can write to provided memory addresses, so we can perform additions with them easily.

Since given "virtual program" was pretty big, almost 3400 lines, I wrote a parser to make "virtual instructions" (format strings) more human-readable. For example, %2$*36$s%2$*41$s%4$hhn becomes mem[3] = mem[3] + mem[8].

After parsing int human-readable form patterns in code became more obvious, so the next thing I wrote were two "optimizing" passes that folded additions in multiplications and then multiplications into one big sum.

Next, after parsing we have pretty simple program already. It is clear that flag is checked using a linear system, so we can use z3 to solve it easily.

parsed_program.txt

mem[3] = flag[0]
flag[0] = flag[13]
flag[13] = mem[3]

mem[3] = flag[1]
flag[1] = flag[7]
flag[7] = mem[3]

mem[3] = flag[2]
flag[2] = flag[10]
flag[10] = mem[3]

mem[3] = flag[5]
flag[5] = flag[10]
flag[10] = mem[3]

mem[3] = flag[6]
flag[6] = flag[14]
flag[14] = mem[3]

mem[3] = flag[7]
flag[7] = flag[15]
flag[15] = mem[3]

mem[3] = flag[9]
flag[9] = flag[14]
flag[14] = mem[3]

mem[3] = flag[10]
flag[10] = flag[15]
flag[15] = mem[3]

mem[3] = flag[12]
flag[12] = flag[14]
flag[14] = mem[3]

mem[3] = flag[13]
flag[13] = flag[15]
flag[15] = mem[3]

mem[3] = flag[14]
flag[14] = flag[15]
flag[15] = mem[3]

mem[2] = flag[0] * 220 + flag[1] * 14 + flag[2] * 22 + flag[3] * 235 + flag[4] * 183 + flag[5] * 129 + flag[6] * 245 + flag[7] * 145 + flag[8] * 25 + flag[9] * 113 + flag[10] * 235 + flag[11] * 35 + flag[12] * 246 + flag[13] * 240 + flag[14] * 93 + flag[15] * 107
mem[0] = 110 + mem[2]
Failed to parse: %1$s%5$hhn
mem[4] = 0
mem[15] = mem[15] + mem[4]
mem[2] = flag[0] * 0 + flag[1] * 152 + flag[2] * 34 + flag[3] * 136 + flag[4] * 253 + flag[5] * 131 + flag[6] * 123 + flag[7] * 165 + flag[8] * 232 + flag[9] * 231 + flag[10] * 182 + flag[11] * 18 + flag[12] * 220 + flag[13] * 171 + flag[14] * 69 + flag[15] * 75
mem[0] = 115 + mem[2]
Failed to parse: %1$s%5$hhn
mem[4] = 0
mem[15] = mem[15] + mem[4]
mem[2] = flag[0] * 43 + flag[1] * 219 + flag[2] * 165 + flag[3] * 225 + flag[4] * 193 + flag[5] * 11 + flag[6] * 248 + flag[7] * 28 + flag[8] * 86 + flag[9] * 5 + flag[10] * 198 + flag[11] * 56 + flag[12] * 212 + flag[13] * 218 + flag[14] * 18 + flag[15] * 154
mem[0] = 95 + mem[2]
Failed to parse: %1$s%5$hhn
mem[4] = 0
mem[15] = mem[15] + mem[4]
mem[2] = flag[0] * 8 + flag[1] * 79 + flag[2] * 96 + flag[3] * 233 + flag[4] * 169 + flag[5] * 183 + flag[6] * 226 + flag[7] * 188 + flag[8] * 205 + flag[9] * 20 + flag[10] * 56 + flag[11] * 119 + flag[12] * 110 + flag[13] * 52 + flag[14] * 233 + flag[15] * 146
mem[0] = 144 + mem[2]
Failed to parse: %1$s%5$hhn
mem[4] = 0
mem[15] = mem[15] + mem[4]
mem[2] = flag[0] * 197 + flag[1] * 241 + flag[2] * 177 + flag[3] * 75 + flag[4] * 107 + flag[5] * 76 + flag[6] * 68 + flag[7] * 208 + flag[8] * 102 + flag[9] * 110 + flag[10] * 26 + flag[11] * 83 + flag[12] * 17 + flag[13] * 26 + flag[14] * 57 + flag[15] * 63
mem[0] = 92 + mem[2]
Failed to parse: %1$s%5$hhn
mem[4] = 0
mem[15] = mem[15] + mem[4]
mem[2] = flag[0] * 205 + flag[1] * 148 + flag[2] * 209 + flag[3] * 248 + flag[4] * 18 + flag[5] * 142 + flag[6] * 67 + flag[7] * 53 + flag[8] * 80 + flag[9] * 174 + flag[10] * 123 + flag[11] * 194 + flag[12] * 201 + flag[13] * 223 + flag[14] * 84 + flag[15] * 47
mem[0] = 206 + mem[2]
Failed to parse: %1$s%5$hhn
mem[4] = 0
mem[15] = mem[15] + mem[4]
mem[2] = flag[0] * 68 + flag[1] * 120 + flag[2] * 89 + flag[3] * 96 + flag[4] * 153 + flag[5] * 29 + flag[6] * 37 + flag[7] * 218 + flag[8] * 101 + flag[9] * 117 + flag[10] * 248 + flag[11] * 65 + flag[12] * 140 + flag[13] * 43 + flag[14] * 239 + flag[15] * 106
mem[0] = 205 + mem[2]
Failed to parse: %1$s%5$hhn
mem[4] = 0
mem[15] = mem[15] + mem[4]
mem[2] = flag[0] * 14 + flag[1] * 218 + flag[2] * 92 + flag[3] * 251 + flag[4] * 91 + flag[5] * 29 + flag[6] * 155 + flag[7] * 16 + flag[8] * 31 + flag[9] * 1 + flag[10] * 118 + flag[11] * 214 + flag[12] * 220 + flag[13] * 174 + flag[14] * 159 + flag[15] * 70
mem[0] = 111 + mem[2]
Failed to parse: %1$s%5$hhn
mem[4] = 0
mem[15] = mem[15] + mem[4]
mem[2] = flag[0] * 196 + flag[1] * 24 + flag[2] * 230 + flag[3] * 117 + flag[4] * 133 + flag[5] * 191 + flag[6] * 90 + flag[7] * 84 + flag[8] * 61 + flag[9] * 82 + flag[10] * 19 + flag[11] * 216 + flag[12] * 93 + flag[13] * 95 + flag[14] * 128 + flag[15] * 161
mem[0] = 233 + mem[2]
Failed to parse: %1$s%5$hhn
mem[4] = 0
mem[15] = mem[15] + mem[4]
mem[2] = flag[0] * 80 + flag[1] * 23 + flag[2] * 133 + flag[3] * 17 + flag[4] * 58 + flag[5] * 134 + flag[6] * 204 + flag[7] * 222 + flag[8] * 245 + flag[9] * 66 + flag[10] * 223 + flag[11] * 96 + flag[12] * 153 + flag[13] * 76 + flag[14] * 189 + flag[15] * 4
mem[0] = 166 + mem[2]
Failed to parse: %1$s%5$hhn
mem[4] = 0
mem[15] = mem[15] + mem[4]
mem[2] = flag[0] * 96 + flag[1] * 116 + flag[2] * 110 + flag[3] * 226 + flag[4] * 57 + flag[5] * 112 + flag[6] * 132 + flag[7] * 185 + flag[8] * 234 + flag[9] * 30 + flag[10] * 167 + flag[11] * 5 + flag[12] * 171 + flag[13] * 222 + flag[14] * 137 + flag[15] * 54
mem[0] = 41 + mem[2]
Failed to parse: %1$s%5$hhn
mem[4] = 0
mem[15] = mem[15] + mem[4]
mem[2] = flag[0] * 68 + flag[1] * 71 + flag[2] * 197 + flag[3] * 155 + flag[4] * 88 + flag[5] * 188 + flag[6] * 220 + flag[7] * 8 + flag[8] * 22 + flag[9] * 42 + flag[10] * 188 + flag[11] * 64 + flag[12] * 23 + flag[13] * 27 + flag[14] * 64 + flag[15] * 204
mem[0] = 60 + mem[2]
Failed to parse: %1$s%5$hhn
mem[4] = 0
mem[15] = mem[15] + mem[4]
mem[2] = flag[0] * 95 + flag[1] * 144 + flag[2] * 238 + flag[3] * 1 + flag[4] * 67 + flag[5] * 18 + flag[6] * 231 + flag[7] * 29 + flag[8] * 18 + flag[9] * 243 + flag[10] * 250 + flag[11] * 119 + flag[12] * 66 + flag[13] * 56 + flag[14] * 12 + flag[15] * 110
mem[0] = 20 + mem[2]
Failed to parse: %1$s%5$hhn
mem[4] = 0
mem[15] = mem[15] + mem[4]
mem[2] = flag[0] * 188 + flag[1] * 219 + flag[2] * 205 + flag[3] * 136 + flag[4] * 205 + flag[5] * 232 + flag[6] * 25 + flag[7] * 192 + flag[8] * 72 + flag[9] * 94 + flag[10] * 148 + flag[11] * 141 + flag[12] * 59 + flag[13] * 0 + flag[14] * 195 + flag[15] * 98
mem[0] = 223 + mem[2]
Failed to parse: %1$s%5$hhn
mem[4] = 0
mem[15] = mem[15] + mem[4]
mem[2] = flag[0] * 107 + flag[1] * 196 + flag[2] * 112 + flag[3] * 47 + flag[4] * 237 + flag[5] * 172 + flag[6] * 223 + flag[7] * 90 + flag[8] * 242 + flag[9] * 207 + flag[10] * 163 + flag[11] * 117 + flag[12] * 162 + flag[13] * 128 + flag[14] * 50 + flag[15] * 139
mem[0] = 247 + mem[2]
Failed to parse: %1$s%5$hhn
mem[4] = 0
mem[15] = mem[15] + mem[4]
mem[2] = flag[0] * 44 + flag[1] * 185 + flag[2] * 38 + flag[3] * 75 + flag[4] * 115 + flag[5] * 112 + flag[6] * 160 + flag[7] * 161 + flag[8] * 178 + flag[9] * 46 + flag[10] * 218 + flag[11] * 239 + flag[12] * 160 + flag[13] * 254 + flag[14] * 59 + flag[15] * 137
mem[0] = 80 + mem[2]
Failed to parse: %1$s%5$hhn
mem[4] = 0
mem[15] = mem[15] + mem[4]

parser.py

import re
from copy import deepcopy as copy

class Expr:
    def __init__(self, dest, ops):
        self.dest = dest
        self.ops = copy(ops)
    def __repr__(self):
        return '{}({})'.format(self.__class__.__name__, str(self))

class SumExpr(Expr):
    def __str__(self):
        ops = ' + '.join(map(str, self.ops))
        if not self.dest:
            return ops
        return '{} = {}'.format(self.dest, ops)

class MulExpr(Expr):
    def __str__(self):
        ops = ' * '.join(map(str, self.ops))
        if not self.dest:
            return ops
        return '{} = {}'.format(self.dest, ops)

def main():
    index_map = {}
    for i in range(16):
        index_map[i + 1] = 'mem[{}]'.format(i)
        index_map[i + 32 + 1] = 'mem[{}]'.format(i)
        index_map[i + 16 + 1] = 'flag[{}]'.format(i)
        index_map[i + 48 + 1] = 'flag[{}]'.format(i)

    # PARSING
    parser = re.compile(r'%\d+\$(\d+)s|%\d+\$\*(\d+)\$s|%(\d+)\$hhn')
    res = []
    with open('default.fs', 'r') as f:
        for line in f:
            line = line.split('\n')[0]
            acc = []
            matches = list(parser.finditer(line))
            try:
                assert matches[0].start() == 0 and matches[-1].end() == len(line) and all(matches[i].end() == matches[i + 1].start() for i in range(len(matches) - 1)), 'Failed to parse ' + line
            except AssertionError:
                print('Failed to parse: ' + line)
                res.append('Failed to parse: ' + line)
            for match in matches:
                if match.group(1):          # imm
                    acc.append(match.group(1))
                if match.group(2):          # get
                    acc.append(index_map[int(match.group(2))])
                if match.group(3):          # set
                    res.append(SumExpr(index_map[int(match.group(3))], sorted(acc) or ['0']))

    # OPTIMIZING PASSES
    next_res = []
    it = 0
    while it < len(res):
        now = res[it]
        if isinstance(now, SumExpr) and str(now) == 'mem[3] = 0' and res[it + 1].dest == 'mem[8]' and len(res[it + 1].ops) == 1:    # multiplying
            it += 1
            op1 = res[it].ops[0]
            it += 1
            op2, cur_pow = 0, 1
            while res[it].dest in ('mem[3]', 'mem[8]'):
                if str(res[it]) == 'mem[8] = mem[8] + mem[8]':
                    cur_pow *= 2
                elif str(res[it]) == 'mem[3] = mem[3] + mem[8]':
                    op2 += cur_pow
                else:
                    print('[!] WTF on line {}'.format(it))
                it += 1
            next_res.append(MulExpr('mem[3]', [op1, str(op2)]))
        else:
            next_res.append(res[it])
            it += 1
    res = copy(next_res)

    next_res = []
    it = 0
    while it < len(res):
        now = res[it]
        ops = []
        if str(now) == 'mem[2] = 0':
            it += 1
            while res[it].dest == 'mem[3]':
                if res[it + 1].dest == 'mem[2]' and 'mem[2]' in res[it + 1].ops and 'mem[3]' in res[it + 1].ops:
                    t = copy(res[it])
                    t.dest = None
                    ops.append(t)
                it += 2
            next_res.append(SumExpr('mem[2]', ops))
        else:
            next_res.append(res[it])
            it += 1
    res = copy(next_res)

    # END
    with open('parsed.txt', 'w') as f:
        f.write('\n'.join(map(str, res)))


if __name__ == '__main__':
    main()

solve.py

import sys
sys.path.append(r'C:\tools\z3-4.5.0-x64-win\bin\python')

from z3 import *
init(r'C:\tools\z3-4.5.0-x64-win\bin')

def main():
    expressions = [
        "flag[0] * 220 + flag[1] * 14 + flag[2] * 22 + flag[3] * 235 + flag[4] * 183 + flag[5] * 129 + flag[6] * 245 + flag[7] * 145 + flag[8] * 25 + flag[9] * 113 + flag[10] * 235 + flag[11] * 35 + flag[12] * 246 + flag[13] * 240 + flag[14] * 93 + flag[15] * 107",
        "flag[0] * 0 + flag[1] * 152 + flag[2] * 34 + flag[3] * 136 + flag[4] * 253 + flag[5] * 131 + flag[6] * 123 + flag[7] * 165 + flag[8] * 232 + flag[9] * 231 + flag[10] * 182 + flag[11] * 18 + flag[12] * 220 + flag[13] * 171 + flag[14] * 69 + flag[15] * 75",
        "flag[0] * 43 + flag[1] * 219 + flag[2] * 165 + flag[3] * 225 + flag[4] * 193 + flag[5] * 11 + flag[6] * 248 + flag[7] * 28 + flag[8] * 86 + flag[9] * 5 + flag[10] * 198 + flag[11] * 56 + flag[12] * 212 + flag[13] * 218 + flag[14] * 18 + flag[15] * 154",
        "flag[0] * 8 + flag[1] * 79 + flag[2] * 96 + flag[3] * 233 + flag[4] * 169 + flag[5] * 183 + flag[6] * 226 + flag[7] * 188 + flag[8] * 205 + flag[9] * 20 + flag[10] * 56 + flag[11] * 119 + flag[12] * 110 + flag[13] * 52 + flag[14] * 233 + flag[15] * 146",
        "flag[0] * 197 + flag[1] * 241 + flag[2] * 177 + flag[3] * 75 + flag[4] * 107 + flag[5] * 76 + flag[6] * 68 + flag[7] * 208 + flag[8] * 102 + flag[9] * 110 + flag[10] * 26 + flag[11] * 83 + flag[12] * 17 + flag[13] * 26 + flag[14] * 57 + flag[15] * 63",
        "flag[0] * 205 + flag[1] * 148 + flag[2] * 209 + flag[3] * 248 + flag[4] * 18 + flag[5] * 142 + flag[6] * 67 + flag[7] * 53 + flag[8] * 80 + flag[9] * 174 + flag[10] * 123 + flag[11] * 194 + flag[12] * 201 + flag[13] * 223 + flag[14] * 84 + flag[15] * 47",
        "flag[0] * 68 + flag[1] * 120 + flag[2] * 89 + flag[3] * 96 + flag[4] * 153 + flag[5] * 29 + flag[6] * 37 + flag[7] * 218 + flag[8] * 101 + flag[9] * 117 + flag[10] * 248 + flag[11] * 65 + flag[12] * 140 + flag[13] * 43 + flag[14] * 239 + flag[15] * 106",
        "flag[0] * 14 + flag[1] * 218 + flag[2] * 92 + flag[3] * 251 + flag[4] * 91 + flag[5] * 29 + flag[6] * 155 + flag[7] * 16 + flag[8] * 31 + flag[9] * 1 + flag[10] * 118 + flag[11] * 214 + flag[12] * 220 + flag[13] * 174 + flag[14] * 159 + flag[15] * 70",
        "flag[0] * 196 + flag[1] * 24 + flag[2] * 230 + flag[3] * 117 + flag[4] * 133 + flag[5] * 191 + flag[6] * 90 + flag[7] * 84 + flag[8] * 61 + flag[9] * 82 + flag[10] * 19 + flag[11] * 216 + flag[12] * 93 + flag[13] * 95 + flag[14] * 128 + flag[15] * 161",
        "flag[0] * 80 + flag[1] * 23 + flag[2] * 133 + flag[3] * 17 + flag[4] * 58 + flag[5] * 134 + flag[6] * 204 + flag[7] * 222 + flag[8] * 245 + flag[9] * 66 + flag[10] * 223 + flag[11] * 96 + flag[12] * 153 + flag[13] * 76 + flag[14] * 189 + flag[15] * 4",
        "flag[0] * 96 + flag[1] * 116 + flag[2] * 110 + flag[3] * 226 + flag[4] * 57 + flag[5] * 112 + flag[6] * 132 + flag[7] * 185 + flag[8] * 234 + flag[9] * 30 + flag[10] * 167 + flag[11] * 5 + flag[12] * 171 + flag[13] * 222 + flag[14] * 137 + flag[15] * 54",
        "flag[0] * 68 + flag[1] * 71 + flag[2] * 197 + flag[3] * 155 + flag[4] * 88 + flag[5] * 188 + flag[6] * 220 + flag[7] * 8 + flag[8] * 22 + flag[9] * 42 + flag[10] * 188 + flag[11] * 64 + flag[12] * 23 + flag[13] * 27 + flag[14] * 64 + flag[15] * 204",
        "flag[0] * 95 + flag[1] * 144 + flag[2] * 238 + flag[3] * 1 + flag[4] * 67 + flag[5] * 18 + flag[6] * 231 + flag[7] * 29 + flag[8] * 18 + flag[9] * 243 + flag[10] * 250 + flag[11] * 119 + flag[12] * 66 + flag[13] * 56 + flag[14] * 12 + flag[15] * 110",
        "flag[0] * 188 + flag[1] * 219 + flag[2] * 205 + flag[3] * 136 + flag[4] * 205 + flag[5] * 232 + flag[6] * 25 + flag[7] * 192 + flag[8] * 72 + flag[9] * 94 + flag[10] * 148 + flag[11] * 141 + flag[12] * 59 + flag[13] * 0 + flag[14] * 195 + flag[15] * 98",
        "flag[0] * 107 + flag[1] * 196 + flag[2] * 112 + flag[3] * 47 + flag[4] * 237 + flag[5] * 172 + flag[6] * 223 + flag[7] * 90 + flag[8] * 242 + flag[9] * 207 + flag[10] * 163 + flag[11] * 117 + flag[12] * 162 + flag[13] * 128 + flag[14] * 50 + flag[15] * 139",
        "flag[0] * 44 + flag[1] * 185 + flag[2] * 38 + flag[3] * 75 + flag[4] * 115 + flag[5] * 112 + flag[6] * 160 + flag[7] * 161 + flag[8] * 178 + flag[9] * 46 + flag[10] * 218 + flag[11] * 239 + flag[12] * 160 + flag[13] * 254 + flag[14] * 59 + flag[15] * 137",
    ]
    expr_results = [110,115,95,144,92,206,205,111,233,166,41,60,20,223,247,80]
    flag = [BitVec('f{}'.format(i), 8) for i in range(16)]
    s = Solver()
    for expr, res in zip(expressions, expr_results):
        s.add(eval(expr) == 256-res)
    print(s.check())
    res = [s.model()[flag[i]].as_long() for i in range(len(flag))]
    res[14], res[15] = res[15], res[14]
    res[13], res[15] = res[15], res[13]
    res[14], res[12] = res[12], res[14]
    res[10], res[15] = res[15], res[10]
    res[14], res[9] = res[9], res[14]
    res[7], res[15] = res[15], res[7]
    res[14], res[6] = res[6], res[14]
    res[5], res[10] = res[10], res[5]
    res[2], res[10] = res[10], res[2]
    res[1], res[7] = res[7], res[1]
    res[0], res[13] = res[13], res[0]
    print('SECCON{{{}}}'.format(''.join(map(chr, res))))   # SECCON{Tur!n9-C0mpl3t3?}


if __name__ == '__main__':
    main()