glyphs

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.

elf x86_64 pie stripped_binary lambda_calculus de_bruijn_indices scott_encoding mt19937 binary_tree

checker_factorizationlambda_term_decodingscott_tree_decodingshape_hashingdifferential_analysisfixed_length_mutationcodebook_recovery

$ ls tags/ techniques/

elf x86_64 pie stripped_binary lambda_calculus de_bruijn_indices scott_encoding mt19937 binary_tree

checker_factorizationlambda_term_decodingscott_tree_decodingshape_hashingdifferential_analysisfixed_length_mutationcodebook_recovery

$ cat /etc/rate-limit

Rate limit reached (20 reads/hour per IP). Showing preview only — full content returns at the next hour roll-over.

glyphs — UIUCTF 2026

Description

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.

Analysis

Binary model

Initial triage identifies a stripped x86-64 PIE. Its large generated data and randomized-looking execution obscure a much smaller semantic model:

terms are variables, applications, and lambdas, with binder references convertible to De Bruijn form;
runtime values use Scott encodings;
MT19937 and the large reachability matrix choose a construction/evaluation schedule;
that schedule and the resulting tree topology depend on the input length, not its contents;
input contents affect the values stored at paths in that topology.

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.

Factor the checker before reducing it

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.

Decode the fixed target

...