About 247CTF

The 247/CTF is a security Capture The Flag (CTF) learning environment. The platform contains a number of hacking challenges where you can test your skills across web, cryptography, networking, reversing and exploitation by solving problems to recover flags.

Or generally saying it is the platform which hosts CTF challs for whole year :)

Task - The Secret Lock

Can you reverse the secret combination to open the lock and recover the flag?

The single HTML page is given with digital lock:

  • it have 40 fields
  • each field have 501 available values (0-500)

Lock

Solution

By looking into the code we can quickly identify the code section, because it is written in plain-text in the single <script> block. Below you can see the main unlocking logic:

onChange() {
    this.code = this.getCode();
    this.flag = this.checkFlag(this.code);
    this.dom.status.textContent = this.flag;
}

getCode() {
    let flag = {};
    for (let i = 0, len = this.dom.rows.length; i < len; i++) {
    flag[i] = this.dom.rows[i].querySelector('.is-selected .text').textContent;
    }
    return flag;
}

checkFlag(flag){
    let result = "LOCKED"
    this.dom.lock.classList.remove('verified');
    if (Object.keys(flag).length == 40 && ((flag[37] - flag[37]) * flag[15] == 0) && /* stripped for readibillity */)) {
    result = "";
    for (var idx in flag) {
        result += (String.fromCharCode(flag[idx]));
    }
    this.dom.lock.classList.add('verified');
    }
    return result;
}

Here is the unlocking summary:

  1. On each digit change the onChange() function is called.
  2. getCode() is run, it returns the integer value.
  3. Code is checked in checkFlag() which runs a lot of algebraic expressions (120 to be precise). I stripped them to improve the readibillity.
  4. If all checks are passed, then each value is treated as ascii character and it’s passed to result value.

Like I mentioned before - we have big block of conditions which needs to be met, you can find short snippet below (I used visual-code to quickly get rid of && operators and put each expression in new line).

((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)

We can notice a lot of expressions -> we can’t don’t want to solve it manually - we need to write a script.

Expressions are utilizing different operations, so we can’t simply parse them in python, it is better to use some specialized tool like z3-solver:

from z3 import *
z = Solver()

# We are creating the bit represenation of int32, 40 = len(FLAG)
# I'm using vectors not ints, because ints are not supporting XOR
flag = [BitVec('flag{:02}'.format(i), 32) for i in range(40)]
for i in flag:
    z.add(i > 0, i <= 500, i > 30, i < 127)
    # z.add(i > 30, i < 127) potential optimization

# copy-paste the conditions
z.add((flag[37] - flag[37]) * flag[15] == 0) 
z.add((flag[3] + flag[31]) ^ (flag[29] + flag[8]) == 234) 
### ---[Stripped conditions]---
z.add((flag[9] - flag[26] + flag[23]) ^ flag[30] == 13)

# Check if  z3 can solve the problem
if z.check() == "sat":
    print("z3 can solve it")

    # now we can create the model and evaluate it to "real" values
    model = z.model()
    solution = ""
    for f in flag:
        solution += chr(int(model.evaluate(f).as_long()))
        print(solution)
else:
    print("unsolvable")

This will give as a flag :)

References