40 lines
1.2 KiB
Python
40 lines
1.2 KiB
Python
from z3 import *
|
|
|
|
flag_data = [72571,144964,217224,289496,361110,433332,502467,574096,645273,716520,792891,858024,925756,995232,1070055,1137952,1209193,1292004,1349513,1414840,1473885,1560372,1617866,1714032,1744800,1852864,1876770,1983016,2014108,2089260,2160607,2225216,2339469,2408560,2418745,2515320,2597400,2604444,2697669,2705680]
|
|
|
|
solver = Solver()
|
|
|
|
# Create 41 symbolic bytes
|
|
passwd = [BitVec(f'p{i}', 8) for i in range(40)]
|
|
|
|
|
|
# Add ASCII printable constraints for all
|
|
for p in passwd:
|
|
solver.add(p >= 32, p <= 126)
|
|
|
|
# Apply known format: GPNCTF{.....}
|
|
known = b"GPNCTF{"
|
|
for i, c in enumerate(known):
|
|
solver.add(passwd[i] == c)
|
|
solver.add(passwd[39] == ord('}'))
|
|
|
|
# Implement compute_secret logic
|
|
for index in range(40):
|
|
total = flag_data[index]
|
|
for pass_char in range(40):
|
|
multi = index + pass_char + index * pass_char + 1
|
|
if pass_char == index:
|
|
multi = 0
|
|
total -= ZeroExt(56, passwd[pass_char]) * multi
|
|
solver.add(total == 0)
|
|
# Solve
|
|
|
|
print(solver.check())
|
|
if solver.check() == sat:
|
|
model = solver.model()
|
|
result = ''.join(chr(model[p].as_long()) for p in passwd)
|
|
print("Recovered flag:", result)
|
|
else:
|
|
print("No solution found.")
|
|
|