BUUCTF simple Cpp

发布时间 2023-07-07 14:41:20作者: zydt10

simple Cpp

 
有两个难点,第一个就是字节叠加的判断,第二个是一堆莫名其妙的运算的化简
还有一些其他稀碎的难点,例如第一次加密,以及程序流程的分析
整个程序很长,分析出flag的流程比较麻烦
 
比较常规的异或加密
判断长度
字节叠加的操作,第一次见
特征就是会不停累加,并且有左位移的操作
这里是判断读入的flag够不够长度,以及反调试
化简运算
把他化简为z3能求解的几个条件
 
思路:
解出一堆莫名其妙的运算之后
复原回dec
用enc和dec异或得到flag
 
 
cv过来后把c的格式修改为python的格式方便使用z3库求解
v21=0
v22=0
v42=0
'''
v42 = m[2];
v21 = m[1];
v22 = *m;
 
我们需要得到这三个的值 就可以倒推flag了
而这三个需要满足经过下面的运算后  if条件的判断是成立的
 
'''
m=0
 
y = v21 & v22
v23 = v21 & v22
x = v42 & ~v22
v23[1] = x
v27 = ~v21
v28 = v42 & v27
v23[2] = v42 & v27
v29 = v22 & v27
v23[3] = v29
if (x != 0x11204161012):
    v23[1] = 0
    x = 0
v30 = x | y | v28 | v29
z = m[1]
n = m[2]
v33 = v28 & m | n & (y | z & ~m | ~(z | m))
v34 = 0
if (v33 == 0x8020717153E3013):
    v34 = v30 == 0x3E3A4717373E7F1F
if ((v30 ^ m[3]) == 0x3E3A4717050F791F):
    l = v34
if ((x | y | z & n) == (~m & n | 0xC00020130082C0C) & l):
    print("bingo!")

 

 
逻辑还是很乱,再继续修改化简
from z3 import *
s=Solver()
m0,m1,m2,m3=BitVecs('m0 m1 m2 m3',64)
 
s.add((m2 & ~m0)==1176889593874)
s.add((( m2 & ~m1) & m0 | m2 & ((m1 & m0) | m1 & ~m0 | ~(m1 | m0))) == 577031497978884115)
s.add(((m2 & ~m0) | (m1 & m0) | ( m2 & ~m1) | (m0 & ~m1)) ==4483974544037412639)
s.add(m3^4483974544037412639==4483974543195470111)
s.add(((m2 & ~m0) | (m1 & m0) | m1 & m2) == (~m0 & m2 | 864693332579200012))
 
if s.check()==sat:
    print(s.model())
    '''
[m3 = 842073600,
 m1 = 864693332579200012,
 m0 = 4483973367147818765,
 m2 = 577031497978884115]
'''
m = s.model()
for i in m:
    print("%s = 0x%x"%(i,m[i].as_long()))
#这里因为m1有多个解,z3库解出来的这个不是flag要求的那个,所以比赛时就给了正确的那个m1解“e!P0or_a”
enc=[0x3e,0x3a,0x46,0x05,0x33,0x28,0x6f,0x0d,0x1,0x08,0x48,0x00,0x00,0x80,0x00,0x04,0x8,0x02,0x07,0x17,0x15,0x3e,0x30,0x13,0x32,0x31,0x06,0x00]
flag=''
str='i_will_check_is_debug_or_not'
for i in range(len(enc)-1):
    flag+=chr(enc[i]^ord(str[i%27]))
print(flag)
#从We1l_D0n后开始把m+k_és[改成e!P0or_a即是最后的flag
#flag{We1l_D0ne!P0or_algebra_am_i}