docs: future-proofing strategy for AI-era language adversaries
ober
f20d5b1861f1cd9f44d8dfc51625ef0656755ad1
new file mode 100644 --- /dev/null +++ b/docs/Future-proofing.md @@ -0,0 +1,380 @@ +# Future-Proofing Jerboa Against AI-Era Adversaries + +Forward-looking design strategy for keeping Jerboa robust as AI-driven bug +hunting and exploit construction scale. This document is the strategic / +language-design layer; see the cross-references at the end for the +current-state assessment and the per-subsystem detail. + +--- + +## 1. Threat Model + +What changed in the AI era: + +- **Scale of variant analysis.** A CVE in OpenSSL becomes a systematic + search across all C codebases within hours, not months. +- **Semantic fuzzing.** Coverage-guided fuzzers primed with + LLM-generated test inputs that understand grammars and protocol state + machines, not just byte-level mutation. +- **Automated exploit-chain construction.** Public PoCs assembled from + a CVE description plus a bug-class library, with minimal human time. +- **Variant hunting across forks and history.** Regression detection + across git history at scale; the same bug introduced years apart in + different forks is now findable in a single pass. +- **Reverse engineering at scale.** Binary analysis that previously + required expert manual work is now routine for any tool. + +What did not change: + +- **Logic bugs in unfamiliar domains** still benefit from human + reasoning more often than AI bug-hunters expect — though the gap is + closing. +- **Stated invariants and types are easier to verify than to evade.** + Every spec you write is a wall AI must climb, not just speculate + around. Refutation requires a counterexample; speculation generalises. +- **Defense via small, well-defined trust boundaries scales linearly; + "harden everything everywhere" does not.** + +The strategic implication: the language posture that wins is not "fewer +bugs" (a losing race at scale) but **bugs that exist cannot compose +into exploits, cannot reach interesting capabilities, and cannot evade +audit.** + +--- + +## 2. Strategic Posture — Three Axes + +Every design choice should ladder up to at least one of: + +**A. Eliminate bug classes by construction.** A bug the language makes +structurally impossible cannot be found by any analysis. This compounds: +each eliminated class is a permanent reduction in the adversary's +effective search space. + +**B. Break the exploit chain.** Even when individual bugs exist, an +exploit needs them to compose into a chain that reaches an interesting +capability. Capability discipline, effects in types, and structural CFI +all attack the chain rather than the bugs. + +**C. Shrink the trust boundary.** A small, well-defined TCB that is +heavily verified outperforms a large, casually-trusted runtime. Finding +a bug in 5 KLOC of audited interpreter is hard; finding a bug in 5 MLOC +of pragmatic runtime is easy. + +--- + +## 3. Core Principles + +Ranked roughly by force, each with Jerboa's current status. + +### 3.1 Eliminate, Don't Detect + +Memory safety, no null, no unchecked integer overflow, no raw pointers, +no implicit type conversions, no buffer-of-bytes-pretending-to-be-typed-data. + +A bug the language makes impossible cannot be found. Memory safety +alone eliminates 60-70% of historical C CVEs. + +**Jerboa today:** Memory safety via Chez Scheme — strong. `#f` instead +of null where idiomatic, but null-equivalents still creep into some +APIs. Integer overflow is checked in fixnum arithmetic; bignum +promotion is automatic. + +**Gap:** Some standard idioms (untyped hash tables, association lists, +raw bytevectors threaded through layers) re-introduce shapes that +bypass static reasoning. Encouraging `defstruct` / `defrecord` over +ad-hoc hash maps tightens this without language changes. + +### 3.2 Capabilities, Not Ambient Authority + +A function with no file-system capability in scope must be **unable** +to open files, not merely discouraged from doing so. Object-capability +discipline (Pony, E, Caja) is the strongest single multiplier: an RCE +in module X stops being equivalent to an RCE everywhere. + +**Jerboa today:** `(std capability)` implements the model, with +attenuation and revocation. See `capability.md`. + +**Gap:** Adoption is opt-in. The default prelude exposes ambient +authority (`open-output-file`, `system`, etc.). Until the **default** +is capability-required and ambient authority is **opt-in**, the model +doesn't bite. + +**Convergence path:** Promote `(jerboa prelude safe)` (the existing +113-binding allowlist documented in `ai-threat.md`) to the production +default for new projects. Make ambient-authority imports explicit, +greppable, and audited. Add a static check that production code does +not import the unsafe prelude. + +### 3.3 Effects in the Type System + +Function signatures should declare what side effects are performed +(fs-read, fs-write, network, exec, alloc). AI-generated code then +cannot sneak in effects without changing types that reviewers see. + +**Jerboa today:** `(std effect)` provides algebraic effects with +handlers. See `effects.md`. + +**Gap:** Like capabilities, effect declarations are opt-in rather than +required. A function that performs IO without declaring it is currently +legal. + +**Convergence path:** Move toward effect inference at compile time, +with declared signatures required on module boundaries. Initially a +lint, eventually a build-time error in strict mode. + +### 3.4 Structural Control-Flow Integrity via WASM + +WebAssembly's separated code/data spaces, typed indirect calls, and +absence of `ret` make ROP **structurally impossible** — not merely +mitigated. Compiling security-critical components to WASM gives this +for free without per-platform hardware work. + +**Jerboa today:** The wasm runtime infrastructure exists — +`(std wasm)`, `jerboa-native-rs` embeds `wasmi`. `secure.md` lays out +a multi-phase rollout. `jerboa-websearch` has shipped wasm-sandboxed +HTML parsing (`src/jerbsearch/sandbox/html-parse.ss`) — the canonical +working example. + +**Gap:** Adoption is per-project and incomplete. `jerboa-dns` currently +parses untrusted UDP wire bytes in native Scheme despite `secure.md` +listing the DNS-parser-in-wasm migration as Phase 1b. This is the +**canonical "case-by-case drift" failure**: the pattern exists, the +default doesn't, and the maintainer's mental model drifts ahead of the +code. + +**Convergence path:** Push wasm-sandboxed parsing into the standard +library as the default for untrusted-byte parsers. A `(std parse +sandboxed)` API that takes bytes and returns a typed parse result, +with the wasm wrapping invisible to the caller. + +### 3.5 First-Class Parser Primitives with Proven Bounds + +WUFFS is the prototype: a domain-specific language for byte parsers +where the compiler proves array bounds, integer bounds, and termination. +Ad-hoc `string-split + index-lookup` parsing is exactly where AI +variant-hunters score easy hits — every protocol parser written this +way has the same bug class. A standard parser story eliminates the +variance. + +**Jerboa today:** No equivalent. Protocol parsers in the ecosystem are +hand-rolled bytevector manipulation (see +`~/mine/jerboa-dns/lib/jerboa-dns/protocol.sls`). + +**Convergence path:** Adopt or build a parser-combinator library with +explicit bounds tracking. Long-term, a Jerboa-flavored WUFFS — a +subset language that compiles to safe bytevector operations with +compile-time proofs. + +### 3.6 Refinement Types / Contracts Default-On + +Function pre/post-conditions and refinement predicates raise AI's bar +significantly: instead of "this might be wrong, let me speculate," it +must produce a counterexample to a stated invariant. Speculation +generalises; counterexamples don't. + +**Jerboa today:** `define/ct` and `lambda/ct` provide contract-typing +per-function. Used inconsistently across stdlib and downstream code. + +**Convergence path:** Make contract-typing on by default for new code +in `(std ...)`. Surface uncovered-boundary warnings in the linter. +Long-term: SMT-backed refinement checking for numerically-precise +invariants. + +### 3.7 Linear / Affine Types for Resources + +Resources (file handles, sockets, capability tokens, cryptographic +keys) consumed-on-use eliminate whole categories: use-after-close, +double-spend, TOCTOU on capability checks. + +**Jerboa today:** No linearity in the type system. `with-resource` +provides scoped cleanup but does not prevent the handle escaping the +scope. + +**Convergence path:** Introduce affine annotations in `define/ct` for +resource-bearing values. Mark capability tokens and file handles as +affine in the standard library. + +### 3.8 Small, Formally Specified TCB + +The smaller and more deliberately scoped the trust base, the more +tractably it can be audited and the less surface there is for runtime +bugs. Large ambient runtimes (Scheme + libkernel + Rust runtime) have +many gadgets, many idiom bugs, and many attack-relevant primitives. + +**Jerboa today:** Chez Scheme + libkernel is ~1 MB of native code. Per +`secure.md`, this is the primary ROP gadget source. + +**Convergence path:** `secure.md` enumerates the options — harden Chez +with CET/SHSTK and hardening CFLAGS, switch security-critical paths to +WASM so the TCB they depend on shrinks to the wasm runtime, or in the +extreme, target a minimal interpreter (s7) for high-assurance tools. + +--- + +## 4. Anti-Patterns + +Things that look like security wins but aren't, or that quietly defeat +the principles above. + +### 4.1 Obscurity as Defense + +"Jerboa is niche, so AI is bad at it." True today, false in 18 months. +Worse: your own LLM tooling suffers symmetrically — every advantage to +the adversary is a disadvantage to you. `jerboa-lora` is the workaround, +but it's a tax, not a structural defense. + +### 4.2 Liberal FFI + +Every `foreign-procedure` is a hole through which the safety model +leaks. The "Fearless FFI" doc (`ffi.md`) introduces a DSL that is much +safer than raw bindings, but the **existence** of the unsafe primitives +in the unrestricted prelude means a future contributor or LLM can reach +for them without noticing the cost. FFI should require an `unsafe` +capability gated and visible at the call site. + +### 4.3 Big Language Surface + +Every feature is a future idiom bug. Macros, reflection, dynamic +loading, `eval` — each is a place where AI variant-hunters will look +for bypass patterns. Add features grudgingly; remove or restrict where +possible. + +### 4.4 Convenience Features That Shadow Safer Alternatives + +If the safe way is verbose, no one uses it under deadline pressure — +and LLMs trained on existing code generate the convenient idiom, not +the safe one. **The easy default must be the safe default.** If +`string-split` is one line and `parse-with-bounds` is six, parsers will +be written with `string-split`. + +### 4.5 Runtime-Only Safety + +A runtime check is something AI can fuzz until it triggers, then write +an exploit around. A compile-time impossibility is something AI cannot +interact with at all. Prefer types, refinements, and capabilities over +runtime assertions wherever feasible. + +### 4.6 Ad-Hoc Per-Project Security Architecture + +The `jerboa-dns` case study makes this concrete: the project's mental +model said "wasm-sandboxed parsing," the code said "native Scheme on +raw UDP bytes." Case-by-case decisions about which security primitives +to deploy drift under time pressure and LLM-assisted feature work. +**The architecture has to encode the security decision, not the +maintainer's intent.** + +--- + +## 5. Where Jerboa Stands — Honest Inventory + +| Principle | Status | Notes | +|------------------------|:--------:|--------------------------------------------------| +| Memory safety | ✓ Strong | Chez Scheme foundation | +| Capabilities | ◐ Partial| `(std capability)` exists; adoption opt-in | +| Effects | ◐ Partial| `(std effect)` exists; declarations opt-in | +| WASM CFI | ◐ Partial| Runtime exists; deployment per-project | +| Parser proofs | ✗ Missing| Hand-rolled bytevector parsing dominant | +| Refinement / contracts | ◐ Weak | `define/ct` exists; not the default | +| Linear / affine | ✗ Missing| `with-resource` is scoped cleanup, not linearity | +| Small TCB | ◐ Partial| Chez + libkernel large; `secure.md` plans work | +| Safe-by-default prelude| ◐ Partial| `(jerboa prelude safe)` exists, not yet default | + +The pattern is consistent: many of the right primitives exist; they +are not the default. **The work for the next era is less "build new +mechanisms" than "make the existing safe ones the path of least +resistance."** + +--- + +## 6. Realistic Convergence Path + +In rough priority order: + +1. **Finish the in-flight wasm migration.** `secure.md` Phases 1a/1b — + embed wasmi properly, port the DNS parser to Rust→WASM. Take + `jerboa-dns` off the "claims wasm, isn't" list. + +2. **Make wasm-sandboxed parsing the stdlib default.** A + `(std parse sandboxed)` API where wasm wrapping is invisible to the + caller. Hand-rolled parsers become the explicit opt-out, not the + implicit default. + +3. **Gate FFI behind an explicit unsafe-tagged surface.** + `(jerboa prelude)` does not export `foreign-procedure`. Code wanting + FFI imports `(jerboa prelude unsafe)` or equivalent — auditable via + `grep`. + +4. **Promote the safe prelude to the production default.** + `(jerboa prelude safe)` exists already; make it the default for new + projects via `jerbuild` templates. Existing projects opt in as they + migrate. + +5. **Add a contract / spec coverage pass.** Extend `define/ct` to be on + by default in stdlib modules. Surface contract coverage in + `jerboa_security_audit`. Long-term: SMT-backed refinement checking + on numeric invariants. + +6. **Build the linear-resource discipline.** Mark capability tokens, + file handles, and crypto keys as affine in stdlib types. Lint for + escape via `define/ct` annotations. + +7. **Audit `secure.md` for other "claimed but not shipped" items.** + The `jerboa-dns` gap suggests other Phase-1 work may also be + deferred without the gap being visible from the top of the project. + +Each step is a refactor of an already-working system, not a research +project. The cumulative effect over a year of incremental work is +substantial; the cost of any single step is bounded. + +--- + +## 7. Reference Language Comparison + +| Language | Mem safety | Capabilities | Effects in types | Structural CFI | Parser proofs | Refinement | Linear | +|-------------------|:---------:|:------------:|:----------------:|:--------------:|:-------------:|:----------:|:--------:| +| C / C++ | ✗ | ✗ | ✗ | ✗ | ✗ | ✗ | ✗ | +| Rust | ✓ | ✗ | ✗ | partial | ✗ | ✗ | affine | +| Haskell | ✓ | ✗ | partial (IO) | ✗ | ✗ | partial (LH)| ✗ | +| Pony | ✓ | ✓ | ✗ | ✗ | ✗ | ✗ | ref-caps | +| Koka / Eff | ✓ | ✗ | ✓ | ✗ | ✗ | ✗ | ✗ | +| WUFFS | ✓ | ✗ | ✗ | ✗ | ✓ | partial | ✗ | +| Idris / Lean | ✓ | partial | ✓ | ✗ | partial | ✓ | ✓ | +| WebAssembly | ✓ | partial | ✗ | ✓ | ✗ | ✗ | ✗ | +| **Jerboa today** | ✓ | opt-in | opt-in | via wasm (per-project) | ✗ | opt-in | ✗ | +| **Jerboa target** | ✓ | default | default | default | ✓ | default | ✓ | + +No shipping language combines all of the principles. The Jerboa +opportunity is to converge the combination over time as a series of +refactors, not a research project. Each row of the "Jerboa target" line +maps to a concrete step in §6. + +--- + +## 8. Cross-References + +- `ai-threat.md` — Current-state security assessment; complements this + document's forward-looking framing +- `capability.md` — `(std capability)` API and patterns for the + object-capability model +- `effects.md` — `(std effect)` API for algebraic effects +- `ffi.md` — Current FFI surface and the "Fearless FFI" DSL +- `../secure.md` — Concrete binary-hardening roadmap (Chez / musl / + wasm-runtime work) +- `architecture-split.md` — Chez / Rust / wasm split architecture + +--- + +## 9. Maintenance + +This document is forward-looking. As convergence work in §6 lands, +update §5's status table and shorten or remove the gap notes in §3. +When the "Jerboa today" row of the §7 comparison table catches up to +"Jerboa target," collapse them into a single row and write a new +target reflecting the next horizon. + +Drift between this document and the code is itself a smell — if the +status table claims a default that the code doesn't enforce (as +`jerboa-dns` did with wasm sandboxing), that's the same case-by-case +drift §4.6 warns about, applied to documentation. Fix the code or fix +the doc.