repwn

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))

如无特殊声明,本页内容采用 CC BY-NC 4.0 授权