前言

如果你之前做过suctf的printf，那么对于此题一定不会陌生，我这又不知道为啥了，动态跟程序直接报错了。

分析

首先你得了解格式化字符串都做了什么。

例如%2$*49$s%4$hhn意味着mem[3] = mem[48],程序中的输入应该是有64个参数，但是我在ida中只看到了61个参数，不过通过default.js我们还是可以确定一些基本的信息。

%2$*64$s%30$hhn ==> mem[29] = mem[63]

%2$*41$s%2$*41$s%9$hhn ==> mem[8] = mem[40] + mem[40]

%2$*35$s%2$110s%1$hhn ==> mem[0] = mem[34] +110

%1$s%5$hhn ==> mem[4]=bool(mem[0])

最后的结果我们需要使mem[15]=0

其中 mem[16]~mem[31] 对应的是flag[0]~flag[15]
men[48]-mem[64] 对应的是flag[0]-flag[15]
首先我们根据格式化参数 转化为 方程组

基本的分析方法有了，接下来就需要写出脚本对格式化参数进行清理，整理出表达式，然后利用z3求解

网上有此题的具体脚本，我就不自己写了。

#!/usr/bin/env python2
import re
import sys
import z3

def memory(addr, write=False):
    assert 1 <= addr <= 64
    assert write == (addr <= 32)
    i = (addr - 1) % 32
    if i >= 16:
        name = 'flag[%d]' % (i - 16)
    elif i == 15:
        name = 'result'
    else:
        name = 'r%d' % (i + 1)
    return name

def parse_op(fmt):
    m = re.match(r'^%2\$\*(\d+)\$s$', fmt)
    if m:
        addr = int(m.groups()[0])
        return { 'cmd': '*s', 'var': memory(addr) }
    m = re.match(r'^%(\d+)\$hhn$', fmt)
    if m:
        addr = int(m.groups()[0])
        return { 'cmd': 'hhn', 'var': memory(addr, write=True) }
    m = re.match(r'^%2\$(\d+)s$', fmt)
    if m:
        value = int(m.groups()[0])
        assert 0 < value < 256
        return { 'cmd': 's', 'var': str(value) }
    if fmt == '%1$s':
        return { 'cmd': 'bool', 'var': 'bool(r1)' }
    assert False

# prepare z3
solver = z3.Solver()
env = {}
for i in range(15):
    env['r%d' % (i + 1)] = 0
flag = []
for i in range(16):
    name = 'flag[%d]' % i
    env[name] = z3.BitVec(name, 8)
    flag += [ env[name] ]
    solver.add(32 <= flag[i])
    solver.add(flag[i] <= 126)

# read and interpret the code
with open('default.fs') as fh:
    for line in fh:
        op = [ parse_op('%' + fmt) for fmt in line.rstrip()[1 :].split('%') ]

        if op[0]['cmd'] == 'hhn':
            env[op[0]['var']] = 0
            print '[*] disas:', op[0]['var'], '= 0'
            op = op[1 :]

        if len(op) == 0:
            pass

        elif len(op) == 2:
            if op[0]['cmd'] == 'bool':
                assert op[0]['var'] == 'bool(r1)' and op[1]['cmd'] == 'hhn'
                solver.add(env['r1'] == 0)
                env[op[1]['var']] = 0
            else:
                assert op[0]['cmd'][-1] == 's' and op[1]['cmd'] == 'hhn'
                env[op[1]['var']] = env[op[0]['var']]
            print '[*] disas:', op[1]['var'], '=', op[0]['var']

        elif len(op) == 3:
            print '[*] disas:', op[2]['var'], '=', op[0]['var'], '+', op[1]['var']
            assert op[0]['cmd'][-1] == op[1]['cmd'][-1] == 's' and op[2]['cmd'] == 'hhn'
            if op[2]['var'] == 'result':
                assert op[0]['var'] == 'result'
                # reduced
            else:
                if op[1]['cmd'] == '*s':
                    env[op[2]['var']] = env[op[0]['var']] + env[op[1]['var']]
                else:
                    env[op[2]['var']] = env[op[0]['var']] + int(op[1]['var'])

        else:
            assert False

    print '[*] disas:', 'assert result == 0'
result = solver.check()
assert result == z3.sat
model = solver.model()
print "model",model
for i in range(16):
    flag[i] = chr(model[flag[i]].as_long())
flag = ''.join(flag)
print '[+] flag:', flag

自己将其理解了，那么之后再遇此类题目，改写就会十分的容易。

总结

此题对格式化参数的运用是比较全面的，通过printf进行运算的题目也算比较常见的。