$ cat writeup.md…
$ cat writeup.md…
UIUCTF 2026
Task: A stripped x86-64 PIE serializes input into lambda-calculus and Scott-encoded structures, then compares it with a fixed target. Solution: Factor the checker, match the length-only tree shape, and recover shifted input pairs with equal-length differential probes.
Strange glyphs inscribed on the wall rearrange themselves chaotically. Will they respond if you call out to them?
The program accepts one command-line argument and prints either a rejection or an acceptance word. The goal is to recover an argument in the public uiuctf{...} format that reaches the accepting result.
Initial triage identifies a stripped x86-64 PIE. Its large generated data and randomized-looking execution obscure a much smaller semantic model:
The last property is decisive. It means content must be changed without changing length. Deleting a cell changes the schedule and globally rewrites the tree, so deletion-based peeling is not a valid local inverse.
The constructed source graph contains a fixed checker at stable heap offsets:
| Heap offset | Meaning |
|---|---|
0x480bb20 | standard call-by-name Y combinator |
0x480bb40 | generic recursive comparison function F |
0x480bba0 | fixed encoded TARGET |
0x480bbe0 | App(App(Y, F), TARGET) |
Thus the 61,719-node checker is not one bespoke transducer. It is a generic recursive equality routine specialized with one constant:
CHECKER = ((Y F) TARGET)
The surrounding final expression applies this predicate to the serialized input and then to the rejection and acceptance results. inspect_checker_highlevel.py and the heap AST helpers reproduce the factorization and administrative reductions.
TARGET is a direct Scott-encoded binary tree. Ignoring unused fields, its constructors are:
Empty = λk. k TRUE _ _ _ Node(value, left, right) = λk. k FALSE value left right
Each node value is itself a Scott stream of ternary digits:
Nil = λk. k TRUE _ _ Cons(digit, tail) = λk. k FALSE digit tail digit ∈ {Sel3(0), Sel3(1), Sel3(2)}
Digits are least-significant first. The glyph decoder performs ternary successor, so decode_checker_target.py decodes target streams and uses the inverse successor codebook when a primitive value is available.
A compact version of the decoder is:
def decode_stream(term): digits = [] while True: tag, digit, tail = tuple3(whnf_if_needed(term)) if selector(tag) == TRUE: return "".join(digits) assert selector(tag) == FALSE arity, choice = selector(digit) assert arity == 3 digits.append(str(choice)) term = tail def decode_tree(term): tag, value, left, right = tuple4(whnf_if_needed(term)) if selector(tag) == TRUE: return None assert selector(tag) == FALSE return (decode_stream(value), decode_tree(left), decode_tree(right))
The decoded constant is a full binary tree with exactly 141 nodes and 142 empty children. This is the object the serialized input must equal.
For each candidate length, serialize an equal-content control and discard all values. Canonicalize only Node/Empty topology:
def topology(node): if node is None: return None _value, left, right = node return (topology(left), topology(right)) def shape_hash(node): return blake2b(repr(topology(node)).encode(), digest_size=16).hexdigest()
The scan is implemented by target_specific_inverse.py:
python3 target_specific_inverse.py --scan-min 3 --scan-max 73 --scan-even
Odd-length controls were also measured through the input limit and did not match. The relevant even-length log ends with:
length=146 cells=73 nodes=141 shape=008ae7d4efc2d0a6d137ee80d58e040b target_shape=true TARGET_LENGTH_MATCH 146 cells 73
Therefore the required serialization uses 146 bytes, or 73 physical two-byte cells. matched_length_146.json records the matching control and hash.
At length 146, topology is fixed. Build one control containing 73 distinct labels while keeping the other byte of every physical cell equal. Then build seven controls. In control b, replace the selected byte of every one-based cell index whose bit b is set, while preserving total length.
For each target path, compare its value with the seven controls:
mask = sum( 1 << bit for bit in range(7) if bit_probe[bit][path] != baseline[path] ) source_cell = mask - 1
The seven-bit signature maps all 141 node paths. target_ordered_cells.json records mapped_paths: 141 and unmapped_paths: 0.
One subtlety is that the meaningful complete-cell values are shifted by one byte relative to the physical input grid. Mutating byte two of physical cell i changes the same path set as mutating byte one of physical cell i+1. Therefore shifted pair i is:
input[2*i + 1 : 2*i + 3]
The 72 pair ranges are consequently [1:3], [3:5], ..., [143:145]. The two outer boundary bytes are fixed by the public uiuctf{...} wrapper.
Changing one pair at a time would require thousands of slow native runs. Instead, put many independent printable pairs into path-bearing slots of one 146-byte control. Because the slots have disjoint path signatures, one run yields many codebook rows.
The essential logic in recover_ordered_cells.py is:
for batch in batches(all_printable_pairs): probe = fixed_length_input(batch) # always 146 bytes values = serialize_and_decode(probe) # path -> LSD-first trits for slot, literal_pair in batch.items(): observed = Counter(values[p] for p in paths_for_slot[slot]) assert len(observed) == 1 inverse_codebook[next(iter(observed))] = literal_pair
A fixed validation pair is placed in two slots in every batch. Its value remains identical, proving that the decoded pair value is position-independent. target_pair_codebook_printable.json contains the printable pair codebook, while target_path_dependencies.json records the controlled path dependencies.
Looking up the target values fixes 59 of the 72 shifted pair slots when combined with the public wrapper. Thirteen payload-relevant slots have no paths and are therefore unconstrained by this tree comparison. The surrounding recovered text forms an unambiguous mixed-case/leetspeak sentence, so those slots can be completed without guessing the constrained bytes.
Do not trust readability alone. Re-serialize the completed candidate, decode all paths, and compare the complete tree against TARGET before invoking the native binary:
python3 recover_ordered_cells.py --check-candidate '<CANDIDATE>'
The exact-casing candidate produces:
NATIVE 'good' TARGET_TREE_EQUAL True mismatches 0 MISMATCHED_SHIFTED_INDICES []
recovered_flag_verification.json independently records 141 actual nodes, 141 target nodes, zero mismatches, and native_good: true. Direct execution under Docker/qemu also prints good:
docker run --rm --platform linux/amd64 \ -v "$PWD:/w" -w /w glyphs-tools \ bash -c 'qemu-x86_64 /w/glyphs "$1"' verify '<CANDIDATE>'
Three tempting approaches added complexity without helping the inversion:
((Y F) TARGET) split.The intended simplification is to separate shape, controlled by length, from values, controlled by content, and invert only the one fixed target.
$ cat /etc/motd
Liked this one?
Pro unlocks every writeup, every flag, and API access. $9/mo.
$ cat pricing.md$ grep --similar