CTF2017 第十四题 半盲道人cm

前言

因比较忙，后来抽空才补的 writeup，渡。 大的 writeup，已经分析的非常彻底了，所以本文就从虚拟机伪码生成开始阐述不同的部分

伪码生成

先上解码代码

with open("CTF.exe", "rb") as f:
    f.seek(0x40ac0)
    code = f.read(0x1c729)
# 先仿造程序逻辑生成指令对
cmds = []
stack = []
for i in xrange(len(code)):
    x = ord(code[i])
    if x == 62:
        cmds.append([1, 0])
    elif x == 60:
        cmds.append([2, 0])
    elif x == 43:
        cmds.append([3, 0])
    elif x == 45:
        cmds.append([4, 0])
    elif x == 46:
        cmds.append([5, 0])
    elif x == 44:
        cmds.append([6, 0])
    elif x == 91:
        cmds.append([7, 0])
        stack.append(i)
    elif x == 93:
        t = stack.pop()
        cmds.append([8, t])
        cmds[t][2] = i
    elif x == 0:
        pass
    else:
        assert False
# 生成伪代码
bufp = 0
tabs = 1
for i in xrange(len(cmds)):
    x, p = cmds[i]
    if x == 1:
        bufp += 1
    elif x == 2:
        bufp -= 1
    elif x == 3:
        print "{0}++ [{1}]".format('\t'*tabs, bufp)
    elif x == 4:
        print "{0}-- [{1}]".format('\t'*tabs, bufp)
    elif x == 5:
        print "{0}[{1}] == check_next".format('\t'*tabs, bufp)
    elif x == 6:
        print "{0}[{1}] = key_next".format('\t'*tabs, bufp)
    elif x == 7:
        print "{0}[{1}] {{".format('\t'*tabs, bufp)
        tabs += 1
    elif x == 8:
        tabs -= 1
        print "{0}}} [{1}]".format('\t'*tabs, bufp)
    else:
        assert False

会生成非常长的代码，在进行找出规律、正则替换、手动美化后，成为这样

	[57..152] = key[0..95] // 赋值输入的 96bit

	[37] = 1
	[37] {
		[41] = [60] * [61] * [62]
			 + [60] * [62]
			 + [61] * [62]
			 + [60] * [61]
			 + [60] + [61] + [62]

		[46] = [59] * [65] * [83]
			 + [58] * [60] * [62] * [64]

		[21] = [41] * [46] + [41] + [46]

		[50] = [21] % 2

		[50] == check_next // 和内置进行监测

		[21] = [103] + [105] + [150] + [152]

		[50] = [21] % 2

		[152..58, 57] = [151..57, 50] // 57-151 向后移动，前面用 50 补

		[37] = (48 - key_next) != 0 // 函数的逻辑是检测满 3600 个 1 后返回 48，而内置最多就3600个
	} [37]

这里要用到逻辑代数的几个推导

那么上面的伪码还能化简

		[50] = [60] | [61] | [62] | (([59] & [65] & [83]) ^ ([58] & [60] & [62] & [64]))

		[50] == check_next

		[50] = [103] ^ [105] ^ [150] ^ [152]

		[152..58, 57] = [151..57, 50]

当时我的想法是认为位数过大(96)，移动变换复杂(4个异或)，要检测的量很大(4k)，我的想法是只检测结果为 0 的部分(只有400多个)，并且，从上面的最简式看，最后是全或，那么只有满足，[60] = [61] = [62] = 0，[59] & [65] & [83] = 0 这 2个判定，结果才能是 0

渡。大的 z3 是神器啊，我手动的方法差距1w倍，因为程序输入是可显字符，那么一开始就隐含了每字节最高位是 0 的条件，附求解代码(自己想的算法)

with open("CTF.exe", "rb") as f:
    f.seek(0x37820)
    inner = f.read(0xfb8)
# 存放已知 0值 的 idx
zero_idx = set()
# 已知最高位 0
for i in xrange(96):
    if i % 8 == 7:
        zero_idx.add(i)
# 存放已知 0值 的 模拟式
zero_f = set()
from collections import defaultdict
# 存放已知 相等 idx 对， a^b = 0 -> a = b
equ_pair = defaultdict(list)
# 消简异或模拟式中的相邻2元素，a^b^b^c = a^c
def rmrpl(arr):
    if len(arr) < 2:
        return arr
    tt = None
    for ii in xrange(len(arr) - 1, -1, -1):
        if tt != arr[ii]:
            tt = arr[ii]
        else:
            del arr[ii + 1]
            del arr[ii]
            tt = None
    return arr
# 插入 相等 idx 对
def ins_pair(lit, big):
    global equ_pair
    if lit not in equ_pair:
        equ_pair[lit].append(big)
        return
    if big in equ_pair[lit]:
        return
    equ_pair[lit].append(big)
    equ_pair[lit].sort()
def get_idx(ss):
    return int(ss[2: -1])
# 插入 模拟式
def ins_f(ff):
    global zero_f
    global zero_idx
    if ff == "0":
        return
    zero_f.add(ff)
    if ff.count("^") == 0:
        # 只有一个元素那它的值就是 0
        zero_idx.add(get_idx(ff))
        return True
    elif ff.count("^") == 1:
        # 两个元素就是 相等对
        arr = ff.split("^")
        ins_pair(get_idx(arr[0]), get_idx(arr[1]))
        return True
    # 返回是否有新的确定项
    return False
and_tuple = set()
def one_round():
    global zero_idx
    global and_tuple
    and_tuple.clear()
    # buf 存放模拟式，用来自身反馈消简
    buf = defaultdict(int)
    for i in xrange(96):
        buf[57 + i] = "k[{0:2d}]".format(i)
    # 初始化已知 0值
    for i in zero_idx:
        buf[57 + i] = '0'
    # 初始化相等对，注意赋值顺序
    keysort = equ_pair.keys()
    keysort.sort()
    for lit in keysort:
        for big in equ_pair[lit]:
            if lit in zero_idx and big not in zero_idx:
                zero_idx.add(big)
            elif lit not in zero_idx and big in zero_idx:
                zero_idx.add(lit)
                buf[57 + lit] = '0'
            buf[57 + big] = buf[57 + lit]
    ret = False
    for x in inner:
        if ord(x) == 0:
            # ret 是返回有没有新增已知项
            ret = ins_f(buf[60]) or ret
            ret = ins_f(buf[61]) or ret
            ret = ins_f(buf[62]) or ret
            buf[60] = buf[61] = buf[62] = '0'
            if buf[59] != '0' and buf[65] != '0' and buf[83] != '0':
                # 收集 与的 结果
                and_tuple.add("({0}) & ({1}) & ({2})".format(buf[59], buf[65], buf[83]))
        tarr = buf[103].split("^") + buf[105].split("^") + buf[150].split("^") + buf[152].split("^")
        # 先去 0
        tarr = [t for t in tarr if t != '0']
        tarr.sort()
        tarr = rmrpl(tarr)
        t = "^".join(tarr)
        # 模拟式已知 0值 则替换成 0
        if len(t) == 0 or t in zero_f:
            t = '0'
        # 模拟移动
        for i in xrange(152, 57, -1):
            buf[i] = buf[i - 1]
        buf[57] = t
    return ret
while True:
    if not one_round():
        # 已经没有新增项了，清楚掉已知模拟式，再来最后一次
        zero_f.clear()
        one_round()
        break
assert len(zero_f) == 0
assert len(and_tuple) == 0
# 很幸运，所有未知条件都清除了
last = [1] * 96
for i in zero_idx:
    last[i] = 0
# 组装最后的结果字符串
r = ""
for i in xrange(12):
    c = 0
    for j in xrange(7, -1, -1):
        c |= last[i * 8 + j]
        c <<= 1
    r += chr(c >> 1)
print r

[培训]内核驱动高级班，冲击BAT一流互联网大厂工作，每周日13:00-18:00直播授课