This is a writeup of this year’s MRMCD CTF challenge “Flag Checker”, which I solved by hand while wondering how to let a computer solve this more elegantly. I thought about using Prolog until jn suggested using Z3, which I want to demonstrate in this post.

Essentially, the challenge was made up of to these JavaScript functions:

function isFlagCorrect(flag) {
  if (hash(flag.length) != 1801011984) return false;
  if (flag.indexOf("G") - flag.indexOf("A") != 5) return false;
  if (flag.indexOf("V") - flag.indexOf("J") != 15) return false;
  if (flag.indexOf("X") > 21) return false;
  if (flag.indexOf("O") - flag.indexOf("I") != 5) return false;
  if (flag.indexOf("E") - flag.indexOf("B") != 1) return false;
  if (flag.indexOf("M") < 9) return false;
  if (flag.indexOf("S") - flag.indexOf("P") != 2) return false;
  if (flag.indexOf("L") - flag.indexOf("B") != 10) return false;
  if (flag.split("H").length != 3) return false;
  if (flag.indexOf("W") - flag.indexOf("P") != 5) return false;
  if (flag.indexOf("N") != 12) return false;
  if (flag.indexOf("Q") - flag.indexOf("D") != 15) return false;
  if (flag.indexOf("F") != 5) return false;
  if (flag.indexOf("V") == 23) return false;
  if (flag.indexOf("X") - flag.indexOf("T") != 4) return false;
  if (flag.indexOf("U") - flag.indexOf("Q") != 6) return false;
  if (flag.indexOf("A") > 5) return false;
  if (flag.indexOf("S") - flag.indexOf("K") != 5) return false;
  if (flag.indexOf("D") == 2) return false;
  if (flag.indexOf("F") - flag.indexOf("C") != 4) return false;
  if (flag.indexOf("R") - flag.indexOf("H") != 10) return false;
  if (flag.indexOf("B") > 3) return false;
  if (flag.indexOf("T") - flag.indexOf("M") != 6) return false;

  return true;
}

function hash(s) {
  s = Math.pow(s, 5) ^ Math.pow(s, 7);
  return s;
};

Instead of manually sorting characters, the machine can do the work!

But let’s start by finding the length of the flag string first:

let findLength = (x) => hash(x) == 1801011984 ? x : findLength(x+1);
findLength(0);
=> 25

Great, now off to the interesting part!

Using constraint programming we can describe the constraints, it tells us whether or not they can be satisfied and we’ll get the solution as a byproduct. As mentioned, I’ll be using the Z3 theorem prover, which also comes with handy python bindings.

from z3 import *
s = Solver()

Transforming the JavaScript conditions to Z3 constraints is rather simple:

# JavaScript
if (flag.indexOf("G") - flag.indexOf("A") != 5) return false;
# Python / Z3
s.add(IndexOf(flag, "G", 0) - IndexOf(flag, "A", 0) == 5)

The following string concatenation

if (flag.split("H").length != 3) return false;

could be expressed in z3 like this:

l = String("left")
m = String("middle")
r = String("right")
s.add(l + "H" + m + "H" + r == flag)

But it’s very slow and the code really only assures that “H” occurs 2 times, which we can do in Z3 using a more performant little hack:

# IndexOf(str, substr, offset)
h1 = IndexOf(flag, "H", 0)
h2 = IndexOf(flag, "H", h1+1)
h3 = IndexOf(flag, "H", h2+1)

s.add(h2 != -1) # exists
s.add(h3 == -1) # doesn't exist

Finally, this is the complete python/z3 code, which doesn’t look too different from the original JavaScript code:

from z3 import *

s = Solver()

# an unknown string called 'flag'
flag = String('flag')

s.add(Length(flag) == 25)

s.add(IndexOf(flag, "G", 0) - IndexOf(flag, "A", 0) == 5)
s.add(IndexOf(flag, "V", 0) - IndexOf(flag, "J", 0) == 15)
s.add(IndexOf(flag, "X", 0) <= 21)
s.add(IndexOf(flag, "O", 0) - IndexOf(flag, "I", 0) == 5)
s.add(IndexOf(flag, "E", 0) - IndexOf(flag, "B", 0) == 1)
s.add(IndexOf(flag, "M", 0) >= 9)
s.add(IndexOf(flag, "S", 0) - IndexOf(flag, "P", 0) == 2)
s.add(IndexOf(flag, "L", 0) - IndexOf(flag, "B", 0) == 10)
s.add(IndexOf(flag, "W", 0) - IndexOf(flag, "P", 0) == 5)
s.add(IndexOf(flag, "Q", 0) - IndexOf(flag, "D", 0) == 15)
s.add(IndexOf(flag, "X", 0) - IndexOf(flag, "T", 0) == 4)
s.add(IndexOf(flag, "U", 0) - IndexOf(flag, "Q", 0) == 6)
s.add(IndexOf(flag, "S", 0) - IndexOf(flag, "K", 0) == 5)
s.add(IndexOf(flag, "F", 0) - IndexOf(flag, "C", 0) == 4)
s.add(IndexOf(flag, "T", 0) - IndexOf(flag, "M", 0) == 6)
s.add(IndexOf(flag, "R", 0) - IndexOf(flag, "H", 0) == 10)

s.add(IndexOf(flag, "N", 0) == 12)
s.add(IndexOf(flag, "F", 0) == 5)
s.add(IndexOf(flag, "V", 0) != 23)
s.add(IndexOf(flag, "A", 0) <= 5)
s.add(IndexOf(flag, "D", 0) != 2)
s.add(IndexOf(flag, "B", 0) <= 3)

h1 = IndexOf(flag, "H", 0)
h2 = IndexOf(flag, "H", h1+1)
h3 = IndexOf(flag, "H", h2+1)

s.add(h2 != -1)
s.add(h3 == -1)

s.check()
print(s.model())

Where s.check() returns sat (satisfiable) and s.model() gives us the model that was created to prove it:

[flag = "DCABEFIGHJMONLKQTPRSXUWHV"]

isFlagCorrect("DCABEFIGHJMONLKQTPRSXUWHV");
=> true

\o/