Dharma.exe

Description

A strange binary file has been sent to us anonymously.

File: dharma.

Methodology

This challenge is fairly simple: a first binary (dharma) drops a second one (2O3naSbh, but let’s call it stage2) using a well-known in-memory loading technique (please refer to this article for details).

As this is a CTF challenge, we’re looking for the shortest path to get the flag: let’s just patch the binary to make it drops the binary to a common file descriptor (e.g., stdout, stdin, stderr).

Because I’m lazy, I decided to apply the following patch:

--- dharma
+++ dharma_patched
 00001470: ffff bfff ffff ffe8 44fe ffff 8b45 fcc9  ........D....E..
 00001480: c3f3 0f1e fa55 4889 e548 83ec 2048 897d  .....UH..H.. H.}
 00001490: f848 8975 f048 8955 e889 4de4 488b 55e8  .H.u.H.U..M.H.U.
-000014a0: 488b 4df8 8b45 e448 89ce 89c7 e83f fdff  H.M..E.H.....?..
+000014a0: 488b 4df8 4831 c048 89ce 89c7 e83f fdff  H.M.H1.H.....?..
 000014b0: ff48 85c0 7934 488b 05a3 6d00 0048 89c1  .H..y4H...m..H..
 000014c0: ba1d 0000 00be 0100 0000 488d 3d5a 0b00  ..........H.=Z..
 000014d0: 00e8 fafd ffff 8b45 e489 c7e8 80fd ffff  .......E........

This allows us to replace the following instruction set:

mov eax, dword ptr [rbp - 0x1c]
mov rsi, rcx
mov edi, eax
call write

By the following one:

xor rax, rax
mov rsi, rcx
mov edi, eax
call write

Download the patched binary here.

We can now analyze the stage2 ELF using IDA, extract the validation checks (just analyze the init function), retrieve the init@stage2 function stack values with gdb (see the following commands to soft-patch the interrupts) and solve the equations with z3.

The following commands can be used in gdb to soft-patch the interrupts:

gdb -q ./dharma
start
c
set *(0x7ffff7fccd74) = 0x3e8bf90
set *(0x555555555893) = 0x3e8bf90
b * 0x7ffff7fcccda
c
# type a test input here
ni
# hit enter to repeat nexti command multiple times and trace the checking process

Based on our gdb tracing, we’re now able to implement our equalitions in a SAT solver such as z3:

#!/usr/bin/env python3
import hashlib

from z3 import *

DEBUG = False

s = Solver()

inp = BitVec('inp', 64)

# make sure that the input is not negative and finish with 0x31337 in hexadecimal
s.add(And(inp >= 0))

# equation from stage2
s.add((0xc80 * (inp ^ 0xc80 & 0x42) / 0x68625361) - 0x6e334f32 == 0)
s.add(inp & 0xffff == 0xfb4c)

while s.check() == sat:  # while there's solution
    model = s.model()  # get solution
    valid_inp = model[inp].as_long()
    s.add(inp != valid_inp)  # make sure that we're not getting the same input value
    flag_candidate = hashlib.sha256(str(valid_inp).encode()).hexdigest()  # the flag corresponds to the sha256 hash digest of our input
    if DEBUG: print(f'{valid_inp} => {flag_candidate}')
    if flag_candidate.endswith('04440d69'):  # we know that the final flag ends with 04440d69 according to the challenge description
        print(f'Flag: {flag_candidate}')
        break

Flag

The final flag is: b2d4837830f4853656e993e4561670d0e461471acbb0e2f7183b514b04440d69

Happy Hacking!

Creased