Backdoor 2017 No Calm 350
Backdoor 2017 no.clam - 350
h3rcul35 and starlord were having a heated conversation and to c00l down the furious starlord, h3rcul35 gave him a binary and said “The binary takes each ‘character’ byte of the flag as argument. Given this info, grab the flag. I hope you dont get angry :P”. Show h3rcul35 that you stayed c00l by finding the flag.
Challenge file
file challenge
challenge: ELF 64-bit LSB executable, x86-64, version 1 (SYSV), dynamically linked, interpreter /lib64/ld-linux-x86-64.so.2,
for GNU/Linux 2.6.32, BuildID[sha1]=19a85aefbf9989c28ef64ae7a1c164882a0fa9af, not stripped
running the program tells us that there should be some arguments
./challenge
Usage ./challenge <each byte of flag seperated by spaces>
let’s examine the binary with radare2
| | 0x004007ea mov dword [local_44h], edi
| | 0x004007ed mov qword [local_50h], rsi
| | 0x004007f1 mov rax, qword fs:[0x28]
| | 0x004007fa mov qword [local_8h], rax
| | 0x004007fe xor eax, eax
| | 0x00400800 cmp dword [local_44h], 0x1f <---- Check for no.of arg
| | ,=< 0x00400804 je 0x40081f
| | | 0x00400806 mov edi, str.Usage_._challenge__each_byte
| | | 0x0040080b mov eax, 0
| | | 0x00400810 call sym.imp.printf
| | | 0x00400815 mov edi, 1
| | | 0x0040081a call sym.imp.exit
| | `-> 0x0040081f mov dword [local_34h], 0
| | .-> 0x00400826 mov eax, dword [local_44h]
here we can see that , no of argument is checked with 0x1f ie we have to give 30 characters
These arguments are moved to the stack and some checks are performed
| | |
|.----------------------------------. .--------------------------------------------.
|| 0x400831 ;[gh];loop to mov input| | 0x40085e ;[gf] |
|| mov eax, dword [local_34h] | | ; JMP XREF from 0x0040082f (sym.main) |
|| cdqe | | movzx eax, byte [local_30h] |
|| add rax, 1 | | movsx edx, al |
|| lea rdx, [rax*8] | | movzx eax, byte [local_2fh] |
|| mov rax, qword [local_50h] | | movsx eax, al |
|| ; '(' | | add edx, eax |
|| add rax, rdx | | movzx eax, byte [local_2eh] |
|| mov rax, qword [rax] | | movsx eax, al |
|| movzx edx, byte [rax] | | sub edx, eax |
|| mov eax, dword [local_34h] | | mov eax, edx |
|| cdqe | | ; 'Q' |
|| mov byte [rbp + rax - 0x30], dl | | ; 'Q' |
|| add dword [local_34h], 1 | | ; 81 |
|| jmp 0x400826;[gg] | | cmp eax, 0x51 <-- the result is compared
|`----------------------------------' | jne 0x400d66;[gi] |
| v `--------------------------------------------'
| | f t
| | | |
`----' | |
| '-.
.--------------------------------------' |
| |
.------------------------------. .--------------------------------------------.
| 0x400882 ;[gk] | | 0x400d66 ;[gi] |
| movzx eax, byte [local_30h] | | ; JMP XREF from 0x0040087c (sym.main) |
| movsx edx, al | | call sym.fail__;[gBs] |
| movzx eax, byte [local_2fh] | `--------------------------------------------'
| movsx eax, al | v
| sub edx, eax | |
| movzx eax, byte [local_2eh] | |
| movsx eax, al | <-- Next comparision
| add eax, edx | |
| ; '5' | |
| ; '5' | |
| ; 53 | |
the first three constrains are
arg[0]+arg[1]-arg[2]=0x51
arg[0]-arg[1]+arg[2]=0x35
arg[1]-arg[0]+arg[2]=0x57
From these constrains we can get the first three characters
We can see a pattern here they take 3 arguments checks the constrains then takes next three and check is performed again , solving these manually is not an option
extracting the comparisons
[0x004007e3]> /c cmp eax
0x004006fd # 3: cmp eax, 0xe
0x00400771 # 5: cmp eax, 0x2018e9
0x0040082c # 3: cmp eax, dword [rbp - 0x34]
0x00400879 # 3: cmp eax, 0x51
0x0040089b # 3: cmp eax, 0x35
0x004008bd # 3: cmp eax, 0x57
0x004008e1 # 3: cmp eax, 0x5a
0x00400903 # 5: cmp eax, 0x9c
0x00400927 # 3: cmp eax, 0x42
0x0040094b # 3: cmp eax, 0x62
0x0040096d # 5: cmp eax, 0x8c
0x00400991 # 3: cmp eax, 0x5c
0x004009b5 # 3: cmp eax, 0x26
0x004009d7 # 5: cmp eax, 0xaa
0x004009fb # 3: cmp eax, 0x3c
0x00400a1f # 3: cmp eax, 0x1d
0x00400a41 # 5: cmp eax, 0xa1
0x00400a65 # 3: cmp eax, 0x45
0x00400a89 # 5: cmp eax, 0xa3
0x00400aad # 3: cmp eax, 0x1b
0x00400acf # 3: cmp eax, 0x45
0x00400af3 # 5: cmp eax, 0x93
0x00400b17 # 3: cmp eax, 0x2b
0x00400b39 # 3: cmp eax, 0x3b
0x00400b5d # 5: cmp eax, 0x92
0x00400b81 # 3: cmp eax, 0x56
0x00400ba3 # 3: cmp eax, 0x2c
0x00400bc7 # 3: cmp eax, 0x43
0x00400be9 # 3: cmp eax, 0x59
0x00400c0b # 3: cmp eax, 0x4b
0x00400c2f # 3: cmp eax, 0x75
0x00400c4d # 3: cmp eax, 0x7d
0x00400c6b # 3: cmp eax, 0x7d
0x00400d2d # 5: cmp eax, 0xfffa99e8
now it’s time to write script , using z3 we can solve these constrains to obtain the flag
from z3 import *
byte = [ 0x51 , 0x35 , 0x57 , 0x5a , 0x9c , 0x42 , 0x62 , 0x8c , 0x5c , 0x26 , 0xaa , 0x3c , 0x1d , 0xa1 , 0x45 , 0xa3 , 0x1b , 0x45 , 0x93 , 0x2b , 0x3b , 0x92 , 0x56 , 0x2c , 0x43 , 0x59 , 0x4b , 0x75 , 0x7d , 0x7d ]
flag = ''
for i in range(0,len(byte),3):
x = Int('x')
y = Int('y')
z = Int('z')
s = Solver()
s.add(x+y-z==byte[i])
s.add(x-y+z==byte[i+1])
s.add(y-x+z==byte[i+2])
s.check()
m = s.model()
flag += chr(int(str(m[x])))
flag += chr(int(str(m[y])))
flag += chr(int(str(m[z])))
print(flag)