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.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);
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)
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 hex1 to hex6 with 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()
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()

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);
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

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)
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