经gpt观察后发现，每 4 字节的第 1 个字节都像是被异或了 0x44。

with open(‘Driver.sys’, ‘rb’) as f:raw bytearray(f.read())repaired bytearray(raw)for i in range(0, len(repaired), 4):repaired[i] ^ 0x44with open(‘Driver_repaired.sys’, ‘wb’) as f:f.write(repaired)按这个规律恢复后Driver.sys 重新变成正常 PE 驱动并能看到关键字符串??\DeviceDrive\Device\MYDEVICEflag is you inputwrong真正缺失的符号是 Drive并且 Drive的md5刚好是f2c6151d6c0d99f3666129b97e2100f5再把exe修改好然后回到Driver.sys看看哪里引用了flag is you inputfor ( 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; // [rsp20h] [rbp-28h]char n52_1; // [rsp21h] [rbp-27h]char n52_2; // [rsp22h] [rbp-26h]int n32_3; // [rsp24h] [rbp-24h]int n32_2; // [rsp28h] [rbp-20h]_BYTE *PoolWithTag; // [rsp30h] [rbp-18h]int n32_1; // [rsp58h] [rbp10h]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]shiftE0x66,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重新梳理下逻辑第一轮从前往后每个字节跟前一个字节或初始值 0x34XORtmp[0] in[0] ^ 0x34 ← 第0个字节用初始值 0x34tmp[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]第二轮从前往后每个字节跟前一个字节或 in31XORout[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)看 out1in[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] ^ 0x34out[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尝试借助刚学的z3from 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() satm 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() satm 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() satm 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}