glyphs

Platform: Uiuctf 2026 | Category: Reversing | Type: Challenge | Difficulty: Hard | OS: NA | Author: D3v0o0Nu11 | Date: 2026-08-09 | Status: Solved Techniques: checker_factorization, lambda_term_decoding, scott_tree_decoding, shape_hashing, differential_analysis, fixed_length_mutation, codebook_recovery

Summary

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.

Recon

Port scan

nmap -p- -sV -sC <TARGET> --min-rate 1000 -Pn

Enumeration highlights

• Event: UIUCTF 2026 | ID: 20260809_uiuc2026_glyphs
• Tags: pie, elf, x86_64, mt19937, stripped_binary, lambda_calculus, de_bruijn_indices, scott_encoding, binary_tree
• Indicators: stripped x86-64 PIE, standard Y combinator in the fixed checker, length-only randomized construction schedule, Scott-encoded binary tree target
• Source: 20260809_uiuc2026_glyphs.md

Foothold

Vulnerability / Misconfiguration

1. Checker_factorization
2. Lambda_term_decoding
3. Scott_tree_decoding
4. Shape_hashing
5. Differential_analysis

<command>

Exploitation

• See original writeup content for detailed exploitation.

Privilege Escalation

Enumeration

sudo -l
find / -perm -4000 2>/dev/null
getcap -r / 2>/dev/null
cat /etc/crontab
ps aux

Exploitation

1. N/A for challenge-type writeup; see exploitation above.
2. Flag obtained via challenge solve.

<command>

Flags

Key Takeaways / Lessons

• checker_factorization
• lambda_term_decoding
• scott_tree_decoding
• shape_hashing
• differential_analysis
• fixed_length_mutation
• codebook_recovery
• Tags: pie, elf, x86_64, mt19937, stripped_binary, lambda_calculus, de_bruijn_indices, scott_encoding, binary_tree

Original Writeup

<details><summary>Click to expand original content</summary>

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:

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

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.

Solution

1. Recover the input length from tree shape

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.

2. Map every tree path to its source cell

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.

3. Invert target values with equal-length pair probes

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.

4. Verify the entire structure and the native binary

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>'

Why the shorter route works

Three tempting approaches added complexity without helping the inversion:

• Treating the 61,719-node checker as monolithic hid the simple ((Y F) TARGET) split.
• A generic suspended-closure or GPE state-space search modeled far more than the fixed comparison required.
• Deleting one cell changes the length-dependent topology globally, so local peeling is invalid. Equal-length mutation is the correct differential because it preserves topology and path identities.

The intended simplification is to separate shape, controlled by length, from values, controlled by content, and invert only the one fixed target.

</details>

---

Auto-tracked: saved to WriteUps; run /xesor-revise to fold lessons into XESXor_Methodology.md.

signed by XESXOR