HackTheBox Spooky License Challenge
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
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
#!/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.