Explore the basics of cybersecurity in the Spooky License Challenge on Hack The Box. This easy-level Challenge introduces encryption reversal and file handling concepts in a clear and accessible way, perfect for beginners.

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#

The Spooky License Challenge on Hack The Box introduces reverse engineering concepts using Python and Z3, a symbolic solver. Participants analyze encryption logic and constraints applied to the flag, which is treated as a 32-character key. By solving the constraints programmatically, the challenge demonstrates practical applications of symbolic execution and encryption reversal to retrieve the valid license key.