Skip to content

Phase 7: Trusted FFI & External Code Boundary Fuzzing #30

@quinn-dougherty

Description

@quinn-dougherty

Phase 7: Trusted FFI & External Code Boundary Fuzzing

Target the boundaries where verified Lean logic hands off to unverified external code (C++ primitives, GMP, native_decide, FFI).

Status: NOT STARTED

Ref: docs/design-plan.md Phase 7


Category 8: External Code Trust Boundary Exploits

Generate prefixes that stress the boundaries where verified logic meets unverified implementation:

  • Kernel Nat C++ primitivesNat.add, Nat.sub, Nat.mul, Nat.div, Nat.mod, Nat.ble, Nat.beq, bitwise ops (GMP-backed bignum arithmetic)
  • native_decide compiled code path — Compilation of Lean to native code for decidable propositions
  • String/ByteArray/FloatArray primitives — Other types with C++ backing implementations
  • Any future kernel built-in — Attack surface grows as Lean adds more optimized primitives

Category 9: Specification-Execution Gap Exploits

Mechanisms that allow the executed behavior to differ from specified (type-checked) behavior:

  • @[implemented_by] — Override a function's implementation; explore indirect effects on kernel reasoning
  • @[extern] — FFI declarations where the type signature may not match the external implementation
  • Compiler plugins / custom elaborators — Code that runs at elaboration time and produces kernel terms
  • Decidable instance mismatches — A Decidable instance whose decide disagrees with the proposition it claims to decide
  • Caching/memoization boundaries — Places where the kernel caches a result and the cache could become inconsistent (e.g., equiv_manager)

Differential testing across trust boundaries

  • Build lean4checker with external implementations disabled or replaced (e.g., pure-Lean Nat arithmetic instead of GMP)
  • For flagged candidates, compare results between standard and restricted checker builds
  • Flag any disagreement as a trust-boundary bug
  • Generalize beyond GMP — any external impl can be swapped for differential testing

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type
    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions