I solved this challenge some time after the CTF. However I decided to publish a writeup as I did not see other ones using this solution.

For this challenge we have a 32bit armhf binary that we need to reverse. The program is accepting an input from the user and if it passes some checks it gives back the flag. In the binary there are hints regarding KLEE (a symbolic execution engine), so I guess that was the intended solution. During the competition I failed while playing with S2E and an ARM virtual machine, but in fact there was an easier solution!

The basic steps for solving the challenge are the following:

  • Run a decompiler on the binary
  • Fix the decompiled code so it compiles and uses symbolic values
  • Get LLVM bitcode
  • Run KLEE on the bitcode and profit

Here’s a fixed compilable code for the challenge. For marking input values as symbolic we substitute the calls to getc() with symbolic chars.

< v6 = getc(stdin);
> klee_make_symbolic(&v6, sizeof(v6), "v6");

Then we need to mark the point of the code that we are interested in reaching (i.e.: the reading of the flag). So we add a klee_assert(0); there.

Now we can compile the program and get LLVM bitcode and run KLEE on it. KLEE will craft the input, such that all the possible paths in the execution are reached.

$ clang -emit-llvm -c -g klug.c
$ klee klug.bc

On my laptop after roughly one hour we hit a path that returns the flag. We can inspect the results to find the testcase that reached that part of the program and get back the used input…

$ ls klee-last/ |grep assert
test016557.assert.err
$ ktest-tool klee-last/test016557.ktest
ktest file : 'klee-last/test016557.ktest'
args : ['klug.bc']
num objects: 15
object 0: name: 'v6'
object 0: size: 1
object 0: data: '\x80'
object 1: name: 'v6'
object 1: size: 1
object 1: data: ' '
object 2: name: 'v6'
object 2: size: 1
object 2: data: 'n'
object 3: name: 'v6'
object 3: size: 1
object 3: data: '\x1f'
object 4: name: 'v6'
object 4: size: 1
object 4: data: '['
object 5: name: 'v6'
object 5: size: 1
object 5: data: '\x02'
object 6: name: 'v6'
object 6: size: 1
object 6: data: '\xb3'
object 7: name: 'v6'
object 7: size: 1
object 7: data: '\xf1'
object 8: name: 'v6'
object 8: size: 1
object 8: data: '\xd7'
object 9: name: 'v6'
object 9: size: 1
object 9: data: '\xd8'
object 10: name: 'v6'
object 10: size: 1
object 10: data: '\x98'
object 11: name: 'v6'
object 11: size: 1
object 11: data: '\x00'
object 12: name: 'v6'
object 12: size: 1
object 12: data: '\xa3'
object 13: name: 'v6'
object 13: size: 1
object 13: data: '\x02'
object 14: name: 'v6'
object 14: size: 1
object 14: data: '\n'

… and profit!

$ python -c 'print "80206e1f5b02b3f1d7d89800a302".decode("hex")' | ./klug

Welcome! Find me the path to your flag and you shall get your reward!
The flag is: testflag

(I never got the real flag as I solved the challenge after the competition, so in the output you see only my test flag)

fox