imnotavirus
解exe，解密pyc
利用解密后的pyc，找到注入的shellcode，用ida解smc，最后解密
比赛的时候还被迫阅读了一下pyinstaller的源码，收获很大
解exe
看到附件给了个pyinstaller，猜测是python逆向
先ida看一眼，有upx壳，自动脱壳，再用exeinfo确认了一下是python逆向，pyinstxtractor.py解包（之前V&N2021就吃了这个亏）
解pyc
解包时提示被加密了
取struct头作为标准头，用pycdc还原出main.py，发现调用了sign
去PYZ00文件夹看一下，发现被加密了，看一下目录，发现pyimod和比一般情况多了一些东西，把这些都解开看一下，有一个key文件
同时发现archive中有一个Cipher类，但是pycdc缺少指令，无法全部还原，考虑看一下pycdas解出来的字节码
字节码中有个对pyinstaller源码的引用，直接去文件夹里面看，发现能解密出来的部分完全一致
照着源码中的方法解密sign
from key import key
import tinyaes
print (key)
f = open('./PYZ-00.pyz_extracted/sign.pyc.encrypted', 'rb')
data = f.read()
cipher = tinyaes.AES(key.encode(), data[:16])
output = cipher.CTR_xcrypt_buffer(data[16:])
f.close()
import zlib
output = zlib.decompress(output)
f = open('./sign.pyc', 'wb')
f.write(output)
解密
解出sign后看到有三个base64，其中两个是执行的语句，此外大部分语句涉及到了内存
另外一个base解出来是乱码，用字节码辅助恢复函数（其实特征已经很明显了），发现进行了rc4加密，直接打印出解密结果，将结果写入文件，用ida查看
发现smc
mov eax, 41178Bh
mov ecx, 411802h
sub ecx, eax
loc_2A:
mov ebx, [rax]
xor ebx, 77h
mov [rax], ebx
loop loc_2A
解出来后尝试恢复了一下函数，结果很丑…只能和汇编比较着进行分析了（好像只要把00 patch一下就可以反编译了）
seg000:000000000000007E loc_7E: ; CODE XREF: sub_0+73↑j
seg000:000000000000007E mov eax, [rbp+var_20]
seg000:0000000000000081 cmp eax, [rbp+var_8]
seg000:0000000000000084 jge short loc_B2
seg000:0000000000000086 mov eax, [rbp+8]
seg000:0000000000000089 add eax, [rbp+var_20]
seg000:000000000000008C movsx ecx, byte ptr [rax]
seg000:000000000000008F xor ecx, 13h
seg000:0000000000000092 mov edx, [rbp+8]
seg000:0000000000000095 add edx, [rbp+var_20]
seg000:0000000000000098 mov [rdx], cl
seg000:000000000000009A mov eax, [rbp+8]
seg000:000000000000009D add eax, [rbp+var_20]
seg000:00000000000000A0 movsx ecx, byte ptr [rax+1]
seg000:00000000000000A4 xor ecx, 37h
seg000:00000000000000A7 mov edx, [rbp+8]
seg000:00000000000000AA add edx, [rbp+var_20]
seg000:00000000000000AD mov [rdx+1], cl
seg000:00000000000000B0 jmp short loc_75
发现是两两一组进行加密，分别异或0x13和0x37
>>> for i in range(len(cipher)):
... if i % 2 == 0:
... print (chr(cipher[i] ^ 0x13), end = '')
... else:
... print (chr(cipher[i] ^ 0x37), end = '')
...
@rey0ug0nn2$1gnth1s0r1tw1llb3y0ursurv1
内卷
这题是赛后边补边写的，所以废话略多
花指令
搜索静态字符串能找到很多有用的字符串，但发现找不到引用
从start开始往里面翻一翻，发现有个一大片数据没有被解析出来，说明是个花指令，之前没见过这个花，简单记录一下
.text:00000001400016AB call loc_1400016B3
.text:00000001400016AB ; ---------------------------------------------------------------------------
.text:00000001400016B0 db 0E8h, 0EBh, 12h
.text:00000001400016B3 ; ---------------------------------------------------------------------------
.text:00000001400016B3
.text:00000001400016B3 loc_1400016B3: ; CODE XREF: sub_1400015E2+C9↑j
.text:00000001400016B3 pop rax ; 取出栈顶数据
.text:00000001400016B4 add rax, 1 ; 对其进行+1
.text:00000001400016B8 push rax ; 然后再压栈
.text:00000001400016B9 mov rax, rsp
.text:00000001400016BC xchg rax, [rax]
.text:00000001400016BF pop rsp
.text:00000001400016C0 mov [rsp+0], rax
.text:00000001400016C4 retn
这个花长这样，所以 Call loc_1400016B3 的操作就是跳过 E8，把第一个E8 patch成nop，发现EB 12就是跳到这个函数的后面，所以这条 Call 指令也可以Patch掉
还有一些长跳转，这个就直接按c转成指令就行
还有这个花
.text:0000000140006D12 loc_140006D12: ; CODE XREF: sub_1400015E2:loc_140006D12↑j
.text:0000000140006D12 jmp short near ptr loc_140006D12+1
把 jmp 指令的第一个字节patch了就行
花指令全部去掉之后发现结尾还有一部分没有反编译，这个比赛的时候没想出来怎么搞，不知道怎么回时，所以这题后面也就没有怎么做了
运算简化
比赛的时候想直接动调跳过这些运算的，结果看到和input还有关系，这就不好办了，尝试手动看一下这是什么运算，但也没啥想法
结果，晚上再看这道题的时候发现竟然看懂这个离谱运算了，啊啊啊啊啊好气啊
虽然有一堆函数，观察发现，通常每一个for循环中，包裹了两个while循环，但比赛的时候一直以for循环为单位在想代码的含义，晚上再看的时候才发现，每一个while循环才是一个单位函数
v1155 = ll;
v1154 = 1i64;
v1153 = ll & 1;
v1152 = ll ^ 1;
while ( v1153 ) {
v1151 = v1152;
v1150 = 2 * v1153;
v1153 = (2 * v1153) & v1152;
v1152 ^= v1150;
}
ll = v1152;
v1041 = v1043;
v1040 = v1045;
v1039 = v1045 & v1043;
v1038 = v1045 ^ v1043; // 运算简化方法：^ 换成 +，然后只保留这一行和最后一行
while ( v1039 ) {
v1037 = v1038;
v1036 = 2 * v1039;
v1039 = (2 * v1039) & v1038;
v1038 ^= v1036;
}
v1043 = v1038;
简单地说，上面这段代码，最终的执行效果就是，ll = ll + 1，推广到下半部分，就是 v1043 = v1038 = v1043 + v1045
好了，到此，就可以完成简化了，之后就变成了一个for循环里面一条自增的语句，所以就转换成了乘法
手动将这些代码整理好看一点，就长下面这样了
for ( ii = 0; ii < 4; ++i) {
v1043 = ii * 8;
v1169 = &list_a_v19[4 * ii];
input_1 = input + v1043;
input_2 = input + v1043 + 4;
sum = 0;
delta = 3 * 884811923;
key0 = v1169[0];
key1 = v1169[1];
key2 = v1169[2];
key3 = v1169[3];
for ( mm = 0; mm <= 0x1F; mm++ ) {
sum = delta + sum;
v1135 = 16 * input_2;
v1118 = key0 + v1135;
v1112 = sum + input_2;
v1109 = input_2 >> 5;
v1106 = key1 + v1109;
input_1 += v1102;
v1095 = 16 * v1100;
v1078 = key2 + v1095;
v1072 = sum + input_1;
v1069 = input_1 >> 5;
v1066 = key3 + v1069;
input_2 += v1062;
}
v1170[0] = input_1;
v1170[1] = input_2;
}
经过了一些手动处理，得到了上面的伪代码，显然就是TEA呗，第一关就这么过了
v510 = "Th1nkMyfr1end";
v507 = 0;
char v18[256] = {};
v504 = 0;
for ( i5 = 0; i5 < 256; i5++ )
{
v17[i5] = i5;
v18[i5] = v510[i5 % 13];
}
for ( i5 = 0; i5 < 256; i5++ )
{
v1 = v18[i5];
v2 = v17[i5];
v380 = v2 + v507;
v371 = v1 + v380;
v507 = v371 % 256;
v504 = v17[i5];
v17[i5] = v17[v507];
v17[v507] = v504;
}
v511 = 32;
v507 = 0;
i5 = 0;
for ( i17 = 0; v511 > i17; i17++ )
{
i5 = (i5 + 1) % 256; // i = i + 1
v3 = v17[i5]; // S[i]
v507 = (v3 + v507) % 256; // j = (j + S[i]) % 256
v155 = v17[i5];
v17[i5] = v17[v507];
v17[v507] = v155; // S[i], S[j] = S[j], S[i]
v103 = v17[v507] + v17[i5]; // S[i] + S[j]
input[i17] ^= v17[v103 % 256]; // data ^= S[(S[i] + S[j]) % 256]
}
256的SBOX，且仅进行一次异或，果断RC4
中间见到了这样的东西
v100 = v103
v98 = v103 / v120;
v97 = v120;
v96 = v97 * v98; // 去除for循环后
v506 = v100 - v96;
$v103 - (v120 * (v103 / v120)) = v103 - (v103 - (v103 % v120))$，显然就是取模运算了
随后是这个
v1013 = (__int64)input;
v1012 = (__int64)v20;
v1011 = strlen(input);
for ( i31 = 0; i31 < 65; ++i31 )
{
v978 = 3 * 823 * 5; // 12345
v948 = i31 * 0x114514;
v18[i31] = v948 % v978;
}
while ( v1011 > 2 )
{
v6 = *(_BYTE *)v1013 >> 2;
*(_BYTE *)v1012 = v18[v6 & 0x3f];
v1012 += 1;
*(_BYTE *)v1012 = v18[(16 * (v1013[0] & 3)) | (v1013[1] >> 4) & 0x0f];
v1012 += 1;
v818 = 4 * (v1013[1] & 0x0f);
v10 = *(_BYTE *)(v1013 + 2) >> 6;
v804 = 2;
v803 = 1;
v802 = 0;
v801 = 3;
*(_BYTE *)v1012 = v18[v818 | v10 & 3];
v1012 += 1;
v11 = v1013[2];
v5 = (unsigned __int8)v18[v11 & 0x63];
*(_BYTE *)v1012 = v5;
v1012 += 1;
v1011 = ~(~v1011 + 3); // v1011 -= 3
v1013 += 3;
}
if ( v1011 )
{
v12 = *(_BYTE *)v1013 >> 2;
*(_BYTE *)v1012 = v18[v12 & 0x3f];
v1012++;
if ( v1011 <= 1 ) {
v16 = *(_BYTE *)v1013;
v640 = (v16 & 3) << 4;
*(_BYTE *)v1012 = v18[v640];
v1012++;
v586 = 64;
*(_BYTE *)v1012 = v18[v586];
v1012++;
}
else {
v13 = *(_BYTE *)v1013;
v720 = (v13 & 3) << 4;
v14 = *(_BYTE *)(v1013 + 1) >> 4;
*(_BYTE *)v1012 = v18[v720 | v14 & 0xf];
v1012++;
v15 = *(unsigned __int8 *)(v1013 + 1);
v666 = (v15 & 0xf) << 2;
*(_BYTE *)v1012 = v18[v666];
v1012++;
}
v564 = 8;
v548 = 8;
v534 = v548;
v533 = v564;
v532 = 64;
*(_BYTE *)v1012 = (unsigned __int8)v18[v532];
v1012++;
}
第一个for循环是v18的生成，后面是个base64换表换成v18的
根据字符串提示，后面就是check了，但这部分好像反编译不出来
看了下汇编（patch前的忘记存了）
07FF7D3CE9906 lea rcx, aWowThatIsAmazi ; "Wow.....That is amazing.......You actua"...
.text:00007FF7D3CE990D call print
.text:00007FF7D3CE9912 mov [rbp+2A80h+var_14], 0
.text:00007FF7D3CE991C jmp loc_7FF7D3CE9A16
.text:00007FF7D3CE9A16 loc_7FF7D3CE9A16: ; CODE XREF: sub_7FF7D3CE15E2+833A↑j
.text:00007FF7D3CE9A16 nop
.text:00007FF7D3CE9A17 nop
.text:00007FF7D3CE9A18 nop
.text:00007FF7D3CE9A19 nop
.text:00007FF7D3CE9A1A nop
.text:00007FF7D3CE9A1B nop
.text:00007FF7D3CE9A1C nop
.text:00007FF7D3CE9A1D nop
.text:00007FF7D3CE9A1E nop
.text:00007FF7D3CE9A1F nop
.text:00007FF7D3CE9A20 nop
.text:00007FF7D3CE9A21 nop
.text:00007FF7D3CE9A22 nop
.text:00007FF7D3CE9A23 nop
.text:00007FF7D3CE9A24 nop
.text:00007FF7D3CE9A25 nop
.text:00007FF7D3CE9A26 lea rcx, aOkYouWinTheRes ; "Ok you win. The result will be shown la"...
.text:00007FF7D3CE9A2D call print
.text:00007FF7D3CE9A32 mov [rbp+2A80h+var_18], 0
.text:00007FF7D3CE9A3C jmp loc_7FF7D3CE9B1A
本来有一个判断和一个跳转，直接patch掉，中间应该是一些浪费时间的东西，再重新反编译一下，就能看到check部分了
v1272 = 0;
while ( 1 )
{
v37 = 49;
if ( v1272 >= v37 )
break;
if ( *((_BYTE *)v21 + v1272) != *((_BYTE *)off_7FF7D3D02010 + v1272) )
{
print((__int64)"No\n");
return;
}
/* 从内存中取出的数据
unsigned char off_7FF7D3D02010[] =
{
0x06, 0xAB, 0x05, 0x6A, 0xA0, 0x72, 0x71, 0x0D, 0x0A, 0x6F,
0xAC, 0x15, 0x05, 0xA5, 0x76, 0x41, 0x0A, 0x77, 0x13, 0xD8,
0x69, 0x03, 0x14, 0x78, 0xD5, 0xA8, 0x44, 0x0F, 0xA7, 0x76,
0x05, 0xAA, 0xA4, 0x09, 0x69, 0xA7, 0x0B, 0x11, 0x15, 0x42,
0x11, 0x72, 0x14, 0xAD, 0x00, 0x00, 0x00, 0x00
};
*/
v1272 += 1;
}
至此全部分析完毕，依次进行了TEA，RC4和Base64，中间进行了密钥生成，最后做个反向进行解密即可。
补充：静态分析while语句实现的加法运算
之前的分析其实是用python实现一遍，然后找规律得到的（毕竟为了速度），但还是应该稍微静态分析一下具体发生了什么事情
看的时候就感觉很像是数电中的加法器，还是用简单的例子分析一下（删去了没有用到的语句）
v1153 = ll & 1; // 判断结尾是否为1
v1152 = ll ^ 1; // 如果结尾是1，将其变为0
// 如果结尾是0，将其变为1
while ( v1153 ) { // 如果此前结尾为1，将会涉及到进位的问题，因此进入循环
// 如果此前结尾为0，就没有进位的问题了，无需进入循环
v1150 = 2 * v1153; // 将结尾左移1
v1153 = (2 * v1153) & v1152; // 与加法之后的结果再进行一次按位与，这个的目的是看接下来是否还需要进位
v1152 ^= v1150; // 进行无进位加法
} // 什么时候不会产生进位的问题了，什么时候就可以退出循环了
ll = v1152;
简单的说，就是用异或运算作为无进位的加法，然后通过一个while循环来完成进位
vs
这道题就比赛的时候简单看了一下，逆向难度很低，从一个文件读取指令，另一个文件当作内存，vm指令其实不难，但文件中的指令很多，需要手写一个vm的分析代码。
写完之后发现行数略多，先手动分析找了找规律，然后写了个自动化脚本提取，生成python代码，直接拿flag。
vm的解析脚本
vmreader.py:
memory = [
0x0C, 0xF4, 0x5F, 0xE9, 0xF2, 0xE6, 0x87, 0x4C, 0x5E, 0x61, 0x11, 0x7B, 0xF0, 0x11, 0x7F, 0xB4, 0xB2, 0xEB, 0x65, 0xE2, 0x15, 0xC6, 0x8B, 0x02, 0x8C, 0xC1, 0x50, 0xD0, 0x0D, 0xA1, 0xCD, 0x3A
]
cnt = 0
class OPCode:
def __init__(self, code_len, code, arglen, pes_code):
self.code_len = code_len
self.code = code
self.arglen = arglen
self.pes_code = pes_code
class Reader:
def __init__(self, file):
self.index = 0
self.buf = open(file, 'rb').read()
self.length = len(self.buf)
self.asm = []
def add_asm(self, asm: OPCode):
self.asm.append(asm)
def read(self):
global cnt
while len(self.buf) > 0:
for a in self.asm:
if a.code(self.buf[:a.code_len]):
# self.output += a.pes_code
op_code = self.buf[:a.code_len]
self.buf = self.buf[a.code_len:]
if op_code == b'\xff\xff' and self.buf[1] > 2:
print (cnt, op_code)
cnt += 1
break
args = [_ for _ in self.buf[:a.arglen]]
a.pes_code(op_code, args)
self.buf = self.buf[a.arglen:]
break
else:
print (cnt, self.buf[0])
cnt += 1
self.buf = self.buf[1:]
def basic_io_code(op_code):
if op_code == b'\xFF\xFF':
return True
return False
def basic_io_op(op_code, args):
global cnt
if args[1] == 2:
if args[0] > 0x20 and args[0] < 0x7f:
print ('%d print %c' % (cnt, args[0]))
cnt += 2
else:
print ('%d print \\x%02x' % (cnt, args[0]))
cnt += 2
elif args[1] == 1:
print ('%d mem[%d] = <input>' % (cnt, args[0]))
cnt += 2
elif args[1] == 0:
print ('%d exit(0)' % cnt)
cnt += 2
else:
print (op_code, args)
def jmp_code(op_code):
if int.from_bytes(op_code, 'little') & 0x8000 == 0:
return True
return False
def jmp_op(op_code, args):
global cnt
pc = int.from_bytes(op_code, 'little')
addr = pc & 0x1FF
if (addr >> 3) > 31:
if (memory[(addr >> 3) - 32] >> (addr & 7)) & 1 == 0:
print (f'{cnt} goto {cnt + ((pc >> 9) & 0x3f)}')
else:
print (f'{cnt} nop')
else:
print ('%d if ((mem[ %d ] >> %d ) & 1) == 0' % (cnt, addr >> 3, addr & 7), f'goto {cnt+((pc >> 9) & 0x3f)}')
cnt += 1
def jmp2_code(op_code):
if int.from_bytes(op_code, 'little') & 0x8000 != 0 and op_code != b'\xff\xff':
return True
return False
def jmp2_op(op_code, args):
global cnt
pc = int.from_bytes(op_code, 'little')
addr = pc & 0x1FF
if (addr >> 3) > 31:
if (memory[(addr >> 3) - 32] >> (addr & 7)) & 1 != 0:
print (f'{cnt} goto {cnt + ((pc >> 9) & 0x3f)}')
else:
print (f'{cnt} nop')
else:
print ('%d if ((mem[ %d ] >> %d ) & 1) != 0' % (cnt, addr >> 3, addr & 7), f'goto {cnt+((pc >> 9) & 0x3f)}')
cnt += 1
basic_io = OPCode(2, basic_io_code, 2, basic_io_op)
r = Reader('program')
jmp = OPCode(2, jmp_code, 0, jmp_op)
jmp2 = OPCode(2, jmp2_code, 0, jmp2_op)
r.add_asm(basic_io)
r.add_asm(jmp)
r.add_asm(jmp2)
r.read()
分析指令
0 print P
2 print l
4 print e
6 print a
8 print s
10 print e
12 print \x20
14 print i
16 print n
18 print p
20 print u
22 print t
24 print \x20
26 print y
28 print o
30 print u
32 print r
34 print \x20
36 print f
38 print l
40 print a
42 print g
44 print :
46 print \x20
48 mem[0] = <input>
50 mem[1] = <input>
52 mem[2] = <input>
54 mem[3] = <input>
56 mem[4] = <input>
58 mem[5] = <input>
60 mem[6] = <input>
62 mem[7] = <input>
64 mem[8] = <input>
66 mem[9] = <input>
68 mem[10] = <input>
70 mem[11] = <input>
72 mem[12] = <input>
74 mem[13] = <input>
76 mem[14] = <input>
78 mem[15] = <input>
80 mem[16] = <input>
82 mem[17] = <input>
84 mem[18] = <input>
86 mem[19] = <input>
88 mem[20] = <input>
90 mem[21] = <input>
92 mem[22] = <input>
94 mem[23] = <input>
96 mem[24] = <input>
98 mem[25] = <input>
100 mem[26] = <input>
102 mem[27] = <input>
104 mem[28] = <input>
106 mem[29] = <input>
108 mem[30] = <input>
110 mem[31] = <input>
这部分是简单的输出和输入，直接看二进制文件的字节也能看出来
然后是输入的判断部分
112 if ((mem[ 12 ] >> 5 ) & 1) != 0 goto 125
113 nop
114 if ((mem[ 19 ] >> 2 ) & 1) == 0 goto 125
115 print N
117 print o
119 print !
121 print \x0a
123 exit(0)
125 goto 127
126 if ((mem[ 22 ] >> 6 ) & 1) != 0 goto 146
127 goto 131
128 if ((mem[ 1 ] >> 1 ) & 1) != 0 goto 140
129 if ((mem[ 0 ] >> 3 ) & 1) != 0 goto 140
130 b'\xff\xff'
131 goto 133
132 b'\xff\xff'
133 if ((mem[ 30 ] >> 5 ) & 1) == 0 goto 146
134 nop
135 nop
136 print N
138 print o
140 print !
142 print \x0a
144 exit(0)
146 nop
147 if ((mem[ 6 ] >> 4 ) & 1) != 0 goto 169
148 goto 150
149 b'\xff\xff'
150 goto 154
151 if ((mem[ 0 ] >> 4 ) & 1) == 0 goto 163
152 if ((mem[ 3 ] >> 0 ) & 1) != 0 goto 163
153 b'\xff\xff'
154 if ((mem[ 8 ] >> 0 ) & 1) == 0 goto 169
155 goto 159
156 if ((mem[ 1 ] >> 0 ) & 1) == 0 goto 168
157 if ((mem[ 1 ] >> 7 ) & 1) != 0 goto 168
158 b'\xff\xff'
159 print N
161 print o
163 print !
165 print \x0a
167 exit(0)
169 if ((mem[ 4 ] >> 4 ) & 1) != 0 goto 190
170 goto 172
171 b'\xff\xff'
172 if ((mem[ 20 ] >> 0 ) & 1) == 0 goto 190
173 nop
174 b'\xff\xff'
175 if ((mem[ 2 ] >> 1 ) & 1) != 0 goto 179 ; 由于ffff后会直接跳过下一个，所以这一句也没有用
176 goto 180
177 if ((mem[ 1 ] >> 3 ) & 1) != 0 goto 189
178 if ((mem[ 3 ] >> 3 ) & 1) == 0 goto 189
179 b'\xff\xff'
180 print N
182 print o
184 print !
186 print \x0a
188 exit(0)
二进制文件中出现了很多奇奇怪怪的 \xFF\xFF，感觉起到了一部分的花指令作用，所以对于不满足的情况全部拆开处理了，但这又导致读取后的逻辑不是很清晰，需要进行简单的手动分析
程序中
if ((mem[ 1 ] >> 3 ) & 1) != 0之间空格实际上是为了后续进一步读取准备的
分析时可以看出，flag的判断逻辑显然是对输入的每一比特加了限定，目的就是跳过所有的退出
对这一部分手动分析，删掉没有用的部分
112 if ((mem[ 12 ] >> 5 ) & 1) != 0 goto 125
114 if ((mem[ 19 ] >> 2 ) & 1) == 0 goto 125
115 print No!
123 exit(0)
125 goto 127
126 if ((mem[ 22 ] >> 6 ) & 1) != 0 goto 146 ; 这句话也没有用，但自动提取时不容易处理，仍然保留
127 goto 131
131 goto 133
133 if ((mem[ 30 ] >> 5 ) & 1) == 0 goto 146
136 print No!
144 exit(0)
146 nop
147 if ((mem[ 6 ] >> 4 ) & 1) != 0 goto 169
148 goto 150
150 goto 154
154 if ((mem[ 8 ] >> 0 ) & 1) == 0 goto 169
155 goto 159
159 print No!
167 exit(0)
169 if ((mem[ 4 ] >> 4 ) & 1) != 0 goto 190
170 goto 172
172 if ((mem[ 20 ] >> 0 ) & 1) == 0 goto 190
173 nop
176 goto 180
180 print No!
188 exit(0)
可以看到，可用的跳转一定是跳转到exit后面的，这样就可以实现一个自动化脚本了
extract.py
infile = open('1.txt')
code = infile.read()
code = code.split('\n')
target = []
for line in code:
if 'exit' in line:
target.append(str(int(line.split(' ')[0]) + 2))
# print (target)
for line in code:
tmp = line.split(' ')
if tmp[-1] in target:
print (line)
最后再自动生成一个z3脚本
def fmt(in_list):
ret = ''
if in_list[2] == '==':
ret += 'eq('
elif in_list[2] == '!=':
ret += 'neq('
ret += in_list[0] + ', ' + in_list[1]
ret += ')'
return ret
infile = open('2.txt')
print ('''from z3 import *
s = Solver()
flag = [BitVec('flag%d' % i, 8) for i in range(32)]
for f in flag:
s.add(f > 0x20)
s.add(f < 0x7f)
def eq(pos_f, pos_b):
return flag[pos_f] & (1 << pos_b) == 0
def neq(pos_f, pos_b):
return flag[pos_f] & (1 << pos_b) != 0
''')
lines = infile.read()
lines = lines.split('\n')
for i in range(0, len(lines) - 1, 2):
a, b = lines[i], lines[i + 1]
a = a.split(' ')
b = b.split(' ')
a = [a[3], a[6], a[-4]]
b = [b[3], b[6], b[-4]]
print ('s.add(Or(' + fmt(a) + ', ' + fmt(b) + '))')
print ('''
if s.check() == sat:
model = s.model()
for f in flag:
print (chr(model[f].as_long().real), end = '')
print ('\\nfinish')''')
运行之后就可以得到flag了
# python3 vmreader.py > 1.txt
# python3 extract.py > 2.txt
# python3 to_py.py > 3.py
# python3 3.py
flag{_2_SAT_15_a_P_pr0b13M_4F6v}
finish
# ./vs
Please input your flag: flag{_2_SAT_15_a_P_pr0b13M_4F6v}
Congratulation!
通过程序验证
总结
还是第一次在一个逆向题目中写这么多代码，最近又看到一些需要写代码的题目，还是需要提高开发能力啊