Drone Firmware

Overview

A drone authentication binary for the PIGEON-CLASS UAV (avian variant). It prompts for a 6-digit serial code and validates it against seven simultaneous arithmetic constraints. Satisfying all constraints causes the binary to XOR-decode and print the flag. Ideal for Z3, but the constraints are small enough to brute-force.

The binary's strings include // UNIT7 WAS HERE, weather_control_v2, and pigeon_sdk_wrapper. Flavour.

Step 1: Reverse the constraints

Load in Ghidra. The check_serial() function is straightforward:

int d[6];  // digit values 0-9
// Seven constraints:
d[0]+d[1]+d[2]+d[3]+d[4]+d[5] == 27
d[0]*d[5] == 15
d[1]*d[4] == 24
d[2]+d[3] == 9
d[2]*d[3] == 14
d[3]*d[4] == 12
d[0]+d[2] == 10

Step 2: Solve

Option A: Solve with Z3

from z3 import *

d = [Int(f'd{i}') for i in range(6)]
s = Solver()

# Bounds
for x in d:
    s.add(x >= 0, x <= 9)

# Constraints
s.add(sum(d) == 27)
s.add(d[0]*d[5] == 15)
s.add(d[1]*d[4] == 24)
s.add(d[2]+d[3] == 9)
s.add(d[2]*d[3] == 14)
s.add(d[3]*d[4] == 12)
s.add(d[0]+d[2] == 10)

if s.check() == sat:
    m = s.model()
    serial = ''.join(str(m[d[i]]) for i in range(6))
    print(f'Serial: {serial}')

Option B: Solve with brute-force

The search space is only 10^6:

for serial in range(1000000):
    s = f'{serial:06d}'
    d = [int(c) for c in s]
    if (d[0]+d[1]+d[2]+d[3]+d[4]+d[5] == 27 and
        d[0]*d[5] == 15 and d[1]*d[4] == 24 and
        d[2]+d[3] == 9 and d[2]*d[3] == 14 and
        d[3]*d[4] == 12 and d[0]+d[2] == 10):
        print(f'Serial: {s}')
        break

Both methods find: 347265

Verification: d=[3,4,7,2,6,5] - Sum: 3+4+7+2+6+5 = 27 ✓ - d[0]d[5]: 3×5 = 15 ✓ - d[1]d[4]: 4×6 = 24 ✓ - d[2]+d[3]: 7+2 = 9 ✓ - d[2]d[3]: 7×2 = 14 ✓ - d[3]d[4]: 2×6 = 12 ✓ - d[0]+d[2]: 3+7 = 10 ✓

Step 3: Get the flag

./drone_firmware.bin 347265
# AUTHENTICATED. Unit cleared for deployment.
# DEADROP{z3_solved_my_drone_auth_problem}

Or decode the XOR-encrypted flag directly:

enc_flag = bytes([0x1e,0x1f,0x1b,0x1e,0x08,0x15,0x0a,0x21,0x20,0x69,
                  0x05,0x29,0x35,0x36,0x2c,0x3f,0x3e,0x05,0x37,0x23,
                  0x05,0x3e,0x28,0x35,0x34,0x3f,0x05,0x3b,0x2f,0x2e,
                  0x32,0x05,0x2a,0x28,0x35,0x38,0x36,0x3f,0x37,0x27])
print(bytes(b ^ 0x5A for b in enc_flag).decode())

Flag: DEADROP{z3_solved_my_drone_auth_problem}

Key Takeaway

Arithmetic constraint systems over small integer domains are the canonical use case for Z3. What would take pages of manual algebra resolves in milliseconds with s.check(). The flag acknowledges this directly.