247CTF - The Secret Lock

Posted on Edited on In Views: Disqus: Word count in article: 1.3k Reading time ≈ 5 mins.

Reverse the lock validation logic and recover the 40-character flag.

Challenge

The page verifies a candidate flag client-side with a long chain of arithmetic and bitwise constraints.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
...
        checkFlag(flag) {
          let result = "LOCKED";
          this.dom.lock.classList.remove("verified");
          if (
            Object.keys(flag).length == 40 &&
            (flag[37] - flag[37]) * flag[15] == 0 &&
            (flag[3] + flag[31]) ^ (flag[29] + flag[8] == 234) &&

// Constraint Satisfaction

          ) {
            result = "";
            for (var idx in flag) {
              result += String.fromCharCode(flag[idx]);
            }
            this.dom.lock.classList.add("verified");
          }
          return result;
        }

...
    </script>

Approach

  • Extract all if (...) constraints from the JavaScript checker.
  • Model each flag[i] as an ASCII character in Z3 (32..126).
  • Convert JavaScript-style constraint expressions into valid Python/Z3 expressions.
  • Solve and rebuild the flag string from the model.

Solver Script (Z3)

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
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
#!/usr/bin/env python3
import re

from z3 import BitVec, Solver, sat

raw_js = """
(flag[37] - flag[37]) * flag[15] == 0 &&
(flag[3] + flag[31]) ^ (flag[29] + flag[8] == 234) &&
(flag[32] - flag[12]) * flag[9] == -2332 &&
(flag[24] - flag[27] + flag[13]) ^ (flag[6] == 114) &&
(flag[38] - flag[15]) * flag[33] == 800 &&
(flag[34] - flag[21]) * flag[26] == 98 &&
(flag[29] + flag[0]) ^ (flag[8] + flag[38] == 248) &&
(flag[21] * flag[18]) ^ (flag[7] - flag[15] == 2694) &&
(flag[28] * flag[23]) ^ (flag[19] - flag[5] == -9813) &&
(flag[34] + flag[30]) ^ (flag[37] + flag[6] == 72) &&
(flag[23] - flag[22]) * flag[12] == 4950 &&
(flag[9] * flag[28]) ^ (flag[20] - flag[11] == 5143) &&
(flag[2] * flag[22]) ^ (flag[37] - flag[0] == 2759) &&
(flag[26] - flag[12]) * flag[3] == -3350 &&
(flag[35] * flag[0]) ^ (flag[23] - flag[21] == 2698) &&
(flag[20] + flag[31]) ^ (flag[5] + flag[10] == 22) &&
(flag[31] * flag[19]) ^ (flag[1] - flag[2] == -2655) &&
(flag[38] - flag[14]) * flag[18] == 55 &&
(flag[29] - flag[19] + flag[10]) ^ (flag[2] == 93) &&
(flag[13] - flag[25] + flag[30]) ^ (flag[29] == 13) &&
(flag[35] + flag[33]) ^ (flag[26] + flag[21] == 249) &&
(flag[17] + flag[24]) ^ (flag[34] + flag[1] == 253) &&
(flag[32] - flag[35] + flag[19]) ^ (flag[1] == 0) &&
(flag[22] - flag[11] + flag[3]) ^ (flag[31] == 113) &&
(flag[19] - flag[0]) * flag[13] == 108 &&
(flag[19] - flag[17]) * flag[14] == -2475 &&
(flag[31] - flag[35] + flag[16]) ^ (flag[19] == 84) &&
(flag[24] * flag[27]) ^ (flag[35] - flag[17] == -5792) &&
(flag[11] * flag[35]) ^ (flag[15] - flag[28] == -2845) &&
(flag[18] - flag[19] + flag[31]) ^ (flag[5] == 112) &&
(flag[20] - flag[6]) * flag[10] == -3933 &&
(flag[39] - flag[33]) * flag[6] == 3075 &&
(flag[22] + flag[1]) ^ (flag[39] + flag[14] == 211) &&
(flag[37] * flag[24]) ^ (flag[12] - flag[39] == -5726) &&
(flag[29] + flag[3]) ^ (flag[8] + flag[11] == 195) &&
(flag[26] * flag[7]) ^ (flag[10] - flag[17] == -2375) &&
(flag[11] - flag[12]) * flag[12] == -4653 &&
(flag[13] * flag[5]) ^ (flag[12] - flag[25] == 3829) &&
(flag[24] * flag[0]) ^ (flag[13] - flag[23] == -2829) &&
(flag[17] + flag[12]) ^ (flag[8] + flag[14] == 170) &&
(flag[38] + flag[23]) ^ (flag[11] + flag[1] == 245) &&
(flag[22] + flag[5]) ^ (flag[21] + flag[24] == 19) &&
(flag[35] - flag[8] + flag[21]) ^ (flag[30] == 85) &&
(flag[18] - flag[31] + flag[28]) ^ (flag[29] == 0) &&
(flag[30] * flag[35]) ^ (flag[27] - flag[29] == 5501) &&
(flag[8] - flag[30] + flag[16]) ^ (flag[36] == 81) &&
(flag[13] * flag[18]) ^ (flag[35] - flag[38] == -2971) &&
(flag[27] - flag[14]) * flag[39] == 5875 &&
(flag[34] - flag[33]) * flag[6] == -6027 &&
(flag[38] * flag[1]) ^ (flag[20] - flag[10] == -2915) &&
(flag[1] - flag[1]) * flag[3] == 0 &&
(flag[36] - flag[20]) * flag[8] == 2640 &&
(flag[23] - flag[11] + flag[17]) ^ (flag[33] == 246) &&
(flag[13] - flag[38]) * flag[0] == -100 &&
(flag[28] - flag[14]) * flag[31] == 2142 &&
(flag[26] + flag[15]) ^ (flag[13] + flag[31] == 8) &&
(flag[36] - flag[15]) * flag[17] == 5238 &&
(flag[16] - flag[30]) * flag[33] == 0 &&
(flag[2] - flag[20] + flag[13]) ^ (flag[6] == 76) &&
(flag[10] - flag[14] + flag[31]) ^ (flag[13] == 3) &&
(flag[0] * flag[10]) ^ (flag[14] - flag[31] == 2854) &&
(flag[28] - flag[34] + flag[14]) ^ (flag[14] == 82) &&
(flag[28] - flag[25]) * flag[1] == 2444 &&
(flag[34] - flag[12]) * flag[25] == -2400 &&
(flag[28] * flag[38]) ^ (flag[17] - flag[4] == 5429) &&
(flag[21] - flag[21] + flag[26]) ^ (flag[23] == 84) &&
(flag[9] - flag[4] + flag[18]) ^ (flag[35] == 47) &&
(flag[28] - flag[21] + flag[1]) ^ (flag[33] == 0) &&
(flag[24] - flag[25] + flag[22]) ^ (flag[0] == 8) &&
(flag[28] - flag[25]) * flag[12] == 4653 &&
(flag[1] * flag[15]) ^ (flag[10] - flag[8] == 2498) &&
(flag[5] * flag[7]) ^ (flag[15] - flag[34] == -3429) &&
(flag[8] * flag[3]) ^ (flag[23] - flag[22] == 3671) &&
(flag[25] - flag[33]) * flag[11] == -2600 &&
(flag[21] + flag[12]) ^ (flag[37] + flag[28] == 81) &&
(flag[30] + flag[33]) ^ (flag[34] + flag[14] == 162) &&
(flag[6] - flag[25]) * flag[8] == 4015 &&
(flag[24] - flag[7] + flag[12]) ^ (flag[7] == 90) &&
(flag[18] * flag[12]) ^ (flag[8] - flag[4] == -5466) &&
(flag[32] * flag[7]) ^ (flag[32] - flag[27] == -2730) &&
(flag[32] * flag[34]) ^ (flag[29] - flag[16] == 2804) &&
(flag[25] * flag[22]) ^ (flag[28] - flag[39] == -2542) &&
(flag[8] - flag[15]) * flag[6] == 861 &&
(flag[20] + flag[18]) ^ (flag[25] + flag[36] == 245) &&
(flag[5] - flag[28] + flag[14]) ^ (flag[39] == 97) &&
(flag[30] * flag[11]) ^ (flag[16] - flag[11] == 5216) &&
(flag[11] + flag[18]) ^ (flag[7] + flag[9] == 13) &&
(flag[9] - flag[2]) * flag[30] == -200 &&
(flag[12] + flag[37]) ^ (flag[9] + flag[4] == 78) &&
(flag[10] - flag[37]) * flag[38] == -2408 &&
(flag[5] * flag[19]) ^ (flag[20] - flag[21] == 3645) &&
(flag[27] * flag[29]) ^ (flag[39] - flag[21] == 10354) &&
(flag[15] * flag[32]) ^ (flag[7] - flag[22] == -2642) &&
(flag[1] - flag[3] + flag[24]) ^ (flag[31] == 25) &&
(flag[13] - flag[0]) * flag[30] == 400 &&
(flag[18] - flag[15] + flag[36]) ^ (flag[28] == 12) &&
(flag[34] + flag[21]) ^ (flag[12] + flag[37] == 163) &&
(flag[36] - flag[33]) * flag[14] == 110 &&
(flag[2] - flag[3]) * flag[3] == -804 &&
(flag[35] - flag[27] + flag[22]) ^ (flag[4] == 80) &&
(flag[10] + flag[9]) ^ (flag[17] + flag[2] == 246) &&
(flag[25] * flag[4]) ^ (flag[27] - flag[23] == 4201) &&
(flag[32] * flag[19]) ^ (flag[3] - flag[25] == 2877) &&
(flag[37] - flag[14]) * flag[23] == 4545 &&
(flag[32] + flag[13]) ^ (flag[31] + flag[32] == 7) &&
(flag[11] - flag[25]) * flag[39] == 250 &&
(flag[17] + flag[31]) ^ (flag[6] + flag[9] == 36) &&
(flag[4] + flag[27]) ^ (flag[2] + flag[31] == 208) &&
(flag[6] + flag[7]) ^ (flag[26] + flag[21] == 206) &&
(flag[19] + flag[25]) ^ (flag[22] + flag[10] == 10) &&
(flag[34] + flag[2]) ^ (flag[8] + flag[26] == 2) &&
(flag[7] + flag[5]) ^ (flag[12] + flag[14] == 237) &&
(flag[1] - flag[13]) * flag[38] == -112 &&
(flag[0] - flag[19] + flag[16]) ^ (flag[0] == 80) &&
(flag[31] + flag[36]) ^ (flag[3] + flag[2] == 227) &&
(flag[32] - flag[3] + flag[26]) ^ (flag[4] == 113) &&
(flag[3] * flag[6]) ^ (flag[16] - flag[27] == -8241) &&
(flag[24] + flag[15]) ^ (flag[2] + flag[30] == 242) &&
(flag[11] + flag[21]) ^ (flag[31] + flag[20] == 12) &&
(flag[9] - flag[26] + flag[23]) ^ (flag[30] == 13)
"""
s = Solver()

flag = [BitVec(f"flag[{i}]", 32) for i in range(40)]

for i in range(40):
    s.add(flag[i] >= 32, flag[i] <= 126)

for line in raw_js.strip().split("&&"):
    line = line.strip()
    if not line:
        continue

    # Convert: A ^ (B == N)   ->   (A ^ B) == N
    if "^" in line:
        line = re.sub(r"(.*)\^\s*\((.*)\s*==\s*(-?\d+)\)", r"(\1 ^ (\2)) == \3", line)

    s.add(eval(line))

if s.check() == sat:
    m = s.model()
    result = "".join([chr(m[flag[i]].as_long()) for i in range(40)])
    print(f"\n[+] Result: {result}")
else:
    print("\n[-] Unsatisfiable.")

Notes

  • ^ in JavaScript is bitwise XOR (not exponent), so constraints must be modeled as XOR equations.
  • 32-bit BitVec variables are used to match JavaScript bitwise operation behavior.

Flag

247CTF{17594c670da74613e921faed37d37fd8}