stage2.md 6.21 KB
Newer Older
David Manouchehri's avatar
David Manouchehri committed
1 2
# Keygenning with KLEE and Hex-Rays

David Manouchehri's avatar
David Manouchehri committed
3
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.
David Manouchehri's avatar
David Manouchehri committed
4

David Manouchehri's avatar
David Manouchehri committed
5
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...`).
David Manouchehri's avatar
David Manouchehri committed
6

David Manouchehri's avatar
David Manouchehri committed
7
![main flowchart](main.png?raw=true)
David Manouchehri's avatar
David Manouchehri committed
8

David Manouchehri's avatar
David Manouchehri committed
9
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.
David Manouchehri's avatar
David Manouchehri committed
10 11 12

![sub_40064D flowchart](sub_40064D.png?raw=true)

David Manouchehri's avatar
David Manouchehri committed
13
Lucky for us, there's no tricks. Using Hex-Rays Decompiler on main results in extremely readable C.
David Manouchehri's avatar
David Manouchehri committed
14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63

```
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]) + 1) != 504 )
      goto LABEL_31;
    v5 = 1;
    if ( *a2[1] != 80 )
      v5 = 0;
    if ( 2 * a2[1][3] != 200 )
      v5 = 0;
    if ( *a2[1] + 16 != a2[1][6] - 16 )
      v5 = 0;
    v4 = a2[1][5];
    if ( v4 != 9 * strlen(a2[1]) - 4 )
      v5 = 0;
    if ( a2[1][1] != a2[1][7] )
      v5 = 0;
    if ( a2[1][1] != a2[1][10] )
      v5 = 0;
    if ( a2[1][1] - 17 != *a2[1] )
      v5 = 0;
    if ( a2[1][3] != a2[1][9] )
      v5 = 0;
    if ( a2[1][4] != 105 )
      v5 = 0;
    if ( a2[1][2] - a2[1][1] != 13 )
      v5 = 0;
    if ( a2[1][8] - a2[1][7] != 13 )
      v5 = 0;
    if ( v5 )
      result = sub_40064D(a2[1]);
    else
LABEL_31:
      result = fprintf(stdout, "Try again...\n", a2);
  }
  else
  {
    result = fprintf(stdout, "Usage: %s <pass>\n", *a2, a2);
  }
  return result;
}
```

David Manouchehri's avatar
David Manouchehri committed
64
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.
David Manouchehri's avatar
David Manouchehri committed
65

David Manouchehri's avatar
David Manouchehri committed
66
First, main.c needs to be adjusted slightly to be able to be recompiled. Only 2 lines were added and 7 changed.
David Manouchehri's avatar
David Manouchehri committed
67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118

```
#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]) + 1) != 504 )
      goto LABEL_31;
    v5 = 1;
    if ( *a2[1] != 80 )
      v5 = 0;
    if ( 2 * a2[1][3] != 200 )
      v5 = 0;
    if ( *a2[1] + 16 != a2[1][6] - 16 )
      v5 = 0;
    v4 = a2[1][5];
    if ( v4 != 9 * strlen(a2[1]) - 4 )
      v5 = 0;
    if ( a2[1][1] != a2[1][7] )
      v5 = 0;
    if ( a2[1][1] != a2[1][10] )
      v5 = 0;
    if ( a2[1][1] - 17 != *a2[1] )
      v5 = 0;
    if ( a2[1][3] != a2[1][9] )
      v5 = 0;
    if ( a2[1][4] != 105 )
      v5 = 0;
    if ( a2[1][2] - a2[1][1] != 13 )
      v5 = 0;
    if ( a2[1][8] - a2[1][7] != 13 )
      v5 = 0;
    if ( v5 )
      printf("Good good!\n");
    else
LABEL_31:
      printf("Try again...\n");
  }
  else
  {
    printf("Usage: %s <pass>\n", *a2);
  }
}
```

David Manouchehri's avatar
David Manouchehri committed
119
To solve the program, we can use KLEE (which is a symbolic virtual machine). I opted to use the [Docker image of KLEE](https://klee.github.io/docker/) to avoid building it.
David Manouchehri's avatar
David Manouchehri committed
120 121

```
David Manouchehri's avatar
David Manouchehri committed
122
sudo docker pull klee/klee
David Manouchehri's avatar
David Manouchehri committed
123 124 125 126
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).
David Manouchehri's avatar
David Manouchehri committed
127

David Manouchehri's avatar
David Manouchehri committed
128 129 130 131 132 133
```
#include "defs.h" // Take from IDA's plugins/
#include <string.h>
#include <stdio.h>
#include <assert.h>
#include <klee/klee.h>
David Manouchehri's avatar
David Manouchehri committed
134

David Manouchehri's avatar
David Manouchehri committed
135 136 137 138
int main(int a1, char **a2, char **a3)
{
  __int64 v4; // rbx@10
  signed int v5; // [sp+1Ch] [bp-14h]@4
David Manouchehri's avatar
David Manouchehri committed
139

David Manouchehri's avatar
David Manouchehri committed
140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181
  if ( a1 == 2 )
  {
    if ( 42 * (strlen(a2[1]) + 1) != 504 )
      goto LABEL_31;
    v5 = 1;
    if ( *a2[1] != 80 )
      v5 = 0;
    if ( 2 * a2[1][3] != 200 )
      v5 = 0;
    if ( *a2[1] + 16 != a2[1][6] - 16 )
      v5 = 0;
    v4 = a2[1][5];
    if ( v4 != 9 * strlen(a2[1]) - 4 )
      v5 = 0;
    if ( a2[1][1] != a2[1][7] )
      v5 = 0;
    if ( a2[1][1] != a2[1][10] )
      v5 = 0;
    if ( a2[1][1] - 17 != *a2[1] )
      v5 = 0;
    if ( a2[1][3] != a2[1][9] )
      v5 = 0;
    if ( a2[1][4] != 105 )
      v5 = 0;
    if ( a2[1][2] - a2[1][1] != 13 )
      v5 = 0;
    if ( a2[1][8] - a2[1][7] != 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);
  }
}
```
David Manouchehri's avatar
David Manouchehri committed
182

David Manouchehri's avatar
David Manouchehri committed
183 184 185 186 187 188 189
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.

```
David Manouchehri's avatar
David Manouchehri committed
190 191 192 193 194 195 196 197 198 199 200 201 202
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'
David Manouchehri's avatar
David Manouchehri committed
203 204 205
```

We can see that the input Pandi_panda (followed by a null byte) is the correct password.
David Manouchehri's avatar
David Manouchehri committed
206 207 208 209 210 211 212 213

## References

- https://doar-e.github.io/blog/2015/08/18/keygenning-with-klee/
- https://klee.github.io/tutorials/testing-function/
- https://klee.github.io/tutorials/testing-coreutils/
- https://www.cs.umd.edu/~mwh/se-tutorial/
- https://www.cs.purdue.edu/homes/kim1051/cs490/proj3/description.html