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}