第二届BMZCTF公开赛REVERSE的checkin

照例下载压缩包附件，解压后是一个单独的exe程序：

.
.
照例扔入exeinfope中查看信息：

.
.
32位windows程序，无壳，照例运行一下查看主要回显信息：


.
.
首先讲一下正确的流程：
前面的LPL自定义函数后已经限定了v8要和v9相等才能接着运行。也就是说v8的值必定等于v9，所以LPL函数就不用管了。直接来看后面的LCK函数即可：


.
.
所以可以直接仿写逻辑写解题脚本：
这里要注意的是题目的putchar函数，输出的是无符号字符，所以我们要用&0xff来限制，因为8位只有0~256，必定是无符号的。

a1 = [12864, 5522, 10710, 6924, 788, 10715, 10008, 13022, 15893, 9754, 7946, 7490, 5636, 13477, 2198, 5861, 5799, 5259, 6464, 6171, 2269, 9251, 8315, 2989, -199, 2680]
a2=[12,-93,-91,120,113,-75,71,-86,37,69,126,42,97,-6,-27,-44,-53,-18,46,120,-72,124,52,-53,102,29,56,-26,-65,98,119,-81,41,-18,123,59]
for i in range(36):
	a2[i]^=((a1[i%26])&0xff)
a2[23]=102
flag=""
print(a2)
for i in range(36):
	#if a2[i]<0:
		#a2[i]+=256
	flag+=chr(int(a2[i]&0xff))
print(flag)

.
结果，得到flag：

.
.
下面说一下我的错误流程，一开始我直接分析LPL函数去了：

.
.
我写的z3库解方程函数：

from z3 import *
a2 = [12864, 5522, 10710, 6924, 788, 10715, 10008, 13022, 15893, 9754, 7946, 7490, 5636, 13477, 2198, 5861, 5799, 5259, 6464, 6171, 2269, 9251, 8315, 2989, 4294967097, 2680]
a1 = [BitVec(i, 8) for i in range(33)]	
print(a1)
v3 = []
for i in range(256):
	v3.append(i)

s = Solver()
s.add(a2[0] == v3[0] + 75 * a1[10] + 12 * a1[5] + 44 * a1[7] + 17 * a1[6] + 100 * a1[8] + 20 * a1[9])
s.add(a2[1] == 58 * a1[9] + 63 * a1[10] + 46 * a1[5] + 25 * a1[8] - 89 * a1[7] + 12 * a1[6] + 2 * v3[1])
s.add(a2[2] == 41 * a1[7] + 11 * a1[10] + 26 * a1[5] + 45 * a1[9] + 23 * a1[8] + 77 * a1[6] + 3 * v3[2])
s.add(a2[3] == 44 * a1[5] + 19 * a1[9] + 15 * a1[10] + 12 * a1[8] + 34 * a1[7] + 20 * a1[6] + 4 * v3[3])
s.add(a2[4] == 8 * a1[6] + 5 * a1[7] + 2 * (2 * a1[9] + a1[10]) - 4 * a1[8] + a1[5] + 5 * v3[4])
s.add(a2[5] == v3[5] + 85 * a1[5] + 99 * a1[10] + 8 * a1[8] + 10 * a1[7] + 12 * a1[6] + 9 * a1[9] + v3[6])
s.add(a2[6] == v3[8] + v3[7] + 55 * a1[14] + 12 * a1[12] + 11 * a1[11] + 33 * a1[13] + 77 * a1[15] + 20 * a1[16] + v3[9])
s.add(a2[7] == 3 * a1[16] + 56 * a1[12] + 21 * a1[14] + 45 * a1[13] + 66 * a1[11] + 78 * a1[15] + v3[10] * v3[11])
s.add(a2[8] == 13 * a1[13] + 96 * a1[11] + 78 * a1[16] + 65 * a1[12] + 25 * a1[15] + 54 * a1[14] + v3[25] / v3[5])
s.add(a2[9] == 41 * a1[12] + 11 * a1[11] + 36 * a1[16] + 7 * a1[15] + 20 * a1[14] + 88 * a1[13] + v3[30] / v3[3])
s.add(a2[10] == v3[200] + a1[13] + 8 * a1[12] + 55 * a1[15] + 14 * a1[14] + 62 * a1[16] + 17 * a1[11] + v3[210])
s.add(a2[11] == 5 * a1[14] + a1[11] + a1[16] + 52 * a1[15] + 2 * a1[12] + 6 * a1[13] + 88 * a1[14] + v3[150] / 3)
s.add(a2[12] == 9 * a1[20] + a1[18] + a1[17] + 8 * a1[19] + 11 * a1[21] + 85 * a1[22] + v3[77] / v3[7])
s.add(a2[13] == 55 * a1[22] + 22 * a1[21] + 78 * a1[20] + 56 * a1[18] + 65 * a1[19] + a1[17] + v3[78] / 3)
s.add(a2[14] == v3[55] + 6 * a1[17] + 19 * a1[19] + 3 * a1[20] - a1[21] - a1[22] + a1[18] * v3[20] - v3[66])
s.add(a2[15] == 4 * a1[17] + 46 * a1[22] + 77 * a1[21] + 8 * a1[20] - 10 * a1[18] - 5 * a1[19] - v3[30])
s.add(a2[16] == 19 * a1[19] + 18 * a1[18] + 17 * a1[17] + 21 * a1[21] + 22 * a1[22] + 20 * a1[20] + v3[120])
s.add(a2[17] == 8 * a1[18] + 5 * a1[20] + 9 * a1[22] + 85 * a1[21] + 9 * a1[19] + 4 * a1[17] - v3[20] * v3[30])
s.add(a2[18] == 88 * a1[27] + 8 * a1[26] + 6 * a1[24] + 5 * a1[23] + 7 * a1[25] + 22 * a1[28] - v3[50] * v3[4])
s.add(a2[19] == 7 * a1[27] + 10 * a1[26] + 80 * a1[25] + 50 * a1[24] + 12 * a1[28] - 20 * a1[23] - 8 * v3[80])
s.add(a2[20] == 3 * a1[23] + 25 * a1[28] + 8 * a1[26] + 14 * a1[25] + 4 * a1[27] + 7 * a1[24] - 12 * v3[60])
s.add(a2[21] == 6 * a1[23] + 8 * (10 * a1[27] + a1[26] + 5 * a1[28]) + 5 * a1[24] + 60 * a1[25] - 5 * v3[100])
s.add(a2[22] == -26 * a1[26] + 41 * a1[24] + 40 * a1[23] + 10 * a1[27] + 85 * a1[28] + 25 * a1[25] - 10 * v3[26])
s.add(a2[23] == -10 * a1[25] + 55 * a1[24] + 9 * (a1[23] + a1[28]) - a1[26] - a1[27])
s.add(a2[24] == a1[20] + a1[30] + a1[29] - a1[19] - 2 * a1[18] + a1[16] - 5 * v3[50])
s.add(a2[25] == a1[25] + 55 * a1[27] + 4 * a1[5] + a1[30] - a1[29] + 3 * a1[16] - 20 * v3[20])
if sat == s.check():
	ans = s.model()		#model方法返回结果数组，索引是前面定义的参数名。
	print(ans)
else:
	print("wdnmd")
flag=""
for i in range(5,31):
	flag+=chr(ans[a1[i]].as_long())
print(flag)
print(len(flag))

.
.
结果：
这里拿着26位的字符我不会了，只能直接用v8的值得到flag了。

.
.
.
.
.
解毕！敬礼！