repwn

2019-03-31

IDA里shift+F12找到“Please Input Your Key_ Now!”，然后找到程序入口“sub_4014C0”（; DATA XREF: sub_4014C0:loc_401588↑o）。

然后输入了一个字符串给v11，sub_4012F0((int)&v11)需要返回1。

sub_4012F0：v2要在*((_BYTE *)&v4 + v2) == *(_BYTE *)(v1 + a1)的情况下从0，++到12，此时若*(_BYTE *)(a1 + 20) == 72则返回1。

v4这样明显超了一字节又强制转成一字节的可以在IDA里对着数值右键，转成16进制取最后两位写进z3。

from z3 import *

d2c = BitVec('d2c', 8)
d20 = BitVec('d20', 8)
d24 = BitVec('d24', 8)
d28 = BitVec('d28', 8)
d34 = BitVec('d34', 8)
d30 = BitVec('d30', 8)
d3c = BitVec('d3c', 8)
d38 = BitVec('d38', 8)

v1 = d2c + 1000*d20 + 100*d24 + 10*d28
v2 = d34 + 10*d30
v3 = d3c + 10*d38

solver = Solver()
solver.add(2*(v1 + v2) == 4040)
solver.add(3*v2/2 + 100*v3 == 115)
solver.add(v1 - 110*v3 == 1900)

while sat == solver.check():
    print(solver.model())
    print('\n-------------')
    solver.add(Or(solver.model()[d2c] != d2c, solver.model()[d20] != d20, solver.model()[d24] != d24, solver.model()[d28] != d28, solver.model()[d34] != d34, solver.model()[d30] != d30, solver.model()[d3c] != d3c, solver.model()[d38] != d38))