Hexagon
[GoogleCTF, 2021]
Introduction
This is a writeup of the Hexagon challenge of the GoogleCTF 2021
Challenge Description
slaps DSP This baby can fit so many instructions in its execution slots!
Attachment: file challenge
Solution
Inpecting the challenge file, we can see that it is a Qualcom Hexagon binary:
$ file challenge
challenge: ELF 32-bit LSB executable, QUALCOMM DSP6, version 1 (SYSV), statically linked, for GNU/Linux 3.0.0, with debug_info, not stripped
Luckily our favorite reversing tool rizin supports disassembly of such files. We can see that it contains
the following functions:
entry0 ();
int main (int argc, char **argv, char **envp);
loc.exit ();
loc.welcome ();
loc.read_flag ();
loc.print_status ();
loc.check_flag ();
loc.hex1 ();
loc.hex2 ();
loc.hex3 ();
loc.hex4 ();
loc.hex5 ();
loc.hex6 ();
Since this is a reversing challenge, we can already guess that this binary expects a flag as input and checks if it is correct.
Before we dive into the main function, there is something supspicious going on in the entry0 function:
entry0 ();
0x00020200 allocframe (0x0)
0x00020204 call loc.welcome
0x00020208 R0 = 4919
0x0002020c immext(#0x30500)
0x00020210 R1 = loc.target
0x00020214 loop0 (0x4, 0x50)
0x00020218 R2 = memb (R1 + 0)
0x0002021c R2 = xor (R0, R2)
0x00020220 R0 = add (R0, 1)
0x00020224 memb (R1 ++ 1) = R4
After calling the welcome function, which just prints Hi!, a loop instruction
loops over 0x50 bytes of memory, xoring it with R0 and writing it back.
R0 is initialized with 4919 and incremented after every byte. We extracted
the data from the binary and transformed it in python:
blob = unhexlify("bf96aa4611236bb2735e5c5446544242"
+"54584e5253534d1e60072e2223652f34"
+"686e091f0a361617082c7573233d3325"
+"3d790203047d372c40180d1616450f09"
+"181c1e4566391c16501015121d1b577dff")
blob = bytes([x ^ ((48-8) + i) for i,x in enumerate(blob)])
Where blob then is
b"\x97\xbf\x80m=\x0eE\x9dCongratulations! Flag is 'CTF{XXX}' where XXX is your input.\nTry again!\n\x87"
So the first thing the binary does is to decrypt some strings and other data. Now to the rest of the binary. Inspecting the main function shows that it indeed checks the flag:
int main (int argc, char **argv, char **envp);
0x00020228 call loc.read_flag
0x0002022c call loc.check_flag
0x00020230 call loc.print_status
0x00020234 call loc.exit
0x00020238 dealloc_return
First read_flag reads the flag into the global variable loc.flag via some sort of syscall
that is invoked with the trap0 instruction:
loc.read_flag ();
0x0002027c R6 = 63
0x00020280 R0 = 0
0x00020284 immext(#0x30500)
0x00020288 R1 = loc.flag
0x0002028c R2 = 8
0x00020290 trap0 (0x1)
0x00020294 jumpr R31
; CALL XREF from main @ 0x20230
Then check_flag does some checks and in the end returns the result in R0:
loc.check_flag ();
0x000202d0 allocframe (0x0)
...
0x00020388 R0 = P
0x0002038c dealloc_return
And print_status takes the result and prints the congratulations from before
if R0 is not 0:
loc.print_status ();
0x00020298 R0 = and (R0, 255)
0x0002029c if !P0.new jump:t 0x202b4
0x000202a0 P0 = cmp.eq (R0, 255)
0x000202a4 immext(#0x30500)
0x000202a8 R1 = loc.good
0x000202ac R2 = 61
0x000202b0 jump 0x202c0
0x000202b4 immext(#0x30540)
0x000202b8 R1 = loc.bad
0x000202bc R2 = 11
0x000202c0 R6 = 64
0x000202c4 R0 = 1
0x000202c8 trap0 (0x1)
0x000202cc jumpr R31
So what we have to analyze is how to get the check_flag function to return "True".
It turns out check flag does the following things:
- Read the flag into R3:R2
- Call
hex1tohex6with mostly static parameters - Compare the result of its calculations in R3:R2 with values loaded from the decrypted part of memory
So what we have to do is let the calculations result in the values we calculate earlier.
To do so we used z3, by reimplemeinting the code in python and letting z3 create a formula that
can be solved for the flag:
flag0 = BitVec('flag0', 32)
flag1 = BitVec('flag1', 32)
def hex1(r0):
r5 = const(173879092)
r0 += r5
r0 = i32(r0)
r0 = ~(r0)
return r0
def hex2(r0):
r0 = ~(r0)
r5 = const(1210484339)
r0 ^= r5
return r0
def hex3(r0):
return i32((r0 ^ const(1519522183)) + const(-373614660))
def hex4(r0):
return ~(r0) ^ const(-686802991)
def hex5(r0):
return i32(~(r0) + const(270515404))
def hex6(r0):
return const(-1962843199) ^ const(-288476533) ^ r0
def check_flag(flag0, flag1):
r3, r2 = flag0, flag1
r0 = const(1869029418)
r0, r2 = r2,r0
r0 = hex1(r0)
r2 ^= r0
r0 = const(1701603183)
r0,r3 = r3,r0
r0 = hex2(r0)
r3 ^= r0
r0 = const(1852400160)
r0 = hex3(r0)
r0 = xor (r0, r3)
r2, r3 = r3, xor (r2, r0)
r0 = const(1747804522)
r0 = hex4(r0)
r0 = xor (r0, r3)
r2, r3 = r3, xor (r2, r0)
r0 = const(1734441061)
r0 = hex5(r0)
r0 = xor (r0, r3)
r2, r3 = r3, xor (r2, r0)
r0 = const(706768495)
r0 = hex6(r0)
r0 = xor (r0, r3)
r2, r3 = r3, xor (r2, r0)
r5, r4 = good0, good1
return And(r5 == r3, r4 == r2)
It did take some time to figure all of this out, but we finally succeded to obtain the flag.
Flag
ctf{IDigVLIW}
Files
solve.py
from z3 import *
from pwn import *
from binascii import *
r1 = [1, 6, 15, 28, 45, 66]
branch = [None for _ in range(6)]
def tstbit(i, idx):
return i & (1 << idx) != 0
branch[0] = tstbit(r1[0], 0x6)
branch[1] = tstbit(r1[1], 0x3)
branch[2] = tstbit(r1[2], 0x8)
branch[3] = tstbit(r1[3], 0x0)
branch[4] = tstbit(r1[4], 0x0)
branch[5] = tstbit(r1[5], 0x3)
print(branch)
def const(val):
return BitVecVal(val, 32)
def i32(v):
return (v + 2**32) % 2**32
flag0 = BitVec('flag0', 32)
flag1 = BitVec('flag1', 32)
blob = unhexlify("bf96aa4611236bb2735e5c5446544242"
+"54584e5253534d1e60072e2223652f34"
+"686e091f0a361617082c7573233d3325"
+"3d790203047d372c40180d1616450f09"
+"181c1e4566391c16501015121d1b577dff")
blob = bytes([x ^ ((48-8) + i) for i,x in enumerate(blob)])
start3 = hexlify(blob[:4]), hexlify(blob[4:8])
goods = start3
good = list(const(u32(unhexlify(x))) for x in goods)[::-1]
good0, good1 = good
def check(expr):
s = Solver()
s.add(expr)
if s.check() == sat:
print(s.model())
return s.check() == sat
def hex1(r0):
r5 = const(173879092)
r0 += r5
r0 = i32(r0)
r0 = ~(r0)
return r0
def hex2(r0):
r0 = ~(r0)
r5 = const(1210484339)
r0 ^= r5
return r0
def hex3(r0):
return i32((r0 ^ const(1519522183)) + const(-373614660))
def hex4(r0):
return ~(r0) ^ const(-686802991)
def hex5(r0):
return i32(~(r0) + const(270515404))
def hex6(r0):
return const(-1962843199) ^ const(-288476533) ^ r0
def xor(a,b):
return a ^ b
res = check_flag(flag0, flag1)
def mustbeascii(bitvec):
cond = True
for i in range(4):
char = Extract(8*(i+1)-1, 8*i, flag0)
cond = cond and (0x20 <= char) and (char <= 0x7e)
return cond
def convflag(m):
flagres = m[flag0], m[flag1]
flag = [p32(x.as_long()) for x in flagres]
return b''.join(flag)
s = Solver()
s.add(res)
while s.check() == sat:
m = s.model()
resbytes = convflag(m)
print(m, resbytes)
s.add(Or(flag0 != m[flag0], flag1 != m[flag1]))
disasm.txt
entry0 ();
0x00020200 allocframe (0x0)
0x00020204 call loc.welcome
0x00020208 R0 = 4919
0x0002020c immext(#0x30500)
0x00020210 R1 = loc.target
0x00020214 loop0 (0x4, 0x50)
0x00020218 R2 = memb (R1 + 0)
0x0002021c R2 = xor (R0, R2)
0x00020220 R0 = add (R0, 1)
0x00020224 memb (R1 ++ 1) = R4
int main (int argc, char **argv, char **envp);
0x00020228 call loc.read_flag
0x0002022c call loc.check_flag
0x00020230 call loc.print_status
0x00020234 call loc.exit
0x00020238 dealloc_return
; CALL XREF from main @ 0x20234
loc.exit ();
0x0002023c R6 = 94
0x00020240 R0 = 0
0x00020244 trap0 (0x1)
0x00020248 jumpr R31
; CALL XREF from entry0 @ 0x20204
loc.welcome ();
0x0002024c allocframe (0x0)
0x00020250 R7 = memw (R30 + 4)
0x00020254 R6 = 64
0x00020258 R0 = 1
0x0002025c immext(#0x30500)
0x00020260 R1 = loc.hello
0x00020264 R2 = 4
0x00020268 trap0 (0x1)
0x0002026c R0 = xor (R7, R0)
0x00020270 immext(#0x20200)
0x00020274 R0 = main ; memw (Sp + 0x4) = R0
0x00020278 dealloc_return
; CALL XREF from main @ 0x20228
loc.read_flag ();
0x0002027c R6 = 63
0x00020280 R0 = 0
0x00020284 immext(#0x30500)
0x00020288 R1 = loc.flag
0x0002028c R2 = 8
0x00020290 trap0 (0x1)
0x00020294 jumpr R31
; CALL XREF from main @ 0x20230
loc.print_status ();
0x00020298 R0 = and (R0, 255)
0x0002029c if !P0.new jump:t 0x202b4
0x000202a0 P0 = cmp.eq (R0, 255)
0x000202a4 immext(#0x30500)
0x000202a8 R1 = loc.good
0x000202ac R2 = 61
0x000202b0 jump 0x202c0
; CODE XREF from loc.print_status @ 0x2029c
0x000202b4 immext(#0x30540)
0x000202b8 R1 = loc.bad
0x000202bc R2 = 11
; CODE XREF from loc.print_status @ 0x202b0
0x000202c0 R6 = 64
0x000202c4 R0 = 1
0x000202c8 trap0 (0x1)
0x000202cc jumpr R31
; CALL XREF from main @ 0x2022c
loc.check_flag ();
0x000202d0 allocframe (0x0)
0x000202d4 immext(#0x30500)
0x000202d8 R3:R2 = memd (gp + 0x68)
0x000202dc immext(#0x6f672000)
0x000202e0 R0 = 1869029418
0x000202e4 R0 = R2 ; R2 = R0
0x000202e8 R1 = 1
0x000202ec call loc.hex1
0x000202f0 R2 = xor (R2, R0)
0x000202f4 immext(#0x656c6740)
0x000202f8 R0 = 1701603183
0x000202fc R0 = R3 ; R3 = R0
0x00020300 R1 = 6
0x00020304 call loc.hex2
0x00020308 R3 = xor (R3, R0)
0x0002030c immext(#0x6e696200)
0x00020310 R0 = 1852400160
0x00020314 R1 = 15
0x00020318 call loc.hex3
0x0002031c R0 = xor (R0, R3)
0x00020320 R2 = R3
0x00020324 R3 = xor (R2, R0)
0x00020328 immext(#0x682d6140)
0x0002032c R0 = 1747804522
0x00020330 R1 = 28
0x00020334 call loc.hex4
0x00020338 R0 = xor (R0, R3)
0x0002033c R2 = R3
0x00020340 R3 = xor (R2, R0)
0x00020344 immext(#0x67617840)
0x00020348 R0 = 1734441061
0x0002034c R1 = 45
0x00020350 call loc.hex5
0x00020354 R0 = xor (R0, R3)
0x00020358 R2 = R3
0x0002035c R3 = xor (R2, R0)
0x00020360 immext(#0x2a206e40)
0x00020364 R0 = 706768495
0x00020368 R1 = 66
0x0002036c call loc.hex6
0x00020370 R0 = xor (R0, R3)
0x00020374 R2 = R3
0x00020378 R3 = xor (R2, R0)
0x0002037c immext(#0x30500)
0x00020380 R5:R4 = memd (gp + 0xa8)
0x00020384 P0 = cmp.eq (R5:R4, R3:R2)
0x00020388 R0 = P
0x0002038c dealloc_return
; CALL XREF from loc.check_flag @ 0x202ec
loc.hex1 ();
0x00020390 P0 = tstbit (R1, 0x6)
0x00020394 if (P0.new) jump:t 0x203b4
0x00020398 immext(#0xa5d2f00)
0x0002039c R5 = 173879092
0x000203a0 R0 = add (R0, R5)
0x000203a4 jump 0x203a8
; CODE XREF from loc.hex1 @ 0x203a4
0x000203a8 R0 = sub (-1, R0)
0x000203ac jump 0x203c8
0x000203b0 immext(#0x7a024200)
; CODE XREF from loc.hex1 @ 0x20394
0x000203b4 R5 = 2046968324
0x000203b8 R0 = add (R0, R5)
0x000203bc jump 0x203c0
; CODE XREF from loc.hex1 @ 0x203bc
0x000203c0 R0 = sub (-1, R0)
0x000203c4 jump 0x203c8
; CODE XREFS from loc.hex1 @ 0x203ac, 0x203c4
0x000203c8 jumpr R31
; CALL XREF from loc.check_flag @ 0x20304
loc.hex2 ();
0x000203cc P0 = tstbit (R1, 0x3)
0x000203d0 if (P0.new) jump:t 0x203f0
0x000203d4 R0 = sub (-1, R0)
0x000203d8 jump 0x203dc
; CODE XREF from loc.hex2 @ 0x203d8
0x000203dc immext(#0x48268640)
0x000203e0 R5 = 1210484339
0x000203e4 R0 = xor (R0, R5)
0x000203e8 jump 0x2040c
0x000203ec immext(#0xe6f45900)
; CODE XREF from loc.hex2 @ 0x203d0
0x000203f0 R5 = -420194037
0x000203f4 R0 = xor (R0, R5)
0x000203f8 jump 0x203fc
; CODE XREF from loc.hex2 @ 0x203f8
0x000203fc immext(#0x5487ce00)
0x00020400 R5 = 1418186270
0x00020404 R0 = add (R0, R5)
0x00020408 jump 0x2040c
; CODE XREFS from loc.hex2 @ 0x203e8, 0x20408
0x0002040c jumpr R31
; CALL XREF from loc.check_flag @ 0x20318
loc.hex3 ();
0x00020410 P0 = tstbit (R1, 0x8)
0x00020414 if (P0.new) jump:t 0x2043c
0x00020418 immext(#0x5a921180)
0x0002041c R5 = 1519522183
0x00020420 R0 = xor (R0, R5)
0x00020424 jump 0x20428
; CODE XREF from loc.hex3 @ 0x20424
0x00020428 immext(#0xe9bb1780)
0x0002042c R5 = -373614660
0x00020430 R0 = add (R0, R5)
0x00020434 jump 0x20450
0x00020438 R0 = sub (-1, R0)
; CODE XREF from loc.hex3 @ 0x20414
0x0002043c jump 0x20440
; CODE XREF from loc.hex3 @ 0x2043c
0x00020440 immext(#0x85776e80)
0x00020444 R5 = -2055770470
0x00020448 R0 = add (R0, R5)
0x0002044c jump 0x20450
; CODE XREFS from loc.hex3 @ 0x20434, 0x2044c
0x00020450 jumpr R31
; CALL XREF from loc.check_flag @ 0x20334
loc.hex4 ();
0x00020454 p0 = tstbit (R1, #0) ; if (p0.new) jump:t 0x20470
0x00020458 R0 = sub (-1, R0)
0x0002045c jump 0x20460
; CODE XREF from loc.hex4 @ 0x2045c
0x00020460 immext(#0xd71037c0)
0x00020464 R5 = -686802991
0x00020468 R0 = xor (R0, R5)
0x0002046c jump 0x20480
; CODE XREF from loc.hex4 @ 0x20454
0x00020470 R0 = sub (-1, R0)
0x00020474 jump 0x20478
; CODE XREF from loc.hex4 @ 0x20474
0x00020478 R0 = sub (-1, R0)
0x0002047c jump 0x20480
; CODE XREFS from loc.hex4 @ 0x2046c, 0x2047c
0x00020480 jumpr R31
; CALL XREF from loc.check_flag @ 0x20350
loc.hex5 ();
0x00020484 p0 = tstbit (R1, #0) ; if (p0.new) jump:t 0x204a0
0x00020488 R0 = sub (-1, R0)
0x0002048c jump 0x20490
; CODE XREF from loc.hex5 @ 0x2048c
0x00020490 immext(#0x55485800)
0x00020494 R5 = 1430804514
0x00020498 R0 = add (R0, R5)
0x0002049c jump 0x204b8
; CODE XREF from loc.hex5 @ 0x20484
0x000204a0 R0 = sub (-1, R0)
0x000204a4 jump 0x204a8
; CODE XREF from loc.hex5 @ 0x204a4
0x000204a8 immext(#0x101fbcc0)
0x000204ac R5 = 270515404
0x000204b0 R0 = add (R0, R5)
0x000204b4 jump 0x204b8
; CODE XREFS from loc.hex5 @ 0x2049c, 0x204b4
0x000204b8 jumpr R31
; CALL XREF from loc.check_flag @ 0x2036c
loc.hex6 ();
0x000204bc P0 = tstbit (R1, 0x3)
0x000204c0 if (P0.new) jump:t 0x204e8
0x000204c4 immext(#0x8b0163c0)
0x000204c8 R5 = -1962843199
0x000204cc R0 = xor (R0, R5)
0x000204d0 jump 0x204d4
; CODE XREF from loc.hex6 @ 0x204d0
0x000204d4 immext(#0xeece3280)
0x000204d8 R5 = -288476533
0x000204dc R0 = xor (R0, R5)
0x000204e0 jump 0x20504
0x000204e4 immext(#0x49a3e800)
; CODE XREF from loc.hex6 @ 0x204c0
0x000204e8 R5 = 1235478542
0x000204ec R0 = xor (R0, R5)
0x000204f0 jump 0x204f4
; CODE XREF from loc.hex6 @ 0x204f0
0x000204f4 immext(#0x6288e180)
0x000204f8 R5 = 1653137829
0x000204fc R0 = xor (R0, R5)
0x00020500 jump 0x20504
; CODE XREFS from loc.hex6 @ 0x204e0, 0x20500
0x00020504 jumpr R31