SangFor(深育杯)-Reverse(逆向) Press Write up

Posted 2021-12-13 水番正文

当你拥有一台液压机的时候，你将很快拥有液压机。

0x00 日常查壳

0x01 分析主函数

0x02 init_0

0x03 Brian函数的符号执行

于是那么一段

++++++++++[->++++++++++++++++->[-]+++++

其实等式很简单

首先是tmp里虽然那么长一个数组其实就用了3个字节

我把他们分别命名为t1 t2 t3 各位师傅看的时候可以画一下帮助理解

这个等式就是

当是第一个液压机的时候 （ i = 0 )

ef[i] = (160 - f[i]) * 5 + 2

之后的液压机 ( i > 0 )

ef[i] = ( (160 + ef[i]) - f[i] ) * 5 + 2

PS:注意t1 t2 t3都只用了一个字节 可以动调看一下

0x04 GetFlag

本来想了半天&0xFF用C解bangzhu了半天 和队内pwn师傅了了一下突然想起z3可以很轻松解出来

from z3 import *
enflag = [0x60, 0xE1, 0x2F, 0x05, 0x79, 0x80, 0x5E, 0xE1, 0xC5, 0x57, 0x8B, 0xCC, 0x5C, 0x9A, 0x67, 0x26,
        0x1E, 0x19, 0xAF, 0x93, 0x3F, 0x09, 0xE2, 0x97, 0x99, 0x7B, 0x86, 0xC1, 0x25, 0x87, 0xD6, 0x0C,
        0xDD, 0xCF, 0x2A, 0xF5, 0x65, 0x0E, 0x73, 0x59, 0x1D, 0x5F, 0xA4, 0xF4, 0x65, 0x68, 0xD1, 0x3D,
        0xD2, 0x98, 0x5D, 0xFE, 0x5B, 0xEF, 0x5B, 0xCC]
input = [BitVec('input[%d]' % i, 8) for i in range(56)]
#yyj = BitVec('yyj', 8)
s = Solver()

s.add( ((160 - input[0]) * 5 + 2) == enflag[0] )	#第一台液压机
for i in range(1, 56):				#之后的液压机
    s.add( (((160 + enflag[i - 1]) - input[i]) * 5 + 2) == enflag[i] )
    
if sat == s.check():
    ans = s.model()
    
flag = ""
for i in range(56):
    flag += chr(ans[input[i]].as_long())   #as_long()转成整数
print(flag)

拿base64解一下

GetFlag!