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
0x040070DRCXis always equals to0x555555.
Verify
- The routine verify takes
RCXas 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()
s.add(F)
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])
s.add(Or(block))
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 = 0x2BB33127ADA5CBCA
rax = (rax - rcx)
rax = (rax + rdx)
rdi = rdi & 0x0FFFFFFFFFFFFFFFE
rdx = 0x54780300041002
rsi = (rsi - rdi)
rcx = (rax + rdi)
rax = 0x0A84525ADA4B05868
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.
Finding valid passwords
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]))
password = "".join(map(chr, block.values()))
print(password)
def get_models(F):
s = Solver()
s.add(F)
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])
s.add(Or(block))
else:
print("done")
break
def calculate(password):
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
for i in range(len(password)):
r13 = 0x2EFA16D0D7B56313
r12 = 0x0D105E92F284A9CED
rbp = 0x0C2FDC6E7E84BDF1B
r9 = 0x0F1B06F67F7109574
r8 = 0x9CBCAF82CBBB622E
rbx = 0x80238EB2DA65B738
rsi = 0x8BCDCD41F52A3FD
r11 = 0x0F743232BE0AD5C03
r10 = 0x37D59EC93CC6D155
rdx = password[i]
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([is_alphanum(password[i]) for i in range(length)])
F.extend([
checksum == 9211484110692677630,
calculate(password) == checksum
])
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.
Finding the expected password
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[0] [104, 105, 106, 107, 108, 109, 110, 111]
# password[1] [48, 49, 50, 51, 52, 53, 54, 55, 97, 98, 99, 100, 101, 102, 103, 112, 113, 114, 115, 116, 117, 118, 119]
# password[2] [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[3] [65, 66, 67, 68, 69, 70, 71, 97, 98, 99, 100, 101, 102, 103]
# password[4] [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[5] [48, 112]
# password[6] [66, 72, 74, 98, 104, 106]
# password[7] [106, 107, 110, 111, 122]
# password[8] [48, 52, 56, 68, 72, 76, 80, 84, 88, 100, 104, 108, 112, 116, 120]
# password[9] [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:
password = "".join(x)
h = hashlib.md5()
h.update(password)
if CHECKSUM == h.hexdigest():
print("Password Found: {:s}".format(password))
break
if __name__ == "__main__":
start_brute()Bruteforce result
After a few minutes (I got lucky) the expected password showed up on one of the 8 threads.