卷,我要卷
刷题!复现!!

smokestack

VM题,比较简单,就当入门了

首先是将命令行参数key,放入一个模拟的栈

image-20210807144027772

然后运行vm方法sub_401610

md5取到唯一的key,rc4解密得到flag

下面分析vm

__int16 sub_401610()
{
  _cfltcvt_init(); // vm初始化
  vm_r1 = 0; // 通用寄存器 r1
  vm_r2 = 0; // 通用寄存器 r2
  vm_sp = 9; // 栈顶
  vm_ip = 0; // 计数器
  while ( (unsigned __int16)vm_ip < (int)(unsigned __int16)word_40D000 )
    sub_401540(); // 执行vm
  return vm_r1;
}

vm的初始化在_cfltcvt_init

通过伪代码,大体可以辨认出函数的功能,修改函数名后

void _cfltcvt_init()
{
  vm[0] = (int)op_push;
  vm[1] = (int)op_pop;
  vm[2] = (int)op_add;
  vm[3] = (int)op_sub;
  vm[4] = (int)op_rol;
  vm[5] = (int)op_ror;
  vm[6] = (int)op_xor;
  vm[7] = (int)op_not;
  vm[8] = (int)op_eq;
  vm[9] = (int)op_if;
  vm[10] = (int)op_br;
  vm[11] = (int)op_store;
  vm[12] = (int)op_load;
  vm[13] = (int)op_nop;
}

看到控制程序执行的vm表funcTables

int sub_401540()
{
  unsigned __int16 v1; // [esp+0h] [ebp-4h]

  v1 = funcTables[(unsigned __int16)vm_ip];
  return ((int (__cdecl *)(unsigned __int16))vm[v1])(v1);
}
image-20210807144639427

得到opcode,vm表等一些必要的数据后,写脚本解析出伪汇编代码

funcTables = [0x0000, 0x0021, 0x0002, 0x0000, 0x0091, 0x0008, 0x0000, 0x0016, 0x0000, 0x000C, 0x0009, 0x000A, 0x000B, 0x0000, 0x0000, 0x000C, 0x0002, 0x000C, 0x0000, 0x0000, 0x001D, 0x000A, 0x000B, 0x0000, 0x0000, 0x0063, 0x0002, 0x000C, 0x0000, 0x0000, 0x0018, 0x0006, 0x0000, 0x0054, 0x0008, 0x0000, 0x0033, 0x0000, 0x0029, 0x0009, 0x000A, 0x000B, 0x0000, 0x0000, 0x002C, 0x0002, 0x000C, 0x0000, 0x0000, 0x003D, 0x000A, 0x0000, 0x000E, 0x0001, 0x000B, 0x0000, 0x0000, 0x0059, 0x0002, 0x000C, 0x0000, 0x000B, 0x0000, 0x0000, 0x0000, 0x000C, 0x0001, 0x0000, 0x0009, 0x000C, 0x0000, 0x000B, 0x0001, 0x0000, 0x0002, 0x0002, 0x000C, 0x0001, 0x000B, 0x0000, 0x0000, 0x0001, 0x0003, 0x000C, 0x0000, 0x000B, 0x0000, 0x0000, 0x0000, 0x0008, 0x0000, 0x0047, 0x0000, 0x0060, 0x0009, 0x000A, 0x000C, 0x0000, 0x000B, 0x0001, 0x0003, 0x0000, 0x005D, 0x0008, 0x0000, 0x007C, 0x0000, 0x006E, 0x0009, 0x000A, 0x000B, 0x0000, 0x0000, 0x0007, 0x0003, 0x000C, 0x0000, 0x0000, 0x005B, 0x000C, 0x0001, 0x0000, 0x0087, 0x000A, 0x0000, 0x0036, 0x000C, 0x0001, 0x000B, 0x0000, 0x000B, 0x0001, 0x0002, 0x000C, 0x0001, 0x000B, 0x0001, 0x0000, 0x0058, 0x0002, 0x0006, 0x0000, 0x00F9, 0x0008, 0x0000, 0x00A0, 0x0000, 0x0096, 0x0009, 0x000A, 0x000B, 0x0000, 0x0000, 0x004D, 0x0006, 0x000C, 0x0000, 0x0000, 0x00AE, 0x000A, 0x0000, 0x0323, 0x0000, 0x012B, 0x0003, 0x000C, 0x0001, 0x000B, 0x0000, 0x000B, 0x0001, 0x0002, 0x000C, 0x0001, 0x000C, 0x0001, 0x000B, 0x0001, 0x000B, 0x0001, 0x0000, 0x0001, 0x0003, 0x000C, 0x0001, 0x0000, 0x0003, 0x0002, 0x000B, 0x0001, 0x0000, 0x0000, 0x0008, 0x0000, 0x00B2, 0x0000, 0x00C7, 0x0009, 0x000A, 0x0007, 0x0000, 0xFE77, 0x0008, 0x0000, 0x00D8, 0x0000, 0x00D1, 0x0009, 0x000A, 0x000B, 0x0000, 0x0000, 0x0058, 0x0002, 0x000C, 0x0000, 0x0000, 0x0003, 0x0004, 0x0000, 0x008C, 0x0002, 0x0000, 0x6094, 0x0008, 0x0000, 0x00EE, 0x0000, 0x00E7, 0x0009, 0x000A, 0x000B, 0x0000, 0x0000, 0x00E7, 0x0002, 0x000C, 0x0000, 0x000B, 0x0001, 0x0002, 0x0000, 0x000C, 0x0006, 0x0000, 0x0074, 0x0008, 0x0000, 0x0107, 0x0000, 0x00FD, 0x0009, 0x000A, 0x000B, 0x0000, 0x0000, 0x0009, 0x0003, 0x000C, 0x0000, 0x0000, 0x011D, 0x000A, 0x0000, 0x000A, 0x000C, 0x0001, 0x000B, 0x0001, 0x0000, 0x0001, 0x0003, 0x000C, 0x0001, 0x000B, 0x0001, 0x0000, 0x0000, 0x0008, 0x0000, 0x010B, 0x0000, 0x011D, 0x0009, 0x000A, 0x0000, 0x0006, 0x0005, 0x0000, 0x1DC0, 0x0008, 0x0000, 0x0133, 0x0000, 0x0129, 0x0009, 0x000A, 0x000B, 0x0000, 0x0000, 0x0071, 0x0002, 0x000C, 0x0000, 0x0000, 0x013D, 0x000A, 0x000B, 0x0000, 0x0000, 0x0077, 0x0002, 0x000C, 0x0000, 0x0000, 0x013D, 0x000A, 0x0000, 0x0016, 0x0002, 0x0000, 0x000E, 0x0003, 0x0000, 0x0061, 0x0008, 0x0000, 0x0153, 0x0000, 0x014C, 0x0009, 0x000A, 0x000B, 0x0000, 0x0000, 0x002C, 0x0003, 0x000C, 0x0000, 0x000C, 0x0001, 0x000B, 0x0001, 0x0000, 0x212C, 0x000B, 0x0001, 0x0000, 0x0001, 0x0003, 0x000C, 0x0001, 0x0000, 0x0007, 0x0003, 0x000B, 0x0001, 0x0000, 0x0000, 0x0008, 0x0000, 0x0159, 0x0000, 0x016E, 0x0009, 0x000A, 0x0000, 0x01CA, 0x0006, 0x0000, 0x1FF5, 0x0008, 0x0000, 0x0181, 0x0000, 0x017A, 0x0009, 0x000A, 0x000B, 0x0000, 0x0000, 0x0012, 0x0002, 0x000C, 0x0000, 0x000D]

op_code = ["push","pop","add","sub", "rol", "ror", "xor", "not",  "eq",  "if", "br", "store", "load", "nop"]

regs = [
    "r1",
    "r2",
    "sp",
    "ip"
]

command = ""

ip = 0

while ip < 386:
    command = hex(ip)[2:].zfill(8) + ": "

    cmd = funcTables[ip]

    if cmd < len(op_code):
        command += " " + op_code[cmd]
        if op_code[cmd] == "push":
            ip += 1
            cmd = funcTables[ip]
            command += " " + hex(cmd)

        elif op_code[cmd] in ("store", "load"):
            ip += 1
            cmd = funcTables[ip]
            command += " " + regs[cmd]
    else:
        print("parse error.")
        exit(-1)

    print(command)

    ip += 1

分析伪汇编

r1 = 0
r2 = 0
sp = 9
ip = 0

push : sp += 1
add	 : sp -= 1
eq	 : sp -= 1



00000000:  push 0x21
00000002:  add			; flag[-1] = flag[-1] + 0x21
00000003:  push 0x91
00000005:  eq
00000006:  push 0x16
00000008:  push 0xc
0000000a:  if			; if flag[-1] == 0x91 ? ip->0xc : ip->0x16
0000000b:  br			; jmp	sp->flag[-2]

0000000c:  store r1		; push r1
0000000e:  push 0xc
00000010:  add
00000011:  load r1		; r1 = 0x0 + 0xc
00000013:  push 0x1d
00000015:  br			; jmp 0x1d

00000016:  store r1
00000018:  push 0x63
0000001a:  add
0000001b:  load r1
0000001d:  push 0x18
0000001f:  xor			; flag[-2] = flag[-2] ^ 0x18
00000020:  push 0x54
00000022:  eq			
00000023:  push 0x33
00000025:  push 0x29
00000027:  if			; if flag[-2] == 0x54 ? ip->0x29 : ip->0x33
00000028:  br			; jmp

00000029:  store r1		; push r1 (0xc)
0000002b:  push 0x2c
0000002d:  add	
0000002e:  load r1		; r1 = r1 (0xc) + 0x2c
00000030:  push 0x3d
00000032:  br			; jmp 0x3d
00000033:  push 0xe
00000035:  pop
00000036:  store r1
00000038:  push 0x59
0000003a:  add
0000003b:  load r1
0000003d:  store r1		; push r1 (0xc + 0x2c)

; for 9
0000003f:  push 0x0
00000041:  load r2		; r2 = 0x0
00000043:  push 0x9
00000045:  load r1		; r1 = 0x9
00000047:  store r2
00000049:  push 0x2
0000004b:  add			
0000004c:  load r2		; r2 = r2 + 0x2
0000004e:  store r1
00000050:  push 0x1
00000052:  sub
00000053:  load r1		; r1 = r1 - 0x1
00000055:  store r1
00000057:  push 0x0
00000059:  eq
0000005a:  push 0x47
0000005c:  push 0x60
0000005e:  if			; if r1 == 0x00 ? 0x60 : 0x47
0000005f:  br

00000060:  load r1		; r1 = flag[-3]
00000062:  store r2		; push r2 (9 * 0x2)
00000064:  sub
00000065:  push 0x5d
00000067:  eq			
00000068:  push 0x7c
0000006a:  push 0x6e
0000006c:  if			; flag[-3] - r2 == 0x5d ? ip->0x6e : ip->0x7c
0000006d:  br			; jmp

0000006e:  store r1		; push r1
00000070:  push 0x7
00000072:  sub			
00000073:  load r1		; r1 = flag[-3] - 0x7
00000075:  push 0x5b
00000077:  load r2		; r2 = 0x5b
00000079:  push 0x87
0000007b:  br			; jmp 0x87

0000007c:  push 0x36
0000007e:  load r2
00000080:  store r1
00000082:  store r2
00000084:  add
00000085:  load r2
00000087:  store r2		; push r2 (0x5b)
00000089:  push 0x58
0000008b:  add
0000008c:  xor
0000008d:  push 0xf9
0000008f:  eq
00000090:  push 0xa0
00000092:  push 0x96
00000094:  if			; (r2 + 0x58) ^ flag[-4] ==  0xf9 ? ip->0x96 : ip->0xa0
00000095:  br

00000096:  store r1		; push r1 (flag[-3] - 0x7)
00000098:  push 0x4d
0000009a:  xor
0000009b:  load r1		; r1 = (flag[-3] - 0x7) ^ 0x4d
0000009d:  push 0xae
0000009f:  br			; jmp 0xae

000000a0:  push 0x323
000000a2:  push 0x12b
000000a4:  sub
000000a5:  load r2
000000a7:  store r1
000000a9:  store r2	
000000ab:  add
000000ac:  load r2

000000ae:  load r2		; r2 = flag[-5]
000000b0:  store r2		; push r2

; for flag[-5] = 4 * flag[-5]
000000b2:  store r2		; push r2
000000b4:  push 0x1
000000b6:  sub
000000b7:  load r2		; r2 = r2 - 0x1
000000b9:  push 0x3
000000bb:  add
000000bc:  store r2		; push r2
000000be:  push 0x0
000000c0:  eq			
000000c1:  push 0xb2
000000c3:  push 0xc7
000000c5:  if
000000c6:  br			; r2 == 0x0 ? ip->0xc7 : ip-> 0xb2

000000c7:  not			; ~flag[-5]
000000c8:  push 0xfe77
000000ca:  eq
000000cb:  push 0xd8
000000cd:  push 0xd1
000000cf:  if
000000d0:  br			; ~flag[-5] == 0xfe77 ? ip->0xd1 : ip->0xd8

000000d1:  store r1		; push r1
000000d3:  push 0x58
000000d5:  add
000000d6:  load r1		; r1 = (flag[-3] - 0x7) ^ 0x4d + 0x58
000000d8:  push 0x3
000000da:  rol
000000db:  push 0x8c
000000dd:  add
000000de:  push 0x6094
000000e0:  eq
000000e1:  push 0xee
000000e3:  push 0xe7
000000e5:  if			; flag[-6] << 3 + 0x8c == 0x6094 ? ip->0xe7 : ip->0xee
000000e6:  br

000000e7:  store r1		; push r1
000000e9:  push 0xe7
000000eb:  add
000000ec:  load r1		; r1 = (flag[-3] - 0x7) ^ 0x4d + 0x58 + 0xe7
000000ee:  store r2		; push r2 (0)
000000f0:  add
000000f1:  push 0xc
000000f3:  xor
000000f4:  push 0x74
000000f6:  eq
000000f7:  push 0x107
000000f9:  push 0xfd
000000fb:  if			; (flag[-7] + r2) ^ 0xc == 0x74 ? ip->0xfd : ip->0x107
000000fc:  br

000000fd:  store r1		; push r1
000000ff:  push 0x9
00000101:  sub
00000102:  load r1		; r1 = (flag[-3] - 0x7) ^ 0x4d + 0x58 + 0xe7 - 0x9
00000104:  push 0x11d
00000106:  br			; jmp 0x11d

00000107:  push 0xa
00000109:  load r2
0000010b:  store r2
0000010d:  push 0x1
0000010f:  sub
00000110:  load r2
00000112:  store r2
00000114:  push 0x0
00000116:  eq
00000117:  push 0x10b
00000119:  push 0x11d
0000011b:  if
0000011c:  br

0000011d:  push 0x6
0000011f:  ror
00000120:  push 0x1dc0
00000122:  eq
00000123:  push 0x133
00000125:  push 0x129
00000127:  if			; flag[-8] >> 0x6 == 0x1dc0 ? ip->0x129 : ip->0x133
00000128:  br

00000129:  store r1		; push r1
0000012b:  push 0x71
0000012d:  add
0000012e:  load r1		; r1 = (flag[-3] - 0x7) ^ 0x4d + 0x58 + 0xe7 - 0x9 + 0x71
00000130:  push 0x13d
00000132:  br			; jmp 0x13d

00000133:  store r1
00000135:  push 0x77
00000137:  add
00000138:  load r1
0000013a:  push 0x13d
0000013c:  br

0000013d:  push 0x16
0000013f:  add
00000140:  push 0xe
00000142:  sub
00000143:  push 0x61
00000145:  eq
00000146:  push 0x153
00000148:  push 0x14c
0000014a:  if			; flag[-9] + 0x16 - 0xe == 0x61 ? ip->0x14c : ip->0x153
0000014b:  br

0000014c:  store r1		; push r1
0000014e:  push 0x2c
00000150:  sub
00000151:  load r1		; r1 = (flag[-3] - 0x7) ^ 0x4d + 0x58 + 0xe7 - 0x9 + 0x71 - 0x2c
00000153:  load r2		; r2 = flag[-10]
00000155:  store r2		; push r2 (flag[-10])
00000157:  push 0x212c

; for xorFlag = 0x212c - 0x7 * flag[-10]
00000159:  store r2		; push r2
0000015b:  push 0x1
0000015d:  sub
0000015e:  load r2		; r2 = r2 - 0x1
00000160:  push 0x7
00000162:  sub
00000163:  store r2
00000165:  push 0x0
00000167:  eq
00000168:  push 0x159
0000016a:  push 0x16e
0000016c:  if			; r2 == 0 ? ip->0x16e : ip->0x159
0000016d:  br

0000016e:  push 0x1ca
00000170:  xor
00000171:  push 0x1ff5
00000173:  eq
00000174:  push 0x181
00000176:  push 0x17a
00000178:  if			; flag[-10] ^ 0x1ca == 0x1ff5 ? ip->0x17a : ip->0x181
00000179:  br
0000017a:  store r1
0000017c:  push 0x12
0000017e:  add
0000017f:  load r1
00000181:  nop

理解这一运行过程,就可以慢慢还原

def op_not(value: int):
    return ~value & 0x0ffff


def op_ror(value: int, dest: int):
    return ((value >> (16 - dest)) | value << dest) & 0x0ffff


def op_rol(value: int, dest: int):
    return ((value << (16 - dest)) | value >> dest) & 0x0ffff



flag = [""] * 10
flag[-1] = chr(0x91 - 0x21)
flag[-2] = chr(0x54 ^ 0x18)
flag[-3] = chr(9 * 0x2 + 0x5d)
flag[-4] = chr((0x5b + 0x58) ^ 0xf9)
flag[-5] = chr(op_not(0xfe77) >> 2)
flag[-6] = chr(op_ror(0x6094 - 0x8c, 3))
flag[-7] = chr(0x74 ^ 0xc)
flag[-8] = chr(op_rol(0x1dc0, 0x6))
flag[-9] = chr(0x61 + 0xe - 0x16)
flag[-10] = chr(int(((0x1ff5 ^ 0x1ca) - 0x212c) / -7))
print("".join(flag))

最后得到命令行参数key:kYwxCbJoLp

一些小问题

形似 1100 0001这类最高位二进制为1的数,进行逻辑左移时会发现并不会移除1,只会为最低位添加0

1000 0101 << 3 = 1000 0101 000

simple CPP

这道题当初刚入门的时候做到直接跳过了,最近复现了红帽杯的file_store大受刺激,C++逆向菜的扣脚……所以拿它来练手了

说是C++逆向,准确的说是逆向算法 :)

前面对输入文本进行了一些限制

image-20210805205111664

第一部分的处理

if ( length )
  {
    j = 0i64;
    do
    {
      v9 = Block; // 输入的文本
      if ( v41 >= 16 )
        v9 = (void **)Block[0];
      v10 = &iwill___; // 后面会提到,这是在初始化的过程中产生的异或key
      if ( (unsigned __int64)qword_140006060 >= 0x10 )
        v10 = (void **)iwill___;
      xorflag[j] = *((_BYTE *)v9 + j) ^ *((_BYTE *)v10 + i % 27);
      ++i;
      ++j;
    }
    while ( i < length );
  }

分析后发现,异或的key为iwill___,查看交叉引用会发现,程序初始化的过程中会给其赋值,其值就是异或的Key

image-20210805205556978

再进行一些格式的条件限制后,看到其进行了数据的堆叠,简单的来讲就是将异或后的数据转换成了十六进制的表示办法。以8位字符为间隔分别赋值v14v13v12,而v11理所当然是数据的最后一部分。

 v16 = xorflag;
  do
  {
    v17 = *v16 + v11;
    ++v15;
    ++v16;
    switch ( v15 )
    {
      case 8:
        v14 = v17;
        goto LABEL_23;
      case 16:
        v13 = v17;
        goto LABEL_23;
      case 24:
        v12 = v17;
LABEL_23:
        v17 = 0i64;
        break;
      case 32:
        sub_1400019C0(std::cout, (__int64)"ERRO,out of range");
        exit(1);
    }
    v11 = v17 << 8;
  }
  while ( v15 < (int)length );

下面就看到了第二层算法

if ( v14 )
  {
    v18 = (__int64 *)operator new(0x20ui64);
    *v18 = v14;
    v18[1] = v13;
    v18[2] = v12;
    v18[3] = v11;
    goto LABEL_28;
  }
LABEL_27:
  v18 = 0i64;
LABEL_28:
  v38 = v18[2];
  v19 = v18[1];
  v20 = *v18;
  v21 = (__int64 *)operator new(0x20ui64);
  IsDebuggerPresent();                          // 反调试
  v22 = v19 & v20;
  *v21 = v19 & v20;                             // v21[0] = v18[1] & v18[0]
  v23 = v38 & ~v20;
  v21[1] = v23;                                 // v21[1] = v18[2] & ~v18[0]
  v24 = ~v19;
  v25 = v38 & v24;
  v21[2] = v38 & v24;                           // v21[2] = v18[2] & ~v18[1]
  v26 = v20 & v24;
  v21[3] = v26;                                 // v21[3] = v18[0] & ~v18[1]
  if ( v23 != 0x11204161012i64 )                // v23 = v21[1] = 0x11204161012i64
  {
    v21[1] = 0i64;
    v23 = 0i64;
  }
  v27 = v23 | v22 | v25 | v26;                  // v27 = v21[1] | v21[0] | v21[2] | v21[3] = 0x3E3A4717373E7F1F
  v28 = v18[1];
  v29 = v18[2];
  v30 = v25 & *v18 | v29 & (v22 | v28 & ~*v18 | ~(v28 | *v18));// v30 = v21[2] & v18[0] | v18[2] & (v21[0] | v18[1] & ~v18[0] | ~(v18[1] | v18[0])) = 0x8020717153E3013
  v31 = 0;
  if ( v30 == 0x8020717153E3013i64 )
    v31 = v27 == 0x3E3A4717373E7F1Fi64;
  if ( (v27 ^ v18[3]) == 0x3E3A4717050F791Fi64 )// v18[3] == 0x32310600
    v3 = v31;
  if ( (v23 | v22 | v28 & v29) == (~*v18 & v29 | 0xC00020130082C0Ci64) && v3 )// (0x11204161012 | v21[0] | v18[1] & v18[2]) == (~v18[0] & v18[2] | 0xC00020130082C0C)
  {
    v32 = sub_1400019C0(std::cout, (__int64)"Congratulations!flag is GXY{");
    v33 = Block;
    if ( v41 >= 0x10 )
      v33 = (void **)Block[0];
    v34 = (__int64 *)sub_140001FD0(v32, v33, length);
    sub_1400019C0(v34, (__int64)"}");
    j_j_free(xorflag);
  }
  else
  {
    sub_1400019C0(std::cout, (__int64)"Wrong answer!try again");
    j_j_free(xorflag);
  }

按顺序将字符串转换后的数值放入v18,然后做了一堆的符号运算……

整理一下,列举出条件,可以例举出四个方程,看到四个未知数

v18[3] = 0x32310600
## 以下条件
v18[2] & ~v18[0] = 0x11204161012
(v18[2] & ~v18[0]) | (v18[1] & v18[0]) | (v18[2] & ~v18[1]) | (v18[0] & ~v18[1]) = 0x3E3A4717373E7F1F
v18[2] & ~v18[1]) & v18[0] | v18[2] & ((v18[1] & v18[0]) | v18[1] & ~v18[0] | ~(v18[1] | v18[0])) = 0x8020717153E3013
(0x11204161012 | (v18[1] & v18[0]) | v18[1] & v18[2]) = (~v18[0] & v18[2] | 0xC00020130082C0C)

尝试使用z3求解

import z3


v18 = [z3.BitVec("v18{0}".format(i), 64) for i in range(4)]

solver = z3.Solver()
solver.add(v18[2] & ~v18[0] == 0x11204161012)
solver.add((v18[2] & ~v18[0]) | (v18[1] & v18[0]) | (v18[2] & ~v18[1]) | (v18[0] & ~v18[1]) == 0x3E3A4717373E7F1F)
solver.add((v18[2] & ~v18[1]) & v18[0] | v18[2] & ((v18[1] & v18[0]) | v18[1] & ~v18[0] | ~(v18[1] | v18[0])) == 0x8020717153E3013)
solver.add((0x11204161012 | (v18[1] & v18[0]) | v18[1] & v18[2]) == (~v18[0] & v18[2] | 0xC00020130082C0C))

chunk = [0] * 4
if solver.check() == z3.sat:
    model = solver.model()
    print(model)

发现是可以求出来值的,下面转回xorflag,然后执行异或即可

### Author: Mas0n
### Date: 2021-08-05 21:15
### Blog: blog.shi1011.cn

import z3

v18 = [z3.BitVec("v18{0}".format(i), 64) for i in range(4)]

solver = z3.Solver()
solver.add(v18[2] & ~v18[0] == 0x11204161012)
solver.add((v18[2] & ~v18[0]) | (v18[1] & v18[0]) | (v18[2] & ~v18[1]) | (v18[0] & ~v18[1]) == 0x3E3A4717373E7F1F)
solver.add((v18[2] & ~v18[1]) & v18[0] | v18[2] & ((v18[1] & v18[0]) | v18[1] & ~v18[0] | ~(v18[1] | v18[0])) == 0x8020717153E3013)
solver.add((0x11204161012 | (v18[1] & v18[0]) | v18[1] & v18[2]) == (~v18[0] & v18[2] | 0xC00020130082C0C))

chunk = [0] * 4
if solver.check() == z3.sat:
    model = solver.model()

    chunk[0] = hex(model[v18[0]].as_long())[2:].rjust(16, "0")
    chunk[2] = hex(model[v18[2]].as_long())[2:].rjust(16, "0")
    chunk[1] = hex(model[v18[1]].as_long())[2:].rjust(16, "0")
    chunk[3] = "323106"
    xorflag = "".join(chunk)
    xorflag = b"".fromhex(xorflag)

    key = "i_will_check_is_debug_or_not"
    flag = []
    for i in range(len(xorflag)):
        flag.append(chr(xorflag[i] ^ ord(key[i % 27])))

    print("".join(flag))


print("end solver")

但是实际上,此题并不是唯一解,也不是唯二解……看了网上的题解后知道赛时提供了乱码部分e!P0or_a

flag = "".join(flag)
print(flag.replace(flag[8:16], "e!P0or_a"))