# HackingWeek 2015 - Reverse 4

How we managed to solve a Keygenme with Python and Z3 a high-performance theorem prover.

## Introduction

This Reverse Engineering challenge was probably the most interesting one I ever solved. It took me a few days to complete it but it was totally worth it because I learned about symbolic execution and how to use Z3 The Theorem Prover.

I will write more articles about Z3 in a near future but until a later time I will explain how to solve this challenge.

## Context

The goal of this Reverse Engineering challenge is to find the password for which the given ELF 64-bit binary will print "Success !".
To make the solving a bit easier we are given a few hints :

• The password must be alphanumeric [a-zA-Z0-9].
• The md5sum of the expected password is 3efafa3e161a756e6e1711dbceaf9d68.

## Static Analysis

We can say that the binary is quite small, it is less than 4 Kb, we won't have too much code to analyse.

The interesting part of the code is located between `0x04006A0` and `0x04008F9`.
We can find a hashing routine from `0x04006A0` to `0x040085D` which we will name calculate and a routine to check if a hash is valid from `0x0400863` to `0x04008F9` which we will name verify.

### Calculate

• The routine calculate iterates for each bytes of the password.
• The value of the hash is stored in `RCX`.
• After `0x040070D` `RCX` is always equals to `0x555555`.

### Verify

• The routine verify takes `RCX` as only argument.
• If the hash is valid the routine verify returns 1, otherwise it returns 0.

## Finding the valid hash

So the first step is to find for which hash the routine verify will return 1.
When the routine calculate jumps to verify.
Because `RCX` is a 64 bit register, trying all values of `RCX` to find a valid hash would take too much time, we need to do something smarter.

### Finding the valid hash with Z3

Z3 is a high-performance theorem prover being developed at Microsoft Research. It is able to solve or simplify complex equations. We are going to use Z3 Python binding to solve several steps of this challenge.

The first step was to convert the Assembly code to Python, since the code is not too large we can do it in a few minutes by hand.
The second step is to make the script comply with Z3. Sometimes you have to specify between Arithmetic and Logic operations.

### Verify script

``````#!/usr/bin/env python
from Z3 import *

def get_models(F):
result = []
s = Solver()
while True:
if s.check() == sat:
m = s.model()
result.append(m)
block = []
for d in m:
if d.arity() > 0:
raise Z3Exception("uninterpreted functions are not supported")
c = d()
if is_array(c) or c.sort().kind() == Z3_UNINTERPRETED_SORT:
raise Z3Exception("arrays and uninterpreted sorts are not supported")
block.append(c != m[d])
else:
return result

def verify(rcx):
rax = 0x0A5E3C04BB1623035
rdx = 0x0E4957041B271F986
rsi = rcx
rax = (rax + rcx * 2)
rax = rax & 0x0FFFFFFFFFFFFFFFE
rdx = (rdx + rax)
rax = 0x0DE9BC364362C55EF
rsi = (rsi - rdx)
rdi = (rax + rsi * 2)
rax = (rax - rcx)
rax = (rax + rdx)
rdi = rdi & 0x0FFFFFFFFFFFFFFFE
rdx = 0x54780300041002
rsi = (rsi - rdi)
rcx = (rax + rdi)
rax = (rax + rsi * 2)
rax = rax & rdx
rdx = 0x23F3F28C54D59B2E
rax = (rax + rcx)
rcx = rax
rax = (~rax)
rcx = rcx ^ rdx
rax = rax & rdx
rcx = rcx | rdx
return (rcx == rax)

if __name__ == "__main__":
rcx = BitVec("rcx", 64)

F = [
verify(rcx)
]

for x in get_models(F):
print(x)``````

### Verify solution

In less than one second the code above found the only satisfying solution which is `rcx = 9211484110692677630`.
It means that the routine verify returns 1 only if `RCX` is equal to 9211484110692677630.

We have to find for which passwords calculate set `RCX` to 9211484110692677630.

This time we are implementing the calculate routine.

``````#!/usr/bin/env python
from Z3 import *

def display_model(m):
block = {}
for x in m:
if "b" in str(x):
block[ord(str(x)[-1:])] = int(str(m[x]))

def get_models(F):
s = Solver()
while True:
if s.check() == sat:
m = s.model()
display_model(m)
block = []
for d in m:
if d.arity() > 0:
raise Z3Exception("uninterpreted functions are not supported")
c = d()
if is_array(c) or c.sort().kind() == Z3_UNINTERPRETED_SORT:
raise Z3Exception("arrays and uninterpreted sorts are not supported")
block.append(c != m[d])
else:
print("done")
break

rax, rbx, rcx, rsi, rbp, r8, r9, r10, r11, r12, r13, r14, r15 = BitVecs("rax rbx rcx rsi rbp r8 r9 r10 r11 r12 r13 r14 r15", 64)

i = BitVec("i", 8)

rcx = 0x555555

r13 = 0x2EFA16D0D7B56313
r12 = 0x0D105E92F284A9CED
rbp = 0x0C2FDC6E7E84BDF1B
r9 = 0x0F1B06F67F7109574
r8 = 0x9CBCAF82CBBB622E
rbx = 0x80238EB2DA65B738
rsi = 0x8BCDCD41F52A3FD
r10 = 0x37D59EC93CC6D155

rax = rdx
r14 = rcx
rdx = (rdx + rdx)
r15 = r8
r14 = (~r14)
r14 = (r14 + r14)
rdx = rdx & r14
rcx = (rcx + rdx)
rdx = rax
rcx = (rcx * r13)
rdx = (rdx * r12)
rdx = (rdx + rcx)
rdx = (rdx * rbp)
r14 = rdx
rdx = rdx | r9
r14 = r14 & r9
rcx = rdx
rax = r14
rcx = (rcx - r14)
rax = (rax - rdx)
rcx = (rcx + rcx)
rax = (rax + rax)
rcx = rcx & r8
r15 = (r15 - rax)
rax = r15
r15 = rcx
r15 = (-r15)
rax = (rax + r15 * 2)
r14 = (r14 * r11)
rax = rax & rbx
rax = (rax + rcx)
rcx = 0x718FE0E52CEF734C
rdx = (rdx * rsi)
rax = (rax * rsi)
rdx = (rdx + r14)
rax = (rax - rdx)
rdx = 0x75D7C82EBB4962B9
rax = (rax * r10)
rax = (rax + rcx)
rcx = rax
rax = LShR(rax, 0x19)
r14 = rax
rcx = (rcx << 0x07)
r14 = (~r14)
r14 = r14 | rdx
r15 = (rax + r14 + 1)
r14 = r15
r15 = r15 & rcx
r14 = r14 ^ rcx
r14 = (r14 + r15)
rax = rax | rdx
rax = (rax - rdx )
rdx = rax
rax = rcx
rax = (~rax)
rax = rax & rdx
rax = (rax + rcx)
rcx = r14
rcx = rcx ^ rax
rax = rax & r14
rcx = (rcx + rax)
return rcx

def is_alphanum(x):
return Or(And(x >= 0x41, x <= 0x5a), And(x >= 0x61, x <= 0x7a), And(x >= 0x30, x <= 0x39))

if __name__ == "__main__":
F = []
length = 10
checksum = BitVec("checksum", 64)
password = [BitVec("b%d" % i, 64) for i in range(length)]

F.extend([
checksum == 9211484110692677630,
])

get_models(F)``````

### calculate output

UhoJ0yam0h
STjH0NBA2l
STzH0JDK0h
STjBpJFK1l
WDnBpkbs0n
WDnJpkbS0n
ZTjJ0SFW7j

The Python script will print a large amount of valid passwords but it might take days before it find the password we are looking for.
We need to develop something faster than Z3 but with the same rules and less voodoo magic.

Z3 the theorem prover will help us to create rules, instead of using `is_alphanum` we will try all alphanumeric char on each `RDX` values.
This will give us all possible characters for the password.

### Get combinations

Using Z3 we are able to find all possible characters for a password of length 10.

``````# password [104, 105, 106, 107, 108, 109, 110, 111]
# password [48, 49, 50, 51, 52, 53, 54, 55, 97, 98, 99, 100, 101, 102, 103, 112, 113, 114, 115, 116, 117, 118, 119]
# password [49, 51, 53, 55, 57, 65, 67, 69, 71, 73, 75, 77, 79, 81, 83, 85, 87, 89, 97, 99, 101, 103, 105, 107, 109, 111, 113, 115, 117, 119, 121]
# password [65, 66, 67, 68, 69, 70, 71, 97, 98, 99, 100, 101, 102, 103]
# password [48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90, 97, 98, 99, 100, 101, 102, 103, 104, 105, 106, 107, 108, 109, 110, 111, 112, 113, 114, 115, 116, 117, 118, 119, 120, 121, 122]
# password [66, 72, 74, 98, 104, 106]
# password [106, 107, 110, 111, 122]
# password [48, 52, 56, 68, 72, 76, 80, 84, 88, 100, 104, 108, 112, 116, 120]
# password [80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90]``````

### Bruteforcing

I implemented my own script which will try all the combinations with the rules defined by Z3.
During the competition I split the tasks on 8 threads to reduce the time of the attack because there are 49,015,612,800 possibilities and my laptop is rather slow.

``````#!/usr/bin/env python
import itertools
import hashlib

CHECKSUM = "3efafa3e161a756e6e1711dbceaf9d68"

def start_brute():
values = [
[80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90],
[48, 52, 56, 68, 72, 76, 80, 84, 88, 100, 104, 108, 112, 116, 120],
[106, 107, 110, 111, 122],
[66, 72, 74, 98, 104, 106],
[48, 112],
[48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90, 97, 98, 99, 100, 101, 102, 103, 104, 105, 106, 107, 108, 109, 110, 111, 112, 113, 114, 115, 116, 117, 118, 119, 120, 121, 122],
[65, 66, 67, 68, 69, 70, 71, 97, 98, 99, 100, 101, 102, 103],
[49, 51, 53, 55, 57, 65, 67, 69, 71, 73, 75, 77, 79, 81, 83, 85, 87, 89, 97, 99, 101, 103, 105, 107, 109, 111, 113, 115, 117, 119, 121],
[48, 49, 50, 51, 52, 53, 54, 55, 97, 98, 99, 100, 101, 102, 103, 112, 113, 114, 115, 116, 117, 118, 119],
[104, 105, 106, 107, 108, 109, 110, 111]
]

expression = [map(chr, x) for x in values]
combinations = itertools.product(*expression)

for x in combinations: