**Binary analysis: Concolic execution with Pin and z3**

by Jonathan Salwan - 2013-08-28
**1 - Introduction**

**2 - Concolic execution**

**3 - Proof of concept on dumb crackme**

3.1 - Introduction

3.2 - Compile a Pin tool with Z3 C++ API

3.3 - Save and solve the constraints

3.4 - Demo on the first crackme

3.5 - Another crackme using XOR-based algorithm

**4 - Conclusion**

4.1 - My Pin tool

4.1 - References

4.2 - Special thanks

**Edit 2015-09-06**: Check out our concolic execution library using python bindings.

### 1 - Introduction

In a previous post, I talked about the concolic execution using Valgrind to the taint analysis and z3 to the constraint path solving. So why another blog post about this technique? Because recently my previous researchs was around Pin and because Pin is supported on Linux, Windows and Mac. I also wanted to see how it's possible to do it without IR - With Valgrind and z3 it was pretty easy because Valgrind provides an IR (VEX). Then, it can be useful for other people or it can be give some new ideas. :-).

### 2 - Concolic execution

We can find two types of analysis, static and dynamic analysis. Both approaches have some advantages and disadvantages. If you use dynamic analysis, we can't cover all the code but you will be more reliable. If you use static analysis, you can cover the code, but you can't get the context information at runtime. The concolic execution is a technic that uses both symbolic and concrete execution to solve a constraint path. The concolic execution is mainly used to cover a code. To list the constraints, the symbolic execution is used. Below, a little example about the symbolic execution:

int foo(int i1, int i2) { int x = i1; int y = i2; if (x > 80){ x = y * 2; y = 0; if (x == 256) return True; } else{ x = 0; y = 0; } /* ... */ return False; }

Based that code, we can see 3 differents paths, for each path we have a specific constraint. The constraints tree look like that:

So, we can say that this code can return **False** via two differents paths and **True** via only one path. With the symbolic
execution, it's possible to know which constraints are necessary to return **False** or **True**.

The concolic execution will use the concrete execution to save and solve the constraints at runtime. With this above case, to cover this code, the program will be executed three times and for each execution, one constraint will be solved to take another path. That's what we'll see in the next chapter.

### 3 - Proof of concept on dumb crackme

#### 3.1 - Introduction

We will start to analyze a simple code which contains only three simple conditions. The goal will be to solve this crackme automatically via the concolic execution.

#include <stdio.h> #include <sys/types.h> #include <stdlib.h> #include <fcntl.h> int main(void) { int fd; char buff[260] = {0}; fd = open("serial.txt", O_RDONLY); read(fd, buff, 256); close(fd); if (buff[0] != 'a') return False; if (buff[1] != 'b') return False; if (buff[2] != 'c') return False; printf("Good boy\n"); return True; }

Based on that code, if we represent all paths and constraints, our constraints tree will look like that:

This code contains four possible paths. Each path has its constraints.

+-----------+----------------------------------------------------+--------------+ | PC number | Constraints | return value | +-----------+----------------------------------------------------+--------------+ | 1 | buff[0] != 'a' | return False | | 2 | buff[0] == 'a' && buff[1] != 'b' | return False | | 3 | buff[0] == 'a' && buff[1] == 'b' && buff[2] != 'c' | return False | | 4 | buff[0] == 'a' && buff[1] == 'b' && buff[2] == 'c' | return True | +-----------+----------------------------------------------------+--------------+

Now that we have listed all constraints which are possible, we can cover the code. For that, we need to run the program with the first constraint, then we re-run the program with the second constraint and repeat this operation until the last constraint is executed. This operation is called the concolic execution. Below you can see a diagram representing this execution.

As you can see above, we can cover all the code with only four executions. Now, we will see how it's possible to implement it with Pin. For that we need to:

- Taint the serial.txt buffer.
- Follow our data (Spread the taint).
- Save the first constraint.
- Solve this constraint.
- Re-run the binary with the first constraint solved.
- And repeat this operation for each constraint (each path)...

In this blog post, we will not talk about the taint analysis, for that, you can read my previous post. Then, to solve the constraints we will use the theorem prover Z3 and its C++ API.

#### 3.2 - Compile a Pin tool with Z3 C++ API

We will use the Z3 C++ API inside the Pin tool. So, you need to install the Z3 library and add the headers/lib in the compile line. In my case, I downloaded the z3.zip in my pintool directory and I compiled the library. Then, to compile my Pin tool, I created a shell script which compiles with the Z3 headers/lib. This script looks like that:

$ pwd /home/jonathan/Works/Tools/pin-2.12-58423-gcc.4.4.7-linux/source/tools/ConcolicExecution $ cat compile.sh g++ -DBIGARRAY_MULTIPLIER=1 -DUSING_XED -Wall -Werror -Wno-unknown-pragmas -fno-stack-protector -DTARGET_IA32E -DHOST_IA32E -fPIC -DTARGET_LINUX -I../../../source/include/pin -I../../../source/include/pin/gen -I../../../extras/components/include -I./z3/src/api/c++ -I../../../extras/xed2-intel64/include -I../../../source/tools/InstLib -O3 -fomit-frame-pointer -fno-strict-aliasing -c -o obj-intel64/ConcolicExecution.o ConcolicExecution.cpp g++ -shared -Wl,--hash-style=sysv -Wl,-Bsymbolic -Wl,--version-script=../../../source/include/pin/pintool.ver -o obj-intel64/ConcolicExecution.so obj-intel64/ConcolicExecution.o -L../../../intel64/lib -L../../../intel64/lib-ext -L../../../intel64/runtime/glibc -L../../../extras/xed2-intel64/lib -lpin -lxed -ldwarf -lelf -ldl -lz3 $

#### 3.3 - Save and solve the constraints

If we look the ASM representation of our C code. We can see that this code loads in the "**eax**" register
our character ("**rbp-0x110**" points on our serial buffer). Then, it compares the smaller size register "**al**"
with a constant and it jumps to two different space if it's true or false.

.text:400683: movzx eax,BYTE PTR [rbp-0x110] .text:40068a: cmp al,0x61 .text:40068c: je 400695 <main+0x81> .text:40068e: mov eax,0x1 .text:400693: jmp 4006c8 <main+0xb4> .text:400695: movzx eax,BYTE PTR [rbp-0x10f] .text:40069c: cmp al,0x62 .text:40069e: je 4006a7 <main+0x93> .text:4006a0: mov eax,0x1 .text:4006a5: jmp 4006c8 <main+0xb4> .text:4006a7: movzx eax,BYTE PTR [rbp-0x10e] .text:4006ae: cmp al,0x63 .text:4006b0: je 4006b9 <main+0xa5> .text:4006b2: mov eax,0x1 .text:4006b7: jmp 4006c8 <main+0xb4> .text:4006b9: mov edi,0x4007c7 .text:4006be: call 4004e0 <puts@plt> .text:4006c3: mov eax,0x0 .text:4006c8: leave .text:4006c9: ret

This code is pretty simple and if we taint the datas used in our serial.txt, we have something like that:

$ printf "xxx" > serial.txt $ ../../../pin -t ./obj-intel64/ConcolicExecution.so -taint-file serial.txt -- ./crackme1 [TAINT] bytes tainted from 0x7fff194a6600 to 0x7fff194a6700 (via read) [READ in 7fff194a6600] 400683: movzx eax, byte ptr [rbp-0x110] eax is now tainted [FOLLOW] 40068a: cmp al, 0x61 [SPREAD] 40068e: mov eax, 0x1 output: eax | input: constant eax is now freed

Now, the real question is: Where does start and stop the equation? I think it's real good/complicated question and I
am currently still working on that! However, in your case, we will start an equation when a byte controllable by the user
is **LOAD** and we will stop it when the "**cmp**" instruction occurs. We will also assign an
unique ID for each constraint.

$ printf "xxx" > serial.txt $ ../../../pin -t ./obj-intel64/ConcolicExecution.so -taint-file serial.txt -- ./crackme1 [TAINT] bytes tainted from 0x7fff194a6600 to 0x7fff194a6700 (via read) [READ in 7fff194a6600] 400683: movzx eax, byte ptr [rbp-0x110] [Constraint] #0 = 0x78 eax is now tainted [FOLLOW] 40068a: cmp al, 0x61 [Equation] cmp(#0, 0x61) [Equation] cmp(x, 0x61) [SPREAD] 40068e: mov eax, 0x1 output: eax | input: constant eax is now freed

As you can see above, we assign the first constraint with the unique ID **#0**. This constraint was the first,
so we tag it to remember that's possible to control it via the user input. Then, when the "**cmp**" occurs, we
display the full equation.

To maintain a link between a register and a constraint number, a table is updated. When a constraint is assigned, it's also assigned to a register.

That means `eax = #0 = 0x78`

- 0x78 is our first character in our serial. Then `cmp(al, 0x61) = cmp(#0, 0x61)`

because `eax = #0`

and `cmp(#0, 0x61) = cmp(x, 0x61)`

because `#0`

is the first constraint of our equation.

Now to solve this equation we just use Z3.

$ printf "xxx" > serial.txt $ ../../../pin -t ./obj-intel64/ConcolicExecution.so -taint-file serial.txt -- ./crackme1 [TAINT] bytes tainted from 0x7fff194a6600 to 0x7fff194a6700 (via read) [READ in 7fff194a6600] 400683: movzx eax, byte ptr [rbp-0x110] [Constraint] #0 = 0x78 eax is now tainted [FOLLOW] 40068a: cmp al, 0x61 [Equation] cmp(#0, 0x61) [Equation] cmp(x, 0x61) [Z3 Solver]------------------------------------- (solver (= x #x00000061)) (define-fun x () (_ BitVec 32) #x00000061) The good value is 0x61 [Z3 Solver]------------------------------------- [SPREAD] 40068e: mov eax, 0x1 output: eax | input: constant eax is now freed

Z3 tries to solve this equation `(= x #x00000061))`

and finds that the result is `0x61`

. At this
time, the Pin tool writes the good character (0x61) in our serial.txt.

#### 3.4 - Demo on the first crackme

To solve this crackme and to generate the good serial.txt, we need to run three times this Pin tool. For each execution, one character is found and written in the serial file.

$ printf "xxx" > serial.txt $ ../../../pin -t ./obj-intel64/ConcolicExecution.so -taint-file serial.txt -- ./crackme1 [TAINT] bytes tainted from 0x7fff065b1ab0 to 0x7fff065b1bb0 (via read) [READ in 7fff065b1ab0] 400683: movzx eax, byte ptr [rbp-0x110] [Constraint] #0 = 0x78 eax is now tainted [FOLLOW] 40068a: cmp al, 0x61 [Equation] cmp(#0, 0x61) [Equation] cmp(x, 0x61) [Z3 Solver]------------------------------------- (solver (= x #x00000061)) (define-fun x () (_ BitVec 32) #x00000061) The good value is 0x61 [Z3 Solver]------------------------------------- [SPREAD] 40068e: mov eax, 0x1 output: eax | input: constant eax is now freed $ cat serial.txt a% $ ../../../pin -t ./obj-intel64/ConcolicExecution.so -taint-file serial.txt -- ./crackme1 [TAINT] bytes tainted from 0x7fff0c1677a0 to 0x7fff0c1678a0 (via read) [READ in 7fff0c1677a0] 400683: movzx eax, byte ptr [rbp-0x110] [Constraint] #0 = 0x61 eax is now tainted [FOLLOW] 40068a: cmp al, 0x61 [Equation] cmp(#0, 0x61) [Equation] cmp(x, 0x61) [Z3 Solver]------------------------------------- (solver (= x #x00000061)) (define-fun x () (_ BitVec 32) #x00000061) The good value is 0x61 [Z3 Solver]------------------------------------- [READ in 7fff0c1677a1] 400695: movzx eax, byte ptr [rbp-0x10f] [Constraint] #1 = 0x00 eax is already tainted [FOLLOW] 40069c: cmp al, 0x62 [Equation] cmp(#1, 0x62) [Equation] cmp(cmp(x, 0x61), 0x62) [Z3 Solver]------------------------------------- (solver (= x #x00000062)) (define-fun x () (_ BitVec 32) #x00000062) The good value is 0x62 [Z3 Solver]------------------------------------- [SPREAD] 4006a0: mov eax, 0x1 output: eax | input: constant eax is now freed $ cat serial.txt ab% $ ../../../pin -t ./obj-intel64/ConcolicExecution.so -taint-file serial.txt -- ./crackme1 [TAINT] bytes tainted from 0x7fff4acd2e60 to 0x7fff4acd2f60 (via read) [READ in 7fff4acd2e60] 400683: movzx eax, byte ptr [rbp-0x110] [Constraint] #0 = 0x61 eax is now tainted [FOLLOW] 40068a: cmp al, 0x61 [Equation] cmp(#0, 0x61) [Equation] cmp(x, 0x61) [Z3 Solver]------------------------------------- (solver (= x #x00000061)) (define-fun x () (_ BitVec 32) #x00000061) The good value is 0x61 [Z3 Solver]------------------------------------- [READ in 7fff4acd2e61] 400695: movzx eax, byte ptr [rbp-0x10f] [Constraint] #1 = 0x62 eax is already tainted [FOLLOW] 40069c: cmp al, 0x62 [Equation] cmp(#1, 0x62) [Equation] cmp(cmp(x, 0x61), 0x62) [Z3 Solver]------------------------------------- (solver (= x #x00000062)) (define-fun x () (_ BitVec 32) #x00000062) The good value is 0x62 [Z3 Solver]------------------------------------- [READ in 7fff4acd2e62] 4006a7: movzx eax, byte ptr [rbp-0x10e] [Constraint] #2 = 0x00 eax is already tainted [FOLLOW] 4006ae: cmp al, 0x63 [Equation] cmp(#2, 0x63) [Equation] cmp(cmp(cmp(x, 0x61), 0x62), 0x63) [Z3 Solver]------------------------------------- (solver (= x #x00000063)) (define-fun x () (_ BitVec 32) #x00000063) The good value is 0x63 [Z3 Solver]------------------------------------- [SPREAD] 4006b2: mov eax, 0x1 output: eax | input: constant eax is now freed $ cat serial.txt abc% $ ./crackme1 Good boy

#### 3.5 - Another crackme using XOR-based algorithm

To complicate things a bit, let's use this following dumb crackme using an XOR-based algorithm.

#include <stdio.h> #include <sys/types.h> #include <stdlib.h> #include <fcntl.h> char *serial = "\x30\x39\x3c\x21\x30"; int main(void) { int fd, i = 0; char buf[260] = {0}; char *r = buf; fd = open("serial.txt", O_RDONLY); read(fd, r, 256); close(fd); while (i < 5){ if ((*r ^ (0x55)) != *serial) return 0; r++, serial++, i++; } if (!*r) printf("Good boy\n"); return 0; }

This code reads and applies an XOR with the constant key "0x55" on each character in the serial file. Then, it checks the result with a constant string serial. This code is intersting to study the execution concolic, because we have a simple algorithm. On the following CFG, the blue blox is our algorithm.

Now. let's see what happens when we taint and follow our datas from the serial file.

$ printf "xxx" > ./serial.txt $ ../../../pin -t obj-intel64/ConcolicExecution.so -taint-file serial.txt -- ./crackme2 [TAINT] bytes tainted from 0x7fff3cab6cc0 to 0x7fff3cab6dc0 (via read) [READ in 7fff3cab6cc0] 400698: movzx eax, byte ptr [rax] eax is now tainted [SPREAD] 40069b: mov edx, eax output: edx | input: eax edx is now tainted [FOLLOW] 40069b: mov edx, eax [FOLLOW] 4195997: xor edx, 0x55 [READ in 4007ec] 4006a7: movzx eax, byte ptr [rax] eax is now freed [FOLLOW] 4006aa: cmp dl, al [SPREAD] 7feb884e67db: mov edx, 0x1 output: edx | input: constant edx is now freed

Same for the first example, we need to assign a unique constraint for each spread. Then, when the **cmp** instruction
occurs, we need to solve the equation via Z3.

$ ../../../pin -t obj-intel64/ConcolicExecution.so -taint-file serial.txt -- ./crackme2 [TAINT] bytes tainted from 0x7fff3cab6cc0 to 0x7fff3cab6dc0 (via read) [READ in 7fff3cab6cc0] 400698: movzx eax, byte ptr [rax] [Constraint] #0 = 0x61 eax is now tainted [SPREAD] 40069b: mov edx, eax output: edx | input: eax edx is now tainted [FOLLOW] 40069b: mov edx, eax [Constraint] #1 = #0 [FOLLOW] 4195997: xor edx, 0x55 [Constraint] #2 = xor(#1, 0x55) [READ in 4007ec] 4006a7: movzx eax, byte ptr [rax] eax is now freed [FOLLOW] 4006aa: cmp dl, al [Equation] cmp(#2, 0x30) [Equation] cmp(xor(x, 0x55), 0x30) [Z3 Solver]------------------------------------- (solver (= (bvxor x #x00000055) #x00000030)) (define-fun x () (_ BitVec 32) #x00000065) The good value is 0x65 [Z3 Solver]------------------------------------- [SPREAD] 7feb884e67db: mov edx, 0x1 output: edx | input: constant edx is now freed $ cat serial.txt e% $

As you can see above, my constraint on the **xor** instruction looks like that: `xor(#1, 0x55)`

, it means we need to
display/follow all ALU operations on a specific convention. Like:

add(a, b) sub(a, b) mul(a, b) div(a, b) xor(a, b) ...

This is a real problem with Pin. Because it doesn't provide an IR, we need to implement all operations.
For example, with the **xor** instruction, we need to catch these following encoding:

xor reg, reg xor mem, reg xor reg, mem xor reg, immed xor mem, immed xor accum, immed

Then, when we need to build our equation like `cmp(#2, 0x30)`

, we need to replace the constraint number by its content -
And for that we will use the constraints table.

After the first constraint solved, we set the first character in the serial file and we re-run the Pin tool to solve the second constraint. We repeat this operation until all constraints are solved. The following diagram represent our executions. As you can see, for each execution, only one constraint is solved.

And the full result which generates a valide file key is pasted below. As you can see, for each execution, one character is found until the valide key.

$ printf "xxx" > ./serial.txt $ ../../../pin -t ./obj-intel64/ConcolicExecution.so -taint-file serial.txt -- ./crackme1 [TAINT] bytes tainted from 0x7fff2d60e7d0 to 0x7fff2d60e8d0 (via read) [READ in 7fff2d60e7d0] 400698: movzx eax, byte ptr [rax] [Constraint] #0 = 0x41 eax is now tainted [SPREAD] 40069b: mov edx, eax output: edx | input: eax edx is now tainted [FOLLOW] 40069b: mov edx, eax [Constraint] #1 = #0 [FOLLOW] 4195997: xor edx, 0x55 [Constraint] #2 = xor(#1, 0x55) [READ in 4007ec] 4006a7: movzx eax, byte ptr [rax] eax is now freed [FOLLOW] 4006aa: cmp dl, al [Equation] cmp(#2, 0x30) [Equation] cmp(xor(x, 0x55), 0x30) [Z3 Solver]------------------------------------- (solver (= (bvxor x #x00000055) #x00000030)) (define-fun x () (_ BitVec 32) #x00000065) The good value is 0x65 [Z3 Solver]------------------------------------- [SPREAD] 7ff3541837db: mov edx, 0x1 output: edx | input: constant edx is now freed $ cat serial.txt e% $ ../../../pin -t ./obj-intel64/ConcolicExecution.so -taint-file serial.txt -- ./crackme1 [TAINT] bytes tainted from 0x7fff6d1f8730 to 0x7fff6d1f8830 (via read) [READ in 7fff6d1f8730] 400698: movzx eax, byte ptr [rax] [Constraint] #0 = 0x65 eax is now tainted [SPREAD] 40069b: mov edx, eax output: edx | input: eax edx is now tainted [FOLLOW] 40069b: mov edx, eax [Constraint] #1 = #0 [FOLLOW] 4195997: xor edx, 0x55 [Constraint] #2 = xor(#1, 0x55) [READ in 4007ec] 4006a7: movzx eax, byte ptr [rax] eax is now freed [FOLLOW] 4006aa: cmp dl, al [Equation] cmp(#2, 0x30) [Equation] cmp(xor(x, 0x55), 0x30) [Z3 Solver]------------------------------------- (solver (= (bvxor x #x00000055) #x00000030)) (define-fun x () (_ BitVec 32) #x00000065) The good value is 0x65 [Z3 Solver]------------------------------------- [READ in 7fff6d1f8731] 400698: movzx eax, byte ptr [rax] [Constraint] #3 = 0x00 eax is now tainted [FOLLOW] 40069b: mov edx, eax [Constraint] #4 = #3 [FOLLOW] 4195997: xor edx, 0x55 [Constraint] #5 = xor(#4, 0x55) [READ in 4007ed] 4006a7: movzx eax, byte ptr [rax] eax is now freed [FOLLOW] 4006aa: cmp dl, al [Equation] cmp(#5, 0x39) [Equation] cmp(xor(x, 0x55), 0x39) [Z3 Solver]------------------------------------- (solver (= (bvxor x #x00000055) #x00000039)) (define-fun x () (_ BitVec 32) #x0000006c) The good value is 0x6c [Z3 Solver]------------------------------------- [SPREAD] 7fe0b6aa47db: mov edx, 0x1 output: edx | input: constant edx is now freed $ cat serial.txt el% $ ../../../pin -t ./obj-intel64/ConcolicExecution.so -taint-file serial.txt -- ./crackme1 [TAINT] bytes tainted from 0x7fff2d1e1e00 to 0x7fff2d1e1f00 (via read) [READ in 7fff2d1e1e00] 400698: movzx eax, byte ptr [rax] [Constraint] #0 = 0x65 eax is now tainted [SPREAD] 40069b: mov edx, eax output: edx | input: eax edx is now tainted [FOLLOW] 40069b: mov edx, eax [Constraint] #1 = #0 [FOLLOW] 4195997: xor edx, 0x55 [Constraint] #2 = xor(#1, 0x55) [READ in 4007ec] 4006a7: movzx eax, byte ptr [rax] eax is now freed [FOLLOW] 4006aa: cmp dl, al [Equation] cmp(#2, 0x30) [Equation] cmp(xor(x, 0x55), 0x30) [Z3 Solver]------------------------------------- (solver (= (bvxor x #x00000055) #x00000030)) (define-fun x () (_ BitVec 32) #x00000065) The good value is 0x65 [Z3 Solver]------------------------------------- [READ in 7fff2d1e1e01] 400698: movzx eax, byte ptr [rax] [Constraint] #3 = 0x6c eax is now tainted [FOLLOW] 40069b: mov edx, eax [Constraint] #4 = #3 [FOLLOW] 4195997: xor edx, 0x55 [Constraint] #5 = xor(#4, 0x55) [READ in 4007ed] 4006a7: movzx eax, byte ptr [rax] eax is now freed [FOLLOW] 4006aa: cmp dl, al [Equation] cmp(#5, 0x39) [Equation] cmp(xor(x, 0x55), 0x39) [Z3 Solver]------------------------------------- (solver (= (bvxor x #x00000055) #x00000039)) (define-fun x () (_ BitVec 32) #x0000006c) The good value is 0x6c [Z3 Solver]------------------------------------- [READ in 7fff2d1e1e02] 400698: movzx eax, byte ptr [rax] [Constraint] #6 = 0x00 eax is now tainted [FOLLOW] 40069b: mov edx, eax [Constraint] #7 = #6 [FOLLOW] 4195997: xor edx, 0x55 [Constraint] #8 = xor(#7, 0x55) [READ in 4007ee] 4006a7: movzx eax, byte ptr [rax] eax is now freed [FOLLOW] 4006aa: cmp dl, al [Equation] cmp(#8, 0x3c) [Equation] cmp(xor(x, 0x55), 0x3c) [Z3 Solver]------------------------------------- (solver (= (bvxor x #x00000055) #x0000003c)) (define-fun x () (_ BitVec 32) #x00000069) The good value is 0x69 [Z3 Solver]------------------------------------- [SPREAD] 7f7e919ef7db: mov edx, 0x1 output: edx | input: constant edx is now freed $ cat serial.txt eli% $ ../../../pin -t ./obj-intel64/ConcolicExecution.so -taint-file serial.txt -- ./crackme1 [TAINT] bytes tainted from 0x7fff597b37a0 to 0x7fff597b38a0 (via read) [READ in 7fff597b37a0] 400698: movzx eax, byte ptr [rax] [Constraint] #0 = 0x65 eax is now tainted [SPREAD] 40069b: mov edx, eax output: edx | input: eax edx is now tainted [FOLLOW] 40069b: mov edx, eax [Constraint] #1 = #0 [FOLLOW] 4195997: xor edx, 0x55 [Constraint] #2 = xor(#1, 0x55) [READ in 4007ec] 4006a7: movzx eax, byte ptr [rax] eax is now freed [FOLLOW] 4006aa: cmp dl, al [Equation] cmp(#2, 0x30) [Equation] cmp(xor(x, 0x55), 0x30) [Z3 Solver]------------------------------------- (solver (= (bvxor x #x00000055) #x00000030)) (define-fun x () (_ BitVec 32) #x00000065) The good value is 0x65 [Z3 Solver]------------------------------------- [READ in 7fff597b37a1] 400698: movzx eax, byte ptr [rax] [Constraint] #3 = 0x6c eax is now tainted [FOLLOW] 40069b: mov edx, eax [Constraint] #4 = #3 [FOLLOW] 4195997: xor edx, 0x55 [Constraint] #5 = xor(#4, 0x55) [READ in 4007ed] 4006a7: movzx eax, byte ptr [rax] eax is now freed [FOLLOW] 4006aa: cmp dl, al [Equation] cmp(#5, 0x39) [Equation] cmp(xor(x, 0x55), 0x39) [Z3 Solver]------------------------------------- (solver (= (bvxor x #x00000055) #x00000039)) (define-fun x () (_ BitVec 32) #x0000006c) The good value is 0x6c [Z3 Solver]------------------------------------- [READ in 7fff597b37a2] 400698: movzx eax, byte ptr [rax] [Constraint] #6 = 0x69 eax is now tainted [FOLLOW] 40069b: mov edx, eax [Constraint] #7 = #6 [FOLLOW] 4195997: xor edx, 0x55 [Constraint] #8 = xor(#7, 0x55) [READ in 4007ee] 4006a7: movzx eax, byte ptr [rax] eax is now freed [FOLLOW] 4006aa: cmp dl, al [Equation] cmp(#8, 0x3c) [Equation] cmp(xor(x, 0x55), 0x3c) [Z3 Solver]------------------------------------- (solver (= (bvxor x #x00000055) #x0000003c)) (define-fun x () (_ BitVec 32) #x00000069) The good value is 0x69 [Z3 Solver]------------------------------------- [READ in 7fff597b37a3] 400698: movzx eax, byte ptr [rax] [Constraint] #9 = 0x00 eax is now tainted [FOLLOW] 40069b: mov edx, eax [Constraint] #10 = #9 [FOLLOW] 4195997: xor edx, 0x55 [Constraint] #11 = xor(#10, 0x55) [READ in 4007ef] 4006a7: movzx eax, byte ptr [rax] eax is now freed [FOLLOW] 4006aa: cmp dl, al [Equation] cmp(#11, 0x21) [Equation] cmp(xor(x, 0x55), 0x21) [Z3 Solver]------------------------------------- (solver (= (bvxor x #x00000055) #x00000021)) (define-fun x () (_ BitVec 32) #x00000074) The good value is 0x74 [Z3 Solver]------------------------------------- [SPREAD] 7f9ac23db7db: mov edx, 0x1 output: edx | input: constant edx is now freed $ cat serial.txt elit% $ ../../../pin -t ./obj-intel64/ConcolicExecution.so -taint-file serial.txt -- ./crackme1 [TAINT] bytes tainted from 0x7fff313be550 to 0x7fff313be650 (via read) [READ in 7fff313be550] 400698: movzx eax, byte ptr [rax] [Constraint] #0 = 0x65 eax is now tainted [SPREAD] 40069b: mov edx, eax output: edx | input: eax edx is now tainted [FOLLOW] 40069b: mov edx, eax [Constraint] #1 = #0 [FOLLOW] 4195997: xor edx, 0x55 [Constraint] #2 = xor(#1, 0x55) [READ in 4007ec] 4006a7: movzx eax, byte ptr [rax] eax is now freed [FOLLOW] 4006aa: cmp dl, al [Equation] cmp(#2, 0x30) [Equation] cmp(xor(x, 0x55), 0x30) [Z3 Solver]------------------------------------- (solver (= (bvxor x #x00000055) #x00000030)) (define-fun x () (_ BitVec 32) #x00000065) The good value is 0x65 [Z3 Solver]------------------------------------- [READ in 7fff313be551] 400698: movzx eax, byte ptr [rax] [Constraint] #3 = 0x6c eax is now tainted [FOLLOW] 40069b: mov edx, eax [Constraint] #4 = #3 [FOLLOW] 4195997: xor edx, 0x55 [Constraint] #5 = xor(#4, 0x55) [READ in 4007ed] 4006a7: movzx eax, byte ptr [rax] eax is now freed [FOLLOW] 4006aa: cmp dl, al [Equation] cmp(#5, 0x39) [Equation] cmp(xor(x, 0x55), 0x39) [Z3 Solver]------------------------------------- (solver (= (bvxor x #x00000055) #x00000039)) (define-fun x () (_ BitVec 32) #x0000006c) The good value is 0x6c [Z3 Solver]------------------------------------- [READ in 7fff313be552] 400698: movzx eax, byte ptr [rax] [Constraint] #6 = 0x69 eax is now tainted [FOLLOW] 40069b: mov edx, eax [Constraint] #7 = #6 [FOLLOW] 4195997: xor edx, 0x55 [Constraint] #8 = xor(#7, 0x55) [READ in 4007ee] 4006a7: movzx eax, byte ptr [rax] eax is now freed [FOLLOW] 4006aa: cmp dl, al [Equation] cmp(#8, 0x3c) [Equation] cmp(xor(x, 0x55), 0x3c) [Z3 Solver]------------------------------------- (solver (= (bvxor x #x00000055) #x0000003c)) (define-fun x () (_ BitVec 32) #x00000069) The good value is 0x69 [Z3 Solver]------------------------------------- [READ in 7fff313be553] 400698: movzx eax, byte ptr [rax] [Constraint] #9 = 0x74 eax is now tainted [FOLLOW] 40069b: mov edx, eax [Constraint] #10 = #9 [FOLLOW] 4195997: xor edx, 0x55 [Constraint] #11 = xor(#10, 0x55) [READ in 4007ef] 4006a7: movzx eax, byte ptr [rax] eax is now freed [FOLLOW] 4006aa: cmp dl, al [Equation] cmp(#11, 0x21) [Equation] cmp(xor(x, 0x55), 0x21) [Z3 Solver]------------------------------------- (solver (= (bvxor x #x00000055) #x00000021)) (define-fun x () (_ BitVec 32) #x00000074) The good value is 0x74 [Z3 Solver]------------------------------------- [READ in 7fff313be554] 400698: movzx eax, byte ptr [rax] [Constraint] #12 = 0x00 eax is now tainted [FOLLOW] 40069b: mov edx, eax [Constraint] #13 = #12 [FOLLOW] 4195997: xor edx, 0x55 [Constraint] #14 = xor(#13, 0x55) [READ in 4007f0] 4006a7: movzx eax, byte ptr [rax] eax is now freed [FOLLOW] 4006aa: cmp dl, al [Equation] cmp(#14, 0x30) [Equation] cmp(xor(x, 0x55), 0x30) [Z3 Solver]------------------------------------- (solver (= (bvxor x #x00000055) #x00000030)) (define-fun x () (_ BitVec 32) #x00000065) The good value is 0x65 [Z3 Solver]------------------------------------- [SPREAD] 7f0d00e1f7db: mov edx, 0x1 output: edx | input: constant edx is now freed $ cat serial.txt elite% $ ./crackme1 Good boy

### 4 - Conclusion

I think that the concolic execution is a great technique and it need to be investigated and improved. I hope that more and more people will look into it. Also, I think it isn't a good idea to do a concolic execution with a DBI (Dynamic Binary Instrumentation) without intermediate language like Pin. Why? Because without IR, you need to implement all instructions set and their different encodings. This is possible but that's really boring and you can forget an operation... To the theorem solver conclusion, I'm not a Z3 expert, I do know it's used internally by Microsoft for a lot of purpose (I guess they got pretty big equations), but I have only used it with toy-equations, so I can't really say.

#### 4.1 - My Pin tool

First of all, my Pin tool is **not** reliable and it works only with the above examples... I only implemented the instruction
necessary for my examples (mov, cmp, xor). So, if you want use it, you need to implement all the x86 instructions... This Pin tool is just
a PoC but it can give you a base to your project. The sources are here.

#### 4.2 - References

- Pin API
- Z3 C++ API
- Taint analysis and pattern matching with Pin
- Concolic execution - Taint analysis with Valgrind and constraints path solver with Z3

#### 4.3 - Special thanks

I would like to thanks Axel "0vercl0k" Souchet for his skills in Z3 and proofreading.