 Nuit du Hack CTF Quals // Matryoshka Stage 2 // Keygenning with KLEE and Hex-Rays (100 Points)

1199

First, we need to identify the code that handles validating passwords. Opening the binary in IDA Pro makes it quite easy to visualize the main function.

Understanding all of the instructions isn’t required; it’s clear that the left branch occurs (outputting `Usage: %s <pass>`) when no input is give and the middle branch happens when an incorrect password is given (outputting `Try again...`). On the bottom right, there’s a call to sub_40064D that should be for the correct. That being said, I’ve seen some CTF challenges where there’s actually no ‘correct’ password, so let’s look at the function to make sure this isn’t a trick. Lucky for us, there’s no tricks. Using Hex-Rays Decompiler on main results in extremely readable C.

``````int __fastcall main(int a1, char **a2, char **a3)
{
int result; // eax@2
__int64 v4; // rbx@10
signed int v5; // [sp+1Ch] [bp-14h]@4

if ( a1 == 2 )
{
if ( 42 * (strlen(a2) + 1) != 504 )
goto LABEL_31;
v5 = 1;
if ( *a2 != 80 )
v5 = 0;
if ( 2 * a2 != 200 )
v5 = 0;
if ( *a2 + 16 != a2 - 16 )
v5 = 0;
v4 = a2;
if ( v4 != 9 * strlen(a2) - 4 )
v5 = 0;
if ( a2 != a2 )
v5 = 0;
if ( a2 != a2 )
v5 = 0;
if ( a2 - 17 != *a2 )
v5 = 0;
if ( a2 != a2 )
v5 = 0;
if ( a2 != 105 )
v5 = 0;
if ( a2 - a2 != 13 )
v5 = 0;
if ( a2 - a2 != 13 )
v5 = 0;
if ( v5 )
result = sub_40064D(a2);
else
LABEL_31:
result = fprintf(stdout, "Try again...\n", a2);
}
else
{
result = fprintf(stdout, "Usage: %s <pass>\n", *a2, a2);
}
return result;
}
``````

At this point, you can solve the equations by hand in a minute or two by looking up all the ASCII values. However, I decided that wouldn’t be a very fun learning experience, and decide to automate the process.

First, main.c needs to be adjusted slightly to be able to be recompiled. Only 2 lines were added and 7 changed.

``````#include "defs.h" // Take from IDA's plugins/
#include <string.h>
#include <stdio.h>

int main(int a1, char **a2, char **a3)
{
__int64 v4; // rbx@10
signed int v5; // [sp+1Ch] [bp-14h]@4

if ( a1 == 2 )
{
if ( 42 * (strlen(a2) + 1) != 504 )
goto LABEL_31;
v5 = 1;
if ( *a2 != 80 )
v5 = 0;
if ( 2 * a2 != 200 )
v5 = 0;
if ( *a2 + 16 != a2 - 16 )
v5 = 0;
v4 = a2;
if ( v4 != 9 * strlen(a2) - 4 )
v5 = 0;
if ( a2 != a2 )
v5 = 0;
if ( a2 != a2 )
v5 = 0;
if ( a2 - 17 != *a2 )
v5 = 0;
if ( a2 != a2 )
v5 = 0;
if ( a2 != 105 )
v5 = 0;
if ( a2 - a2 != 13 )
v5 = 0;
if ( a2 - a2 != 13 )
v5 = 0;
if ( v5 )
printf("Good good!\n");
else
LABEL_31:
printf("Try again...\n");
}
else
{
printf("Usage: %s <pass>\n", *a2);
}
}
``````

To solve the program, we can use KLEE (which is a symbolic virtual machine). I opted to use the Docker image of KLEE to avoid building it.

``````sudo docker pull klee/klee
sudo docker run -v /mnt/hgfs/stage2:/home/klee/stage2 --rm -ti --ulimit='stack=-1:-1' klee/klee # Adjust -v depending on what folder you're using.
``````

To flag to KLEE when we’ve reached the state we want, `klee_assert(0)` has to be added (which will flag it down as an error when it occurs).

``````#include "defs.h" // Take from IDA's plugins/
#include <string.h>
#include <stdio.h>
#include <assert.h>
#include <klee/klee.h>

int main(int a1, char **a2, char **a3)
{
__int64 v4; // rbx@10
signed int v5; // [sp+1Ch] [bp-14h]@4

if ( a1 == 2 )
{
if ( 42 * (strlen(a2) + 1) != 504 )
goto LABEL_31;
v5 = 1;
if ( *a2 != 80 )
v5 = 0;
if ( 2 * a2 != 200 )
v5 = 0;
if ( *a2 + 16 != a2 - 16 )
v5 = 0;
v4 = a2;
if ( v4 != 9 * strlen(a2) - 4 )
v5 = 0;
if ( a2 != a2 )
v5 = 0;
if ( a2 != a2 )
v5 = 0;
if ( a2 - 17 != *a2 )
v5 = 0;
if ( a2 != a2 )
v5 = 0;
if ( a2 != 105 )
v5 = 0;
if ( a2 - a2 != 13 )
v5 = 0;
if ( a2 - a2 != 13 )
v5 = 0;
if ( v5 ) {
printf("Good good!\n");
klee_assert(0);
}
else
LABEL_31:
printf("Try again...\n");
}
else
{
printf("Usage: %s <pass>\n", *a2);
}
}
``````

Onto compiling!

`clang -I ~/klee_src/include/ -emit-llvm -g -o main.ll -c main.`

Now, here’s the magic of KLEE. Running `klee --optimize --libc=uclibc --posix-runtime main.ll --sym-arg 100` will look for all possible solutions that are under 100 chars. After a mere few seconds (on an ancient mobile i3 CPU), the entire process is done. In this binary there’s one `*.err` file since there’s only one solution.

``````klee@4a860a030d10:~/stage2\$ ls klee-last/*err
klee-last/test000025.assert.err

klee@4a860a030d10:~/stage2\$ ktest-tool klee-last/test000025.ktest
ktest file : 'klee-last/test000025.ktest'
args       : ['main.ll', '--sym-arg', '100']
num objects: 2
object    0: name: b'arg0'
object    0: size: 101
object    0: data: b'Pandi_panda\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff'
object    1: name: b'model_version'
object    1: size: 4
object    1: data: b'\x01\x00\x00\x00'
``````

We can see that the input Pandi_panda (followed by a null byte) is the correct password.

All the source code can be found on GitLab.

https://gitlab.com/Manouchehri/Matryoshka-Stage-2/tree/master