64 lines
1.2 KiB
Python
64 lines
1.2 KiB
Python
from z3.z3 import *
|
|
from ctypes import c_uint32
|
|
|
|
|
|
def int32(val):
|
|
return c_uint32(val).value
|
|
|
|
|
|
a = 1103515245
|
|
c = 12345
|
|
m = 2147483647
|
|
seed = int32(1337)
|
|
seeds = []
|
|
STATE = [0x1e48add6, 0xaaa7550c, 0x18df53bf, 0xe6af1116]
|
|
|
|
start = [0x0, 0x0, 0x0, 0x0]
|
|
|
|
for i in range(2 * 4):
|
|
seed = int32((int32(int32(int32(a) * int32(seed)) + int32(c)) % m))
|
|
seeds.append(seed)
|
|
print(hex(seed))
|
|
|
|
|
|
s = Solver()
|
|
|
|
user_input = BitVecs("ui0 ui1 ui2 ui3", 32)
|
|
|
|
for i in range(4):
|
|
start[i] |= user_input[(i * 4)] << 24
|
|
start[i] |= user_input[(i * 4)+1] << 16
|
|
start[i] |= user_input[(i * 4)+2] << 8
|
|
start[i] |= user_input[(i * 4)+3] << 0
|
|
|
|
for i in range(4):
|
|
temp = start[i]
|
|
temp *= 0xcafebeef
|
|
temp += seeds[i*2]
|
|
temp *= 0xfacefeed
|
|
temp ^= seeds[i*2+1]
|
|
|
|
s.add(STATE[i] == temp)
|
|
|
|
while s.check() == sat:
|
|
m = s.model()
|
|
block = []
|
|
for var in m:
|
|
block.append(var() != m[var])
|
|
s.add(Or(block))
|
|
|
|
string = ""
|
|
for i in range(4):
|
|
string += m[user_input[i]].as_string()
|
|
temp = int32(0x61626364 * 0xcafebeef)-seeds[i]
|
|
|
|
print(f"x * 0xcafebeef = {hex(temp)}")
|
|
|
|
print(m)
|
|
# print(string)
|
|
for i in range(int(len(string)/2)):
|
|
print(chr(int(string[i*2:i*2+2], 16)), end="")
|
|
|
|
|
|
|