with open(‘Driver.sys’, ‘rb’) as f:
raw = bytearray(f.read())
repaired = bytearray(raw)
for i in range(0, len(repaired), 4):
repaired[i] ^= 0x44
with open(‘Driver_repaired.sys’, ‘wb’) as f:
f.write(repaired)
按这个规律恢复后，Driver.sys 重新变成正常 PE 驱动，并能看到关键字符串：
??\DeviceDrive
\Device\MYDEVICE
flag is you input
wrong
真正缺失的符号是 Drive，并且 Drive的md5刚好是f2c6151d6c0d99f3666129b97e2100f5
再把exe修改好
然后回到Driver.sys，看看哪里引用了flag is you input
for ( i = 0; i < v5; ++i )
*((_BYTE *)buf + (int)i) = Format[i];
for ( n32 = 1; n32 < 32; ++n32 )
*((_BYTE)buf + n32 - 1) ^= (unsigned __int8)(((_BYTE *)buf + n32 - 1) % 0x12u + *((_BYTE *)buf + n32) + 5) ^ 0x34;
if ( (unsigned int)sub_140001000(buf, 32) )
{
strcpy(Format, “flag is you input”);
Irp_1->IoStatus.Information = 18;
DbgPrint(&Format__2);
}
跟踪sub_140001000
__int64 __fastcall sub_140001000(__int64 buf, __int64 n32)
{
char n52; // [rsp+20h] [rbp-28h]
char n52_1; // [rsp+21h] [rbp-27h]
char n52_2; // [rsp+22h] [rbp-26h]
int n32_3; // [rsp+24h] [rbp-24h]
int n32_2; // [rsp+28h] [rbp-20h]
_BYTE *PoolWithTag; // [rsp+30h] [rbp-18h]
int n32_1; // [rsp+58h] [rbp+10h]
n32_1 = n32;
PoolWithTag = ExAllocatePoolWithTag(NonPagedPool, 0x100u, 0x504F4F4Cu);
n52 = 52;
for ( n32_2 = 0; n32_2 < n32_1; ++n32_2 )
{ //每一个字节都是和上一个原始字节进行异或
n52_1 = *(_BYTE *)(buf + n32_2);
PoolWithTag[n32_2] = n52 ^ n52_1;
n52 = n52_1;
}
for ( n32_3 = 0; n32_3 < n32_1; ++n32_3 )
{
n52_2 = PoolWithTag[n32_3];
PoolWithTag[n32_3] = n52 ^ n52_2;
n52 = n52_2;
if ( (unsigned __int8)PoolWithTag[n32_3] != byte_140003000[n32_3] )
return 0;
}
return 1;
}
两次链式异或，结果与byte_140003000[n32_3]比较
去找byte_140003000[n32_3]
shift+E
0x66,0xA,0x9,0xE0,0xE2,0xE3,0xCB,0x9,0x14,0x15,0xC,0x38,0x1,0x1F,0x5,0x42,0x71,0x6E,0x56,0x7A,0x0,0x20,0xE4,0xBF,0xE6,0xCD,0x28,0x30,0x2C,0x75,0xA0,0x3A
重新梳理下逻辑
第一轮：从前往后，每个字节跟前一个字节（或初始值 0x34）XOR
tmp[0] = in[0] ^ 0x34 ← 第0个字节用初始值 0x34
tmp[1] = in[1] ^ in[0] ← 第1个字节用 in[0]
tmp[2] = in[2] ^ in[1] ← 第2个字节用 in[1]
tmp[3] = in[3] ^ in[2]
…
tmp[31] = in[31] ^ in[30]
第二轮：从前往后，每个字节跟前一个字节（或 in31）XOR
out[0] = tmp[0] ^ in[31] ← 第0个字节用 in[31]
out[1] = tmp[1] ^ tmp[0] ← 第1个字节用 tmp[0]
out[2] = tmp[2] ^ tmp[1] ← 第2个字节用 tmp[1]
out[3] = tmp[3] ^ tmp[2]
…
out[31] = tmp[31] ^ tmp[30]
我们把第一轮的公式代入第二轮去
out[0] = (in[0] ^ 0x34) ^ in[31]
out[1] = (in[1] ^ in[0]) ^ (in[0] ^ 0x34)
看 out1：in[0] 出现了两次，XOR 抵消了！
out[1] = in[1] ^ 0x34
继续：
out[2] = (in[2] ^ in[1]) ^ (in[1] ^ in[0])
= in[2] ^ in[0] ← in[1] 抵消了
out[3] = (in[3] ^ in[2]) ^ (in[2] ^ in[1])
= in[3] ^ in[1] ← in[2] 抵消了
out[4] = (in[4] ^ in[3]) ^ (in[3] ^ in[2])
= in[4] ^ in[2] ← in[3] 抵消了
最后：
out[31] = (in[31] ^ in[30]) ^ (in[30] ^ in[29])
= in[31] ^ in[29] ← in[30] 抵消了
合并后的完整公式：
out[0] = in[0] ^ 0x34 ^ in[31]
out[1] = in[1] ^ 0x34
out[2] = in[2] ^ in[0]
out[3] = in[3] ^ in[1]
out[4] = in[4] ^ in[2]
out[5] = in[5] ^ in[3]
…
out[31] = in[31] ^ in[29]
out已知，可以推出in
尝试借助刚学的z3
from z3 import *
s = Solver()
out=[0x66, 0xA, 0x9, 0xE0, 0xE2, 0xE3, 0xCB, 0x9, 0x14, 0x15, 0xC, 0x38, 0x1, 0x1F, 0x5, 0x42, 0x71, 0x6E, 0x56, 0x7A, 0x0, 0x20, 0xE4, 0xBF, 0xE6, 0xCD, 0x28, 0x30, 0x2C, 0x75, 0xA0, 0x3A]
inn=[BitVec(f’x_{i}', 8) for i in range(32)]
s.add(
out[0] == inn[0] ^ 0x34 ^ inn[31],
out[1] == inn[1] ^ 0x34,
)
for i in range(2, 32):
s.add(out[i] == inn[i] ^ inn[i-2])
assert s.check() == sat
m = s.model()
flag = bytes([m.eval(inn[i]).as_long() for i in range(32)])
print(list(flag))
输出
[47, 62, 38, 222, 196, 61, 15, 52, 27, 33, 23, 25, 22, 6, 19, 68, 98, 42, 52, 80, 52, 112, 208, 207, 54, 2, 30, 50, 50, 71, 146, 125]
别忘了在sub_140001000的两次异或前还有一次处理
简化一下代码
buf[n32-1] ^= (buf[n32-1] % 18 + buf[n32] + 5) ^ 0x34;
自己除以18，加5，加下一位，与0x34异或，再与自己异或，赋值给自己
from z3 import *
s = Solver()
buf_new=[47, 62, 38, 222, 196, 61, 15, 52, 27, 33, 23, 25, 22, 6, 19, 68, 98, 42, 52, 80, 52, 112, 208, 207, 54, 2, 30, 50, 50, 71, 146, 125]
buf_old=[BitVec(f’x_{i}', 8) for i in range(32)]
for n32 in range(1,32):
s.add(
buf_new[n32-1] == (buf_old[n32-1] % 18 + buf_old[n32] + 5) ^ 0x34 ^ buf_old[n32-1]
)
assert s.check() == sat
m = s.model()
flag = bytes([m.eval(buf_old[i]).as_long() for i in range(32)])
print(flag.hex())
但是发现这个输出很奇怪，转换成字符是乱码
我们加一段代码看是不是有多解
s.add(Or([buf_old[i] != m[buf_old[i]] for i in range(32)]))
if s.check() == sat:
print(“many”)
m2 = s.model()
else:
print(“only one”)
输出many说明有多解，我们再加一些关于输出格式为flag的限制
限制第一个字符为f(0x66)
最终脚本
from z3 import *
s = Solver()
buf_new=[47, 62, 38, 222, 196, 61, 15, 52, 27, 33, 23, 25, 22, 6, 19, 68, 98, 42, 52, 80, 52, 112, 208, 207, 54, 2, 30, 50, 50, 71, 146, 125]
buf_old=[BitVec(f’x_{i}', 8) for i in range(32)]
for n32 in range(1,32):
s.add(
buf_new[n32-1] == (buf_old[n32-1] % 18 + buf_old[n32] + 5) ^ 0x34 ^ buf_old[n32-1],
buf_old[0]==0x66
)
assert s.check() == sat
m = s.model()
flag = bytes([m.eval(buf_old[i]).as_long() for i in range(32)])
print(flag)
s.add(Or([buf_old[i] != m[buf_old[i]] for i in range(32)]))
if s.check() == sat:
print(“many”)
m2 = s.model()
else:
print(“only one”)
flag{wnNCZJbBOqL3QA1C1cypiKYII4}
