https://app.hackthebox.com/challenges/409

Description

After cleaning up we found this old program and wanted to see what it does, but we can’t find the licence we had for it anywhere. Can you help?

Exploitation

#!/usr/bin/python3
from z3 import *

s = Solver()
flag = [BitVec(f'flag_{i}', 8) for i in range(0x20)]
for i in range(0x20):
    s.add(flag[i] >= 0x20, flag[i] <= 0x7f)
s.add(flag[9] == ord('p'))
s.add(flag[0x1d] == (flag[5] - flag[3]) + ord('F'))
s.add((flag[2] + flag[0x16]) == (flag[0xd] + ord('{')))
s.add((flag[0xc] + flag[4]) == (flag[5] + 0x1c))
s.add((flag[0x19] * flag[0x17]) == (flag[0] + flag[0x11] + 0x17))
s.add((flag[0x1b] * flag[1]) == (flag[5] + flag[0x16] - 0x15))
s.add((flag[9] * flag[0xd]) == (flag[0x1c] * flag[3] - 9))
s.add((flag[0x13] + flag[0x15]) == (flag[6] - 0x80))
s.add(flag[0x10] == (flag[0xf] - flag[0xb]) + ord('0'))
s.add((flag[7] * flag[0x1b]) == (flag[1] * flag[0xd] + ord('-')))
s.add(flag[0xd] == (flag[0x12] + flag[0xd] - 0x65))
s.add((flag[0x14] - flag[8]) == (flag[9] + ord('|')))
s.add(flag[0x1f] == (flag[8] - flag[0x1f]) - 0x79)
s.add((flag[0x14] * flag[0x1f]) == (flag[0x14] + 0x04))
s.add((flag[0x18] - flag[0x11]) == (flag[0x15] + flag[8] - 0x17))
s.add((flag[7] + flag[5]) == (flag[5] + flag[0x1d] + ord(',')))
s.add((flag[0xc] * flag[10]) == (flag[1] - flag[0xb] - 0x24))
s.add((flag[0x1f] * flag[0]) == (flag[0x1a] - 0x1b))
s.add((flag[1] + flag[0x14]) == (flag[10] - 0x7d))
s.add(flag[0x12] == (flag[0x1b] + flag[0xe] + 0x02))
s.add((flag[0x1e] * flag[0xb]) == (flag[0x15] + ord('D')))
s.add((flag[5] * flag[0x13]) == (flag[1] - 0x2c))
s.add((flag[0xd] - flag[0x1a]) == (flag[0x15] - 0x7f))
s.add(flag[0x17] == (flag[0x1d] - flag[0] + ord('X')))
s.add(flag[0x13] == (flag[8] * flag[0xd] - 0x17))
s.add((flag[6] + flag[0x16]) == (flag[3] + ord('S')))
s.add(flag[0xc] == (flag[0x1a] + flag[7] - 0x72))
s.add(flag[0x10] == (flag[0x12] - flag[5] + ord('3')))
s.add((flag[0x1e] - flag[8]) == (flag[0x1d] - 0x4d))
s.add((flag[0x14] - flag[0xb]) == (flag[3] - 0x4c))
s.add((flag[0x10] - flag[7]) == (flag[0x11] + ord('f')))
s.add((flag[1] + flag[0x15]) == (flag[0xb] + flag[0x12] + ord('+')))
if s.check() == sat:
    m = s.model()
    solution = ''
    for i in range(0x20):
        c = m[flag[i]].as_long()
        solution += chr(c)
    print(f"Found valid license key: {solution}")
else:
    print("No solution found")

Summary

Spooky License: reverse the validation logic, model the transform, and recover the accepted input.