Tenable ZDA: ARM Binary Reverse Engineering with Z3

Challenge

Challenge 4: Solve Me
===
This challenge binary asks for a password.  Reverse engineer the binary and
determine the password.  Write-up your approach.

Deliverables:
1. A write up describing how you approached the challenge and found the password
   (if found).
2. The password (if found).

Binary Reconnaissance

The target is a 32-bit ARM ELF binary:

$ file solve_me
solve_me: ELF 32-bit LSB shared object ARM, EABI5 version 1 (SYSV),
dynamically linked, interpreter /lib/ld-, BuildID[sha1]=7f974e81c0982ce5619ba301a9e65a4fcc2b7b77,
for GNU/Linux 3.2.0, stripped

Running it on an ARM instance:

$ ./solve_me
Enter the password: i have no idea
Wrong password

Static Analysis with Ghidra

Loading the binary into Ghidra, main() is straightforward — it calls a top-level routine at 0x0001333e responsible for reading and verifying the password:

The function at 0x000131e4 (referred to here as validate_password) contains the interesting logic:

The validation is structured as a single large if condition composed of 23 individual function calls, each returning a boolean. All 23 must return true for the password to be accepted. Examining one of these functions:

Each function takes the password buffer as input and computes a weighted sum: for every character in the password, its ordinal value is multiplied by a coefficient unique to that function. If the resulting sum equals a target constant, the function returns 1 (true).

Concretely, a single constraint looks like this (after cleaning up Ghidra's variable names):

pw22 * 0xba5 + pw0 * 0xb02 + pw1 * 0x2253 + pw2 * 0x1fa7 + pw3 * 0x1ab0
+ pw4 * -0x1ec2 + pw5 * -0x1957 + pw6 * 0x12ec + pw7 * -0x175e
+ pw8 * -0x1170 + pw9 * 0x250f + pw10 * 0x566 + pw11 * 0x153e
+ pw12 * 0xa2f + pw13 * -0x2567 + pw14 * -0x200f + pw15 * 0x13f8
+ pw16 * 0x17ec + pw17 * 0x1b43 + pw18 * 0x260b + pw19 * 0xd58
+ pw20 * -0x176b + pw21 * -0xbbd == 0x25ddae

With 23 such constraints over 23 password characters, this is a classic system of linear equations over integer variables — exactly the type of problem an SMT solver is built to handle.

SMT Solving with Z3

Z3 (Microsoft Research) is an SMT solver widely used in the reverse engineering and CTF communities. Beyond determining whether a formula is satisfiable, Z3 can produce concrete witness values for all symbolic variables — in this case, the exact character values that satisfy all 23 constraints simultaneously.

Each of the 23 constraint functions was extracted from the decompiled output, variable names were cleaned up, and the constraints were encoded into Z3's Python API (pip install z3-solver). The full solver script is available here: PoCs/c4_solver.py

Result

Running the solver:

$ python solver.py
T3nabl3_Z3r0_D4ys_52366

Z3 determines the system is satisfiable and produces a concrete password. Verifying against the target binary:

$ ./solve_me
Enter the password: T3nabl3_Z3r0_D4ys_52366
Correct password

Challenge file: solve_me (32-bit ARM ELF)