GXYCTF2019 simple CPP

https://buuoj.cn/challenges#[GXYCTF2019]simple%20CPP

64 c 艹

程序比较复杂，需要使用动调看程序的逻辑（终于来了，结构分析）

GXY{114514}

动态调试进去看不出来具体内容的时候要进入汇编层面看看才行，在反编译界面看准是哪个寄存器，在汇编界面进入寄存器指的值，Ctrl+E 导出

整个程序的逻辑是先把输入和一个数组循环异或，再把异或后的数据存在 i64 数组里面（大小为 4，大端的方式去存），通过 5 个方程验证数组里的数字是否符合要求

这种一般能 angr 就秒了，奈何实在 Win 下，只能用 z3 一点点往回推了

from z3 import *
 
data_48 = [0x69, 0x5F, 0x77, 0x69, 0x6C, 0x6C, 0x5F, 0x63, 0x68, 0x65,
           0x63, 0x6B, 0x5F, 0x69, 0x73, 0x5F, 0x64, 0x65, 0x62, 0x75,
           0x67, 0x5F, 0x6F, 0x72, 0x5F, 0x6E, 0x6F, 0x74, 0x00]
 
d0, d1, d2, d3 = BitVecs('d0 d1 d2 d3', 64)
 
s = Solver()
 
s.add(d2 & ~d0 == 1176889593874)
s.add(d2 & ~d1 & d0 | d2 & (d1 & d0 | d1 & ~d0 | ~(d1 | d0)) == 577031497978884115)
s.add(d2 & ~d0 | d1 & d0 | d2 & ~d1 | d0 & ~d1 == 4483974544037412639)
s.add(d3 == 842073600)
s.add(d2 & ~d0 | d1 & d0 | d1 & d2 == ~d0 & d2 | 864693332579200012)
 
# 用十六进制输出所有结果
while s.check() == sat:
    m = s.model()
    print(hex(m[d0].as_long()), hex(m[d1].as_long()), hex(m[d2].as_long()), hex(m[d3].as_long()))
    s.add(Or(d0 != m[d0], d1 != m[d1], d2 != m[d2], d3 != m[d3]))
 

得到开始的 dump 为：

0x3e3a460533286f0d 0xc00020130082c0c 0x8020717153e3013 0x32310600

循环异或回去就行了

from z3 import *  
  
data_48 = "i_will_check_is_debug_or_noi_wil"  
  
d0, d1, d2, d3 = BitVecs('d0 d1 d2 d3', 64)  
  
s = Solver()  
  
s.add(d2 & ~d0 == 1176889593874)  
s.add(d2 & ~d1 & d0 | d2 & (d1 & d0 | d1 & ~d0 | ~(d1 | d0)) == 577031497978884115)  
s.add(d2 & ~d0 | d1 & d0 | d2 & ~d1 | d0 & ~d1 == 4483974544037412639)  
s.add(d3 == 842073600)  
s.add(d2 & ~d0 | d1 & d0 | d1 & d2 == ~d0 & d2 | 864693332579200012)  
  
# 用十六进制输出所有结果  
while s.check() == sat:  
    m = s.model()  
    print(hex(m[d0].as_long()), hex(m[d1].as_long()), hex(m[d2].as_long()), hex(m[d3].as_long()))  
    s.add(Or(d0 != m[d0], d1 != m[d1], d2 != m[d2], d3 != m[d3]))  
  
  
# 0x3e3a460533286f0d 0xc00020130082c0c 0x8020717153e3013 0x000000032310600  
# 大端  
dump = [0x3e, 0x3a, 0x46, 0x05, 0x33, 0x28, 0x6f, 0x0d,  
        0xc, 0x00, 0x02, 0x01, 0x30, 0x08, 0x2c, 0x0c,  
        0x8, 0x02, 0x07, 0x17, 0x15, 0x3e, 0x30, 0x13,  
        0x32, 0x31, 0x06]  
  
for i in range(len(dump)):  
    dump[i] ^= ord(data_48[i % 27])  
  
print(''.join([chr(i) for i in dump]))
 

发现 dump1 部分是有很多个解的，在比赛的时候放出来是 e!P0or_a

We1l_D0ne!P0or_algebra_am_i