Use radare2 and z3 to solve a self-modifying crackme.
Information
- category : reverse
- points : 150
Description
1 file: reee.bin
Writeup
We have a 64 bit elf binary, let’s start analyzing it with radare2:
$ r2 reee.bin
[0x00400430]> aaa
[0x00400430]> i
fd 3
file reee.bin
size 0x19d8
humansz 6.5K
mode r-x
format elf64
iorw false
blksz 0x0
block 0x100
type EXEC (Executable file)
arch x86
baddr 0x400000
binsz 4753
bintype elf
bits 64
canary false
class ELF64
compiler GCC: (Ubuntu 5.4.0-6ubuntu1~16.04.12) 5.4.0 20160609
crypto false
endian little
havecode true
intrp /lib64/ld-linux-x86-64.so.2
laddr 0x0
lang c
linenum false
lsyms false
machine AMD x86-64 architecture
maxopsz 16
minopsz 1
nx true
os linux
pcalign 0
pic false
relocs false
relro partial
rpath NONE
sanitiz false
static false
stripped true
subsys linux
va true
[0x00400430]> afl
0x00400430 1 41 entry0
0x00400410 1 6 sym.imp.__libc_start_main
0x00400400 1 6 sym.imp.puts
0x0040064e 14 747 -> 195 main
0x00400500 8 134 -> 90 entry.init0
0x004004e0 3 28 entry.fini0
0x00400460 4 50 -> 41 fcn.00400460
0x00400526 1 296 fcn.00400526
0x004006e5 6 176 -> 60 fcn.004006e5
0x004003c8 3 26 fcn.004003c8
It’s a stripped binary and it’s not a PIE executable.
This it the main graph:
And this is the main decompiled:
void main(char *argc, char **argv)
{
char *placeholder_2;
code cVar1;
int64_t iVar2;
uint32_t in_ECX;
char **arg2;
char **var_40h;
undefined8 var_34h;
int32_t second_index;
int32_t index;
int64_t var_20h;
uint32_t var_18h;
arg2 = argv;
if ((int32_t)argc < 2) {
argc = "need a flag!";
sym.imp.puts();
}
placeholder_2 = argv[1];
index = 0;
while (index < 0x7a69) {
second_index = 0;
while (second_index < 0x228) {
argc = (char *)(uint32_t)fcn.004006e5[second_index];
cVar1 = (code)fcn.00400526((int64_t)argc);
fcn.004006e5[second_index] = cVar1;
second_index = second_index + 1;
}
index = index + 1;
}
iVar2 = fcn.004006e5(argc, (int64_t)arg2, placeholder_2, in_ECX);
if (iVar2 == 0) {
sym.imp.puts("Wrong!");
} else {
sym.imp.puts("Correct!");
}
return;
}
From the decompiled version we can deduce 3 things:
- The program take in input an argument (flag).
- The argument is passed to the function fcn.004006e5.
- The function fcn.004006e5 is modified in the nested while using the function fcn.00400526.
In fact if we check the asm of fcn.004006e5 is messed up:
┌ 60: fcn.004006e5 (int64_t arg2, uint32_t arg4, int64_t arg_58ae7f6ah);
│ ╎╎╎ ; arg int64_t arg_58ae7f6ah @ rbp+0x58ae7f6a
│ ╎╎╎ ; arg int64_t arg2 @ rsi
│ ╎╎╎ ; arg uint32_t arg4 @ rcx
│ ╎╎╎ 0x004006e5 stc
│ ╎╎╎ 0x004006e6 xchg eax, ebx
│ ┌────< 0x004006e7 jne 0x400716
│ │╎╎╎ 0x004006e9 fcmovnb st(0), st(6)
│ │╎╎╎ 0x004006eb stosd dword [rdi], eax
│ │╎╎└─< 0x004006ec loopne 0x400690
│ │╎╎ 0x004006ee cmp ecx, dword [rcx - 0x63] ; arg4
│ │╎╎ 0x004006f1 mov word [rsi + rax*4 - 0x23], ds ; arg2
│╎╎ 0x004006f5 invalid
│╎└──< 0x004006f6 jae 0x4006c5 ; main+0x77
│╎ 0x004006f8 stc
│╎ 0x004006f9 invalid
│╎ 0x004006fa imul ebx, dword [rax], 0x2f592932
│╎ 0x00400700 invalid
│╎ 0x00400701 cmpsd dword [rsi], dword ptr [rdi]
│╎ 0x00400702 invalid
│╎ ; CODE XREF from fcn.004006e5 @ +0x90
│╎ ┌─< 0x00400703 jns 0x40070e
│╎ │ 0x00400705 adc byte [rdi + 0x5bcbfed6], cl
│╎ │ 0x0040070b ret
│└───< 0x0040070c jo 0x4006d1 ; main+0x83
│ │ ; CODE XREF from fcn.004006e5 @ +0x1e
│ └─> 0x0040070e invalid
│ 0x0040070f invalid
│ 0x00400710 lodsb al, byte [rsi]
│ 0x00400711 xchg dword [rdx - 0x61], eax
│ ┌─< 0x00400714 jns 0x400760
│ │ │ ; CODE XREF from fcn.004006e5 @ 0x4006e7
│ └────> 0x00400716 xor eax, 0xe0bb9da8
│ │ 0x0040071c sar dword [arg_58ae7f6ah], 0xeb
│ │ 0x00400723 pop rsp
│ │ 0x00400724 add dword [rcx + 0x1dad7797], esi ; arg4
│ ╎│ 0x0040072a adc esp, ebp
│ ╎│ 0x0040072c adc byte [0x6e340251], bh
│ ┌────< 0x00400732 loop 0x40079b
│ │╎╎│ 0x00400734 mov cl, 0x79 ; 'y' ; 121
│ │╎╎│ 0x00400736 sahf
│ │╎╎│ 0x00400737 pop rsi
│ │╎╎│ 0x00400738 cmp al, 0x14 ; 20
│ │╎╎│ 0x0040073a xor cl, cl
│ │╎╎│ 0x0040073c cld
│ │╎╎│ 0x0040073d mov bh, bh
│ │╎╎│ 0x0040073f int3
│╎╎│ 0x00400740 call 0xffffffff8987d4da
│╎╎│ 0x00400745 fnstenv [rcx + 1]
│╎╎│ 0x00400748 mov bh, 0x25 ; '%' ; 37
│╎╎│ 0x0040074a and al, 0x6a ; 106
│╎╎│ 0x0040074c invalid
│╎╎│ 0x0040074d mov dh, 0xe2 ; 226
│╎╎│ 0x0040074f int1
│╎╎│ 0x00400750 sbb al, 0x5c
│╎╎│ 0x00400752 fidiv dword [rax + rdi*4 + 0x2b]
│╎╎│ 0x00400756 invalid
│╎╎│ 0x00400757 pop rbp
│╎╎│ 0x00400759 and bl, byte [rax + 0x60299194]
│╎└──< 0x0040075f jns 0x400729 ; fcn.004006e5+0x44
│└───< 0x00400761 jge 0x400730 ; fcn.004006e5+0x4b
│ 0x00400763 sub eax, 0x8e88118d
│ 0x00400768 rol byte [rdx + 0x66], cl
│ 0x0040076b sti
│ 0x0040076c xlatb
│ 0x0040076d hlt
│ 0x0040076e mov al, byte [rdx]
And it’s full of invalid instructions.
We can try to check fcn.00400526:
int32_t fcn.00400526(int64_t arg1)
{
int64_t var_4h;
*(uint8_t *)0x601161 = *(char *)0x601161 + 1;
*(uint8_t *)0x601162 = *(char *)0x601162 + *(char *)((int64_t)*(uint8_t *)0x601161 + 0x601060);
*(uint8_t *)((int64_t)*(uint8_t *)0x601161 + 0x601060) =
*(uint8_t *)((int64_t)*(uint8_t *)0x601161 + 0x601060) ^
*(uint8_t *)((int64_t)*(uint8_t *)0x601162 + 0x601060);
*(uint8_t *)((int64_t)*(uint8_t *)0x601162 + 0x601060) =
*(uint8_t *)((int64_t)*(uint8_t *)0x601162 + 0x601060) ^
*(uint8_t *)((int64_t)*(uint8_t *)0x601161 + 0x601060);
*(uint8_t *)((int64_t)*(uint8_t *)0x601161 + 0x601060) =
*(uint8_t *)((int64_t)*(uint8_t *)0x601161 + 0x601060) ^
*(uint8_t *)((int64_t)*(uint8_t *)0x601162 + 0x601060);
return arg1 +
*(uint8_t *)
((int64_t)
(*(char *)((int64_t)*(uint8_t *)(0x601162 + 0x601060) +
*(char *)((int64_t)*(uint8_t *)(0x601161 + 0x601060) + (0x601060);
}
This function is not impossible to understand, but we can take another approach. We can set a breakpoint in:
iVar2 = fcn.004006e5(argc, (int64_t)arg2, placeholder_2, in_ECX);
And simply debug the binary
[0x0040064e]> db 0x004006db
[0x0040064e]> ood PCTF{fake_flag}
Process with PID 6619 started...
[0x7f2400442100]> dc
hit breakpoint at: 4006db
[0x004006db]> v!
Now the function is more clear. We can also decompile the function:
[0x004006e5]> pdg
undefined fcn.004006e5(uint32_t arg4)
{
undefined uVar1;
undefined4 in_RDI;
uVar1 = func_0x00400702(CONCAT44(in_RDI, arg4));
return uVar1;
}
The asm code of the function 0x00400702 is long and I will not post it, but
we can easily decompile it. Since this function is not define on radare2, we
need to define it. In visual mode seek to 0x00400702 and press df, and then pdg:
bool fcn.00400702(int64_t arg1)
{
char cVar1;
char *in_RAX;
int32_t iVar2;
int64_t iVar3;
char *pcVar4;
uint8_t uVar5;
int32_t iVar6;
int32_t iVar7;
bool bVar8;
iVar3 = -1;
// in_RAX = our argument
pcVar4 = in_RAX;
do {
if (iVar3 == 0) break;
iVar3 = iVar3 + -1;
cVar1 = *pcVar4;
pcVar4 = pcVar4 + 1;
} while (cVar1 != '\0');
// compute the length of the argument
iVar2 = ~(uint32_t)iVar3 - 1;
uVar5 = 0x50;
iVar6 = 0;
// apply this function to our flag
// (xor every character with the precedent one)
while (iVar6 < 0x539) {
iVar7 = 0;
while (iVar7 < iVar2) {
in_RAX[iVar7] = in_RAX[iVar7] ^ uVar5;
uVar5 = uVar5 ^ in_RAX[iVar7];
iVar7 = iVar7 + 1;
}
iVar6 = iVar6 + 1;
}
bVar8 = true;
iVar6 = 0;
while (iVar6 < iVar2) {
if (bVar8 == false) {
bVar8 = false;
} else {
bVar8 = in_RAX[iVar6] == *(char *)((int64_t)iVar6 + 0x4008eb);
}
iVar6 = iVar6 + 1;
}
return bVar8;
}
This code is very clear now. fcn.00400702 applies to our input argv[1] a function:
xor every character with the precedent one and repeat the operation 0x539 times.
At the end the function checks that the result is equal to the array in 0x4008eb.
We can dump the content of 0x4008eb:
[0x0040071a]> pxj 100@0x4008eb
[
72,95,54,53,53,37,20,44,29,1,3,45,12,111,53,97,126,52,10,68,36,44,74,70,25,89,
91,14,120,116,41,19,44,0,72,137,194,72,137,85,232,72,131,125,232,0,116,12,191,
209,9,64,0,232,219,250,255,255,235,10,191,218,9,64,0,232,207,250,255,255,144,
72,131,196,56,91,93,195,15,31,128,0,0,0,0,65,87,65,86,65,137,255,65,85,65,84,
76,141,37,190
]
Now we have one problem, we don’t know the length of the flag.
We can:
- Bruteforce it.
- Guess it.
- Doing some math.
We did it with bruteforce but we can guess that is long until the first null terminator
\x00 in the output of pxj 100@0x4008eb.
Now it’s time to compute the flag, I personally chose to use z3.
Exploit
from z3 import *
data = [
0x48, 0x5f, 0x36, 0x35, 0x35, 0x25, 0x14, 0x2c, 0x1d, 0x01, 0x03, 0x2d,
0x0c, 0x6f, 0x35, 0x61, 0x7e, 0x34, 0x0a, 0x44, 0x24, 0x2c, 0x4a, 0x46,
0x19, 0x59, 0x5b, 0x0e, 0x78, 0x74, 0x29, 0x13, 0x2c
]
flag = [BitVec(f'{i:2}', 8) for i in range(len(data))]
s = Solver()
# flag mut be a printable character
for f in flag:
s.add(f > 0x20, f <= 0x7f)
# just copy the code decompiled and rename some variables
xored = 0x50
indx = 0
while (indx < 0x539):
index = 0
while (index < len(flag)):
flag[index] = flag[index] ^ xored
xored = xored ^ flag[index]
index = index + 1
indx += 1
for f, d in zip(flag, data):
s.add(f == d)
print(s.check())
m = s.model()
model = sorted([(d, m[d]) for d in m], key = lambda x: str(x[0]))
for m in model:
print(chr(m[1].as_long()), end='')
Flag
pctf{ok_nothing_too_fancy_there!}
Fails
Me and @sen tried to solve the challenge using instructions counting with frida, but we failed since this challenge is not vulnerable to that type of attack.