Byte Bandits CTF 2018 - laz3y (350)

In this challenge we're presented with a web server which contains a heavily obfuscated JavaScript file as one of it's resources.

We're going to jump into an intro of Z3 to solve parts of this challenge after some initial reversing.

If you would like to watch a better version of the topics discussed in this blog post, check out LiveOverflow's great video on "Using z3 to find a password and reverse obfuscated JavaScript" - https://www.youtube.com/watch?v=TpdDq56KH1I. It helped a lot when attempting to solve this challenge.

Reversing

Here's a snippet of the file which was beautified using the online service jsnice:

(function() {
    _0x13c3dd(this, function() {
        if (_0x15c2('0x7') === _0x15c2('0x7')) {
            var _0x42483f = new RegExp('function\x20*\x5c(\x20*\x5c)');
            var _0x43babc = new RegExp(_0x15c2('0x8'), 'i');
            var _0x53dbc9 = _0x4f7527(_0x15c2('0x4'));
            if (!_0x42483f[_0x15c2('0x5')](_0x53dbc9 + _0x15c2('0x6')) || !_0x43babc[_0x15c2('0x5')](_0x53dbc9 + 'input')) {
                if (_0x15c2('0x9') === _0x15c2('0x9')) {
                    _0x53dbc9('0');
                } else {
                    return !![];
                }
            } else {
                if ('CJMng' === _0x15c2('0xa')) {
                    _0x4f7527();
                } else {
                    return !![];
                }
            }
        } else {
            return function(_0x256bf0) {}[_0x15c2('0xb')](_0x15c2('0xc'))[_0x15c2('0xd')](_0x15c2('0xe'));
        }
    })();
}());

We can jump to potentially interesting parts of the code to find out what's going on.

One interesting part included a 'Flag{' string. This was used to build up the final flag, stored originally in a giant array of mixed snippets used for various reasons:

var _0x387a = ["GfKdJ", ... "slice", "tryingharder", "Flag{", "log", "Invalid Password", "pDsTn", "UOAuo", ... ];

There's another interesting part of the code which contains the variable 'solver' -- sounds like this may help us solve the challenge. It's also a hint mixed with the challenge title 'laz3y' referencing the Z3 SMT solver.

function solver(value) {
  if (!/[^nfTzhb_0FAiuctxlswa!]/[_0xd1e9[9]](value) &&
      value[29] == _0xd1e9[10] &&
      value[4] == value[8] &&
      value[10] == value[14] &&
      value[17] == _0xd1e9[11] &&
      value[4] == _0xd1e9[11] &&
      leng(value) &&
      crypto(value) &&
      a(value) &&
      b(value) &&
      c(value) &&
      d(value) &&
      f(value)) {
    if (_0x15c2("0x26") === _0x15c2("0x26")) {
      console[_0xd1e9[14]](_0xd1e9[12] + value + _0xd1e9[13]);
    } else {
      return !![];
    }
  } else {
    if (_0x15c2("0x27") !== "DbvWm") {
      /** @type {!Function} */
      var advancement = firstCall ? function() {
        if (fn) {
          var denies = fn[_0x15c2("0xd")](context, arguments);
          /** @type {null} */
          fn = null;
          return denies;
        }
      } : function() {
      };
      /** @type {boolean} */
      firstCall = ![];
      return advancement;
    } else {
      console[_0xd1e9[14]](_0xd1e9[15]);
    }
  }
}

Executing the script in a stub html file and looking at the following value we can see it's just a console.log pulled from one of the obscure array's:

console[_0xd1e9[14]](_0xd1e9[15]);
...
console['log']("Invalid Password");

The same is with the first condition after all the conditional checks:

console[_0xd1e9[14]](_0xd1e9[12] + value + _0xd1e9[13]);
...
console['log']("Flag{" + value + "}");

There are also a lot of false flows in this obfuscated code, so we can reduce this function to the following:

function solver(value) {
  if (!/[^nfTzhb_0FAiuctxlswa!]/.test(value) &&
    value[29] == "!" &&
    value[4] == value[8] &&
    value[17] == "_" &&
    value[4] == "_" &&
    leng(value) &&
    crypto(value) &&
    value[10] == value[14] &&
    a(value) &&
    b(value) &&
    c(value) &&
    d(value) &&
    f(value)) {
      console.log("Flag{" + value + "}");
  } else {
      console.log("Invalid Password");
  }
}

Now we need to analyze each one of these functions to make sure we can setup input to make it pass.

Starting with the interesting sounding function first 'crypto', isn't heavily related to cryptography:

function crypto(context) {
  var val = "";
  var row = context.slice(18, 29);
  var masks = [68, 16, 31, 28, 29, 4, 9, 21, 27, 84, 11, 114];

  for (var i = 0; i <= row.length; i++) {
    val += String.fromCharCode(row.charCodeAt(i) ^ masks[i]);
  }

  return val == "tryingharder";
}

Looking at this, we can tell it wants the result of "tryingharder" by xor'ing against a given mask.

Reversing this process, we'll get the expected value for part of the flag:

$ python
>>> from pwn import *
>>> masks = [68, 16, 31, 28, 29, 4, 9, 21, 27, 84, 11, 114]
>>> tryHarder = "tryingharder"
>>> ''.join([xor(tryHarder[i], masks[i]) for i in range(len(masks))])
'0bfuscati0n\x00'

Continuing with each function, we can inline any obvious values and write simple formulas for others (//X// comments represent known values to skip during the constraint solve):

190     value[29] == "!" &&           //X// payload[29]         = '!'
191     value[4] == value[8] &&       //X// 08 & 04             = '_'
192     value[17] == "_" &&           //X// payload[17]         = '_'
193     value[4] == "_" &&            //X// payload[4]          = '_'
194     leng(value) &&                //X// len(payload)       == 30
195     crypto(value) &&              //X// payload[18:29]     == 0bfuscati0n
196     value[10] == value[14] &&   // p[10] == p[14]
197     a(value) &&                 // p[3] - p[0] == 32 && p[5] - p[12] == 71
198     b(value) &&                   //X// p[12] == p[15] &&
199                                   //X// p[11] == "l" &&
200                                   //X// p[12] == "0" &&
201                                   //X// p[13] == "T" &&
202                                   //X// p[0]  == p[13]
203     c(value) &&                 // p[9] + p[6] - p[1] == 58;
204     d(value) &&                 // (p[0] * p[1] * p[2] * p[3]) / 128 === 767949;
205     f(value)) {                 // (p[5] * p[6] * p[7]) / 25 === 35581;

We only have five constraints to solve for!  With the other values, we get the following partial flag from the static analysis done so far:

T???_???_??l0T?0?_0bfuscati0n!

Z3 Solve

If you haven't heard of Z3 before, check out the Z3-Playground repo, it has some fantastic examples of how to use Z3 in general and for security related tasks.

Using the basic hello-world example from Z3-Playground we can add one constraint to see how Z3 works. We give it two variables a & b, then say a + b is equal to 1337, also b is above 20.

from z3 import *

a, b = BitVecs('a b', 32)
s = Solver()

s.add((a + b) == 1337)
s.add(b > 20)

if s.check() == sat:
    print s.model()
else:
    print 'Unsat'

Letting z3 solve for this, it will return input which satisfies these constraints:

$ python hello.py
[b = 21, a = 1316]

The values 21 and 1316 do sum to 1337, so it looks like this works!

Now we can get into solving this challenge!

Instead of using BitVecs for variables, we'll be using integer values representing characters.
Initializing the unknown flag, we use the z3 Int type:

flag = [Int(i) for i in xrange(30)]

If you remember from above, the important constraints we need to setup are:

196     value[10] == value[14] &&   // p[10] == p[14]
197     a(value) &&                 // p[3] - p[0] == 32 && p[5] - p[12] == 71
203     c(value) &&                 // p[9] + p[6] - p[1] == 58;
204     d(value) &&                 // (p[0] * p[1] * p[2] * p[3]) / 128 === 767949;
205     f(value)) {                 // (p[5] * p[6] * p[7]) / 25 === 35581;

Changing 'p' to 'flag' and wrapping a solve add around them will get us most of the way there:

s.add(flag[10] ≡ flag[14])
s.add(flag[3] - flag[0] ≡ 32)
s.add(flag[5] - flag[12] == 71)
s.add(flag[9] + flag[6] - flag[1] ≡ 58)
s.add((flag[0] * flag[1] * flag[2] * flag[3]) / 128 ≡ 767949)
s.add((flag[5] * flag[6] * flag[7]) / 25 ≡ 35581)

There are six constraints instead of five here, this is because line 197 was split into two separate constraints for readability.

We should also setup the parts of the flag we know about already:

partial = 'T???_???_??l0T?0?_0bfuscati0n!'

for x in range(len(partial)):
  if partial[x] is not '?':
    s.add(flag[x] ≡ ord(partial[x]))

And setup the flag to be within a printable range:

for x in range(0, 30):
  s.add(flag[x] >= ord('!') and flag[x] <= ord('z'))

With all of this setup, we could attempt to print the flag (converting ints to chars in the process):

if s.check() == sat:
  m = s.model()
  print 'Flag{' + ''.join([chr(m[x].as_long()) for x in flag]) + '}'
else:
  print 'Not Found.'

This yields:

Flag{That_wsA_/zl0Tz0z_0bfuscati0n!}

This is very close! But not there yet! There are a few errors to work out.
First part that seems off is the '/' character, it doesn't seem likely it would be in this flag and if it was, it wouldn't be in that position.

So for this we'll setup a constraint against it:

s.add(flag[9] != ord('/'))
...
Flag{Taht_wsA_(zl0Tz0z_0bfuscati0n!}

Now the slash character is fixed, but we have some other problems, Taht was switched, and wsA looks like the word 'was'. To fix the first word, we'll constrain the 'h' where it was:

s.add(flag[1] == ord('h'))
...
Flag{That_wAs_azl0Tz0z_0bfuscati0n!}

If we look at 'wAs_azl0T', it looks like the words 'was a lot' so there's a missing space between 'a' and 'lot', we'll add this with an underscore:

s.add(flag[10] == ord('_'))

Now when we run this we get the Flag!

Flag{That_wAs_a_l0T_0z_0bfuscati0n!}

This was the final Z3 client for the solve: