第三题 七十二疑冢
观察
题目（又）给出了一个 32 位控制台 Windows 应用程序 C72.exe:
$ file C72.exe
C72.exe: PE32 executable (console) Intel 80386, for MS Windows
同样没有任何保护，运行一下：
N:\pediy\3>C72.exe
请输入序列号！////当且仅当回显“序列号输入正确”时才算破解成功
----------------------------------------------------
序列号：12345678
Input invalid!
看起来也是一个经典的输入 flag，输出对错的题目。
分析
这个程序分析起来难度比较小，其本身代码量很小，也没有任何保护，无论是采用 IDA Pro 还是在调试器中跟踪，很快便可以看清程序逻辑，故这里不再给出“如何阅读反汇编”这部分的分析过程，也不在着重分析诸如输入是怎么编码的之类的小细节问题，若有疑问可直接参阅后文的解题代码。
程序首先采用预定义的字符串初始化了一个作为 key 使用的 buffer，接下来读取输入，并对其进行 hex decode，这里的 hex decode 过程写的不太鲁棒（没有判断长度和字符范围），但其采用了转完之后再用 sprintf 重新格式化成大写 hex 串并和原串比较的方法，保证了输入一定是总计 18 个字符的大写 hex 串。将 decode 得到的 9 字节记为 g_input。
程序接下来逐个考虑这 9 个字节中的每一位（共 72 位），根据每一位利用另一张预定义的常量表（共 72 * 16 字节，不妨将其视作72行，每行16字节的表）将原始的 key buffer 进行变换。变换的具体方法为，对于第 i 位，若其是 1，则将 key_buffer+i 开始的 16 字节与预定义的常量表中的第 i 行进行异或。
接下来，程序摸出了一个 16 字节的 buffer，并调用了一个函数对其进行“解密”，要求解密得到的最后两字节为 0，若符合则将解密得到的内容作为字符串输出。结合程序一开始输出的提示，很显然，这里要求解密得到的是对应 序列号输入正确 这七个汉字的 GBK 编码加上两字节 00。
而这个“解密”函数也十分简单：
unsigned char kMysteriousTable[256][16] = { /* 略 */ };
void DecryptResponse(unsigned char *data, unsigned char *key, unsigned int keylen)
{
for (unsigned int i = 0; i < keylen; i++)
{
unsigned int lsb = data[0] ^ key[i];
for (int j = 0; j < 15; j++) {
data[j] = data[j+1] ^ kMysteriousTable[lsb][j];
}
data[15] = 0 ^ kMysteriousTable[lsb][15];
}
}
其对输入进行了 keylen 次操作，每次将数据的最低字节混合上当前 key，用作索引查表，然后将数据移动 8 位，前方补 0 并异或上表中对应的 16 字节。“移位”、“根据输入决定异或上的值”、“异或”……敏锐的读者可能在 10 句话之前就意识到了，这听上去就是一个反馈移位寄存器。
其与教科书般的 FSR 的差别在于其一次做 8 位而非 1 位。
知道了其是一个 FSR 之后，我们首先验证一下它是不是线性的，即对于一字节中 8 位分别的反馈的组合等同于整体的反馈：
import pefile
import operator
def u128(x):
assert len(x) == 16
return reduce(operator.or_, [(ord(c) << (8 * i)) for i, c in enumerate(x)])
pe = pefile.PE('C72.exe')
kBytewiseLFSRTable = 0xDEC0
bwlfsr_table = [u128(pe.get_data(i, 16)) for i in xrange(kBytewiseLFSRTable, kBytewiseLFSRTable + 256 * 16, 16)]
for i in xrange(256):
val = reduce(operator.xor, [bwlfsr_table[1 << j] for j in xrange(8) if (i >> j) & 1], 0)
assert val == bwlfsr_table[i]
print 'OK'
程序输出了 OK，同时我们发现：
assert bwlfsr_table[1] << 1 == bwlfsr_table[1 << 1]
也成立，因此看起来其就是一个单个的 Galois 模式的 LFSR 的一次处理一字节的“加速处理”版，也就是说，若将上述 C 代码中的 data、key 都视作小端表示的整数，其完全等价于以下代码：
mask = 0x1000000001408008000000002000000 << 7 # toggle mask
for i in xrange(keylen * 8):
lsb = ((data & 1) ^ ((key >> i) & 1))
data >>= 1
if lsb:
data ^= mask
解决
知道了这一点之后，接下来就好办了，线性反馈移位寄存器中的重点在于 线性，也就是说其输出完全是输入的线性组合，注意到输入及 LFSR 的参数已知，key 混合进去和 LFSR 同样是在 GF(2) 上进行的（说人话：都是异或），因此输出可以表示为 key 的各位的线性表示，加上已知的预期输出，可以得到一个线性方程组。
由于 LFSR 的长度是 128 位，这里可以得到 128 个线性方程，而 key 的长度是 138 * 8 位，远超过 128，因此可能的 key 会十分多，但由于 key 的生成方式所限，其中绝大多数都无法找到一个对应的 g_input。因此直接求解 key 再试图反算回程序的输入是不可行的。
注意到 key 生成的过程也是线性的，因此其实可以将 key 的每一位也表示成关于输入的 72 位的线性表示，这样只要解存在，其一定是唯一的，并且可以直接求出。
接下来就是愉快的写代码时间了，由于最后 GF(2) 上的线性方程组打算直接采用 Sage 求解，不如就把整个代码用 Sage 写吧。（当然也可以自己写 Gauss Elimination，但是何必呢……）
import pefile
import operator
def u128(x):
assert len(x) == 16
return reduce(operator.or_, [(ord(c) << (8 * i)) for i, c in enumerate(x)])
def split_bits(x):
return [(x >> i) & 1 for i in xrange(128)]
pe = pefile.PE('C72.exe')
# Data offsets (RVA)
kInitialKey = 0xB9D0 # length = 138
kBytewiseLFSRTable = 0xDEC0
kKeyRowTobeMixed = 0xEEC0
kWinMsg = 0xBA7E # length = 14
LFSRInputInstr = 0x1281
# Sanity check
bwlfsr_table = [u128(pe.get_data(i, 16)) for i in xrange(kBytewiseLFSRTable, kBytewiseLFSRTable + 256 * 16, 16)]
for i in xrange(256):
val = reduce(operator.xor, [bwlfsr_table[1 << j] for j in xrange(8) if (i >> j) & 1], 0)
assert val == bwlfsr_table[i], hex(val) + ' ' + hex(bwlfsr_table[i]) + ' ' + str(i)
# Solve
key = map(ord, pe.get_string_at_rva(kInitialKey))
encmsg = u128(''.join([pe.get_data(i+3, 4) for i in xrange(LFSRInputInstr, LFSRInputInstr + 7 * 4, 7)]))
winmsg = u128(pe.get_data(kWinMsg, 14) + '\x00\x00')
mask = bwlfsr_table[1] << 7
bitspos = [i for i, x in enumerate(bin(mask)[2:][::-1]) if x == '1']
keyrows = [map(ord, pe.get_data(i, 16)) for i in xrange(kKeyRowTobeMixed, kKeyRowTobeMixed + 72 * 16, 16)]
class Symbol(object):
def __init__(self, *idx):
self.const_v = 0
self.vars = set(idx)
def __ixor__(self, other):
if isinstance(other, int):
self.const_v ^^= other
else:
assert isinstance(other, Symbol)
self.const_v ^^= other.const_v
self.vars.symmetric_difference_update(other.vars)
return self
@classmethod
def const(cls, v):
result = cls()
result.const_v = v
return result
inpbit = map(Symbol, xrange(72))
cur = map(Symbol.const, split_bits(encmsg))
# LFSR in Galois mode
for i in xrange(len(key)):
for j in xrange(8):
c = Symbol.const((key[i] >> j) & 1)
for k in xrange(16):
if i - k < 0: break
if i - k > 71: continue
if (keyrows[i-k][k] >> j) & 1:
c ^^= inpbit[i-k]
c ^^= cur[0]
nxt = cur[1:] + [Symbol.const(0)]
for pos in bitspos:
nxt[pos] ^^= c
cur = nxt
GF2 = GF(2)
lhs = matrix(GF2, len(cur), len(inpbit))
rhs = vector([GF2(a ^^ b.const_v) for a, b in zip(split_bits(winmsg), cur)])
for i, sym in enumerate(cur):
for b in sym.vars:
lhs[i, b] = 1
print hex(int(''.join(map(str, lhs.solve_right(rhs))), 2))[2:].rstrip('L').upper()
运行即可得到本题的“序列号”：
$ time sage solve.sage
E7DFE373BFF25B92B6
sage solve.sage 0.81s user 0.13s system 99% cpu 0.944 total
Trivia
- 其实 Sage 自带符号计算功能，用的好的话甚至不用像上面的代码一样手动建出矩阵，可以直接 .solve()，但我不记得怎么用了，又懒得看文档，所以……
- 出于好奇，事后去看了一下把这个问题丢进 SMT Solver （比如 Z3）能不能直接解出来。看起来至少 Z3 可以 simplify 出等价于手动建出来的表示的 sexpr，不过这种通用的 SMT Solver 并不是拿来算这种问题的，所以能不能跑出来大概看运气（和一些 trick）吧。
吐槽
稍微认真一点写题解真的好累呀……
[培训]内核驱动高级班，冲击BAT一流互联网大厂工作，每周日13:00-18:00直播授课
