add docs
ober
6119ec25897ce37ddcfb4c61dd7418c50cac8b6b
new file mode 100644 --- /dev/null +++ b/docs/contracts.md @@ -0,0 +1,331 @@ +# Runtime Contracts for Jerboa + +Engineering plan for adding lightweight, opt-in runtime contracts to +Jerboa — borrowing Gerbil's scope-based `using` form rather than +Racket's per-definition wrapper macros. Inspiration: +`~/mine/gerbil/src/gerbil/core/contract.ss` and +`~/mine/gerbil/src/std/contract.ss`. + +--- + +## 0. ELI5 — What This Buys Us + +> *Why bother, when Scheme already throws an error when something is +> wrong?* + +Today, calling `(parse-config "/etc/hosts")` with the wrong kind of +input fails **deep inside** the function — maybe ten frames down, with +a message like `car: expected a pair, got #f`. You then have to read +the stack to figure out *which* caller passed garbage and *what* they +should have passed. + +With contracts, the same call fails **at the front door** with: + +``` +contract violation: parse-config + expected: string? + given: #<port> + in: arg 1 + blaming: config-loader.ss:42 +``` + +The bug is named, the violator is named, the location is named. No +stack-archaeology required. + +**Concretely you get:** + +1. **Error localization.** Failures point at the *caller*, not at some + inner helper. The single largest debugging-time win. +2. **Executable documentation.** The signature on `parse-config` is + the docstring, and it cannot drift from the code because it *is* + the code. +3. **Refactor safety.** Tighten a predicate from `number?` to + `exact-integer?` and every caller that was sloppy lights up. No + grep, no guessing. +4. **Tooling surface.** IDEs read the same predicates for completion + and signature help. Property-based test generators reuse them as + `gen` instances. Static analyzers can prune impossible branches. +5. **Cheap path to gradual typing later.** Contracts today, optional + compile-time checking of those same annotations tomorrow — without + a second migration. + +**What it does NOT buy:** + +- *Compile-time proof.* Failures still happen at runtime. To get + Rust-style "won't compile if wrong" you need a real type checker + (separate, larger project — see `docs/typed-jerboa.md` if/when + written). +- *Performance.* Contracts cost cycles. Designed correctly, the cost + lives at module boundaries (cheap), not inside hot loops. +- *Soundness across untyped→typed boundaries* unless higher-order + values are wrapped in chaperones. Phase 3 work. + +--- + +## 1. Scope + +In scope: + +- A new `(using (var :- type) body ...)` form in `(jerboa prelude)`. +- A separate `(: name signature)` form for module-export annotations. +- Desugaring that reuses existing `defstruct` predicates and Chez + record type descriptors. No new runtime machinery for the simple + case. +- Integration with chaperones (already in tree as of `28b8166`) for + higher-order arguments. +- A small set of standard combinators: `or/c`, `and/c`, `listof`, + `maybe`, `->`, `->*`. +- Error reporting that names the violating module, line, and argument + position. + +Out of scope (initially): + +- Full Racket-style blame tracking with party-positive/negative + flipping. Possible later; not needed for the first useful slice. +- Static (compile-time) checking. Annotations are runtime-only. +- Dependent contracts (`->i`). Defer until requested. +- Contract-driven test generation. Reuses the predicates but lives in + a separate module. + +--- + +## 2. Surface Syntax + +Two forms, both additive — existing code keeps compiling unchanged. + +### 2.1 Scope-based assertions (Gerbil-style) + +```scheme +(def (process-request req) + (using (req :- request?) ; assert req satisfies request? + (using (body :- string?) + (let ([body (request-body req)]) + (parse body))))) +``` + +`(using (var :- pred) body ...)` evaluates `body` in a scope where +`var` has been asserted to satisfy `pred`. On failure, raises a +contract violation pointing at the surrounding `def` and the failing +`using` form. + +For Jerboa-defined structures, `:-` can take a struct identifier +directly, matching Gerbil's idiom: + +```scheme +(defstruct request (method url headers body)) +(using (req :- request) ...) ; equivalent to (req :- request?) +``` + +### 2.2 Module-export annotations + +```scheme +(: parse-int (-> string? (or/c exact-integer? #f))) +(def (parse-int s) + ...) +``` + +`(: name signature)` attaches a checked signature to a top-level +binding. The check fires on every call that crosses the module +boundary (i.e., every external caller). Internal recursion does not +re-check. + +### 2.3 Combinators (minimal initial set) + +| Form | Meaning | +|-----------------------------|------------------------------------------| +| `(or/c p ...)` | satisfies any of the listed predicates | +| `(and/c p ...)` | satisfies all | +| `(listof p)` | a list whose elements all satisfy p | +| `(vectorof p)` | a vector whose elements all satisfy p | +| `(maybe p)` | `p` or `#f` | +| `(-> arg ... result)` | function contract | +| `(->* (req ...) (opt ...) result)` | optional/required arities | + +--- + +## 3. Desugaring and Semantics + +### 3.1 `using` expansion + +```scheme +(using (x :- string?) body ...) +;; expands to +(let ([x (or (and (string? x) x) + (raise-contract-violation 'x 'string? x + (current-source-location)))]) + body ...) +``` + +Plain. No allocation in the success case (the `and` short-circuits and +returns `x` unchanged). The raise path is cold and can carry as much +context as we want. + +### 3.2 `:` annotation expansion + +```scheme +(: parse-int (-> string? (or/c exact-integer? #f))) +(def (parse-int s) body) +;; expands to +(def parse-int + (let ([raw (lambda (s) body)]) + (lambda (s) + (using (s :- string?) + (let ([result (raw s)]) + (unless (or (exact-integer? result) (eq? result #f)) + (raise-contract-violation/result 'parse-int ...)) + result))))) +``` + +Wrapper allocated once at module load. Inner `raw` is the unchecked +body — recursive self-calls go through `raw`, not the wrapper, so +internal recursion is cheap. + +### 3.3 Higher-order via chaperones + +```scheme +(: map (-> (-> any/c any/c) list? list?)) +``` + +A `(->)` contract on a function argument is enforced lazily: when the +caller passes a procedure, we chaperone it so every call from inside +`map` checks its argument and result. This catches the case where the +caller passed a function with the wrong shape — without forcing us to +inspect the function's body. + +Reuses Chez's chaperone-procedure machinery; no new primitive. + +--- + +## 4. Integration with Existing Machinery + +| Existing feature | Reuse | +|-------------------------|------------------------------------------------------------------| +| `defstruct` predicates | `:- foo` resolves to `foo?` when `foo` is a defstruct name | +| Chez record descriptors | Used directly by `:-` for fast structural checks | +| Chaperones (`28b8166`) | Wrap higher-order args; lazy contract enforcement | +| `keyword:` args | `->*` distinguishes positional, optional, keyword | +| Reader extras | Untouched — no new lexical syntax, `:` is identifier-legal | + +No reader changes. No core-form changes. Everything is a macro. + +--- + +## 5. Implementation Phases + +### Phase 1 — `using` + flat predicates (1 week) + +- New macro `using` in `(jerboa prelude)`. +- `:-` resolves to predicate via syntax-local lookup (defstruct name → + predicate name). +- `raise-contract-violation` with source-location + identifier + value + + expected predicate. +- Tests: positive, negative, struct-name shorthand, nested `using`. + +Deliverable: every internal assertion `(unless (foo? x) (error ...))` +can be replaced with `(using (x :- foo?) ...)` and get better error +messages for free. + +### Phase 2 — `:` annotations + combinators (2 weeks) + +- `(: name signature)` macro. Captures signature at module top level, + associates with the next `def`. +- Combinators: `or/c`, `and/c`, `listof`, `vectorof`, `maybe`, `->`. +- Module-boundary wrapping: only exported bindings are wrapped. +- Tests: signature mismatch reporting, recursive-call performance. + +Deliverable: stdlib modules can opt in to contract-checked exports. + +### Phase 3 — Higher-order via chaperones (1–2 weeks) + +- `(->)` contracts on function-typed args wrap with chaperone. +- Blame: chaperone wrapper records *who* passed the bad function, so + the violation message names the caller, not the callee. +- Tests: `map`, `filter`, fold-style functions with bad procedures. + +Deliverable: `(-> (-> any/c any/c) list? list?)` enforces both the +function-shape and the list-shape. + +### Phase 4 — Tooling integration (open-ended) + +- Export contract metadata for `jerboa-apropos` / IDE signature help. +- Property-test bridge: given a `(-> p1 p2 result)`, generate test + inputs from `p1`, `p2` predicates. +- Optional: contract-stripping build mode for benchmarking (NOT for + release builds — silent semantic change is worse than the cost). + +--- + +## 6. Performance Budget + +| Site | Cost | Acceptable? | +|-------------------------------|----------------------------|----------------------------| +| `using (x :- pred)` success | one predicate call | yes | +| Internal recursion | unchanged (calls `raw`) | yes | +| Module-boundary call | predicate + result check | yes — boundaries are rare | +| `(listof p)` check | O(n) | document; provide opt-out | +| Chaperoned higher-order call | ~2× call overhead | yes for non-hot paths | + +Rough expectation: ~5–20% overhead at instrumented module boundaries, +near-zero inside. Hot inner loops should not cross module boundaries +on every iteration anyway. + +--- + +## 7. Risks and Open Questions + +1. **`using` vs. `let`-binding rebinding.** Gerbil's `using` shadows + the variable in scope. We follow the same rule. Document it. + +2. **Macro hygiene around `:-`.** The `:-` token is a literal in + `using`; needs `syntax-parse`-style literal binding so user code + that uses `:-` for other purposes isn't broken. + +3. **Error formatting in non-terminal contexts.** Contract violations + from inside a chaperoned callback may surface far from the original + call site. Phase 3 needs careful blame plumbing. + +4. **Interaction with `eval` / dynamic dispatch.** A contract attached + to a `def` is invisible to direct procedure references obtained via + `eval`. Acceptable — `eval` already breaks every static guarantee. + +5. **Cost of `or/c` short-circuit.** Trivially solvable but document: + put the cheap, common cases first in `(or/c integer? string? ...)`. + +6. **Should `:` annotations be enforced on imports?** I.e., if module + A imports `parse-int` from B, does A see the contract-wrapped + version or the raw one? **Decision:** always the wrapped version. + Otherwise contracts are toothless. Internal recursion stays raw via + the `raw` binding. + +7. **Source-location capture for the violator.** Easy at the macro + site (we have it). Harder at the indirect-call site (the actual + bad caller). Phase 3 problem. + +--- + +## 8. Out-of-Scope Future Work + +- **Compile-time checking** of `:` signatures (a real type checker). + Would land as `docs/typed-jerboa.md` if pursued. +- **Refinement contracts** (`(integer-in 0 255)` with range checks). + Trivially expressible as `(and/c integer? (lambda (n) (<= 0 n 255)))` + in the meantime. +- **Contract inference** from usage. Probably not worth it; explicit + is fine here. +- **Module-level invariants** beyond function signatures (e.g., "this + hash-table only contains symbol keys"). Possible but big. + +--- + +## 9. References + +- Gerbil: `~/mine/gerbil/src/gerbil/core/contract.ss`, + `~/mine/gerbil/src/std/contract.ss` — scope-based `using`, MOP + integration, no blame tracking. +- Racket: `racket/contract` — full blame tracking, party flipping, + much richer but heavier surface. +- Findler & Felleisen, "Contracts for Higher-Order Functions" + (ICFP 2002) — the blame-tracking semantics. +- Typed Racket — `:` annotation form, gradual-typing soundness work. +- Jerboa internals: `lib/jerboa/prelude/*.sls`, + `lib/std/chaperone.sls`, `lib/jerboa/defstruct.sls`. new file mode 100644 --- /dev/null +++ b/docs/uhoh.md @@ -0,0 +1,258 @@ +# Uh Oh — A Field Guide to Reimplemented-Crypto Disasters + +A curated graveyard of real-world incidents where someone re-rolled +their own cryptographic code (or just made small, "obvious" changes +to existing code) and got bitten. Read in order of severity, weep, +then link `ring` / `libsodium` for anything involving keys, nonces, +or signatures. + +The takeaway up front: **the bugs are never in the algorithm.** They +are in nonce reuse, RNG seeding, error-path control flow, parameter +choice, side channels, padding oracles, and constant-time violations. +A re-implementer doesn't know to worry about these things until after +the CVE has their name on it. + +--- + +## 1. Debian OpenSSL RNG (CVE-2008-0166, 2008) + +**What happened.** A Debian maintainer noticed Valgrind flagging two +lines in OpenSSL's PRNG as "uninitialized memory reads." They +commented the lines out. The lines were *deliberately* feeding +uninitialized memory into the entropy pool — that was the point. + +**Consequence.** The PRNG's effective key space collapsed from +2^1024-ish to **~32,768** possible keys. *Every* SSH key, TLS cert, +OpenVPN key, DNSSEC key, and GPG key generated on Debian or Ubuntu +between **September 2006 and May 2008** was effectively guessable in +seconds. + +**Cleanup.** Worldwide mass key rotation. Years of residual fallout +as people found unrotated keys in production into the 2010s. + +**Lesson.** Cryptographic code looks weird *on purpose*. Don't "tidy +up" code you don't understand. The maintainer was acting in good +faith — that's the scary part. + +--- + +## 2. Sony PlayStation 3 ECDSA (2010) + +**What happened.** Sony's PS3 firmware-signing code used ECDSA but +**reused the same random nonce `k`** across every signature instead +of generating a fresh one per signature. + +**The math.** ECDSA's security depends on `k` being unpredictable and +fresh. Two signatures `(r, s1)` and `(r, s2)` with the same `k` over +different messages let an attacker recover the private key with +high-school algebra. fail0verflow demonstrated this on stage at 27C3. + +**Consequence.** Sony's master code-signing key extracted. Every PS3 +fully jailbroken. Sony's response (suing the researchers, mass +account compromises) is its own separate disaster. + +**Lesson.** ECDSA is a foot-gun. Use Ed25519, where `k` is derived +deterministically from the message and key, removing this entire +class of bug. (Cloudflare, Salt, and many others have hit the same +nonce-reuse pattern since.) + +--- + +## 3. Apple "goto fail" (CVE-2014-1266, 2014) + +**What happened.** Someone (Apple's iOS/macOS TLS implementation, in +`sslKeyExchange.c`) had a stray duplicated line in the cert +validation chain: + +```c + if ((err = SSLHashSHA1.update(&hashCtx, &signedParams)) != 0) + goto fail; + goto fail; // <-- duplicate. Always taken. + if ((err = SSLHashSHA1.final(&hashCtx, &hashOut)) != 0) + goto fail; +``` + +Because there are no braces, the second `goto fail` is **always** +executed, unconditionally skipping the final signature check. The +function then returns success with `err == 0`. + +**Consequence.** Every iOS and macOS device shipped with broken +HTTPS for months. Any MITM could forge any cert. Caught only when a +researcher noticed it in the open-sourced Security framework. + +**Lesson.** Mandatory braces in security-critical code aren't +aesthetic; they're load-bearing. Also: lint for unreachable code. +Also: have *tests* that try to authenticate a wrong cert and ensure +the function returns failure. + +--- + +## 4. Android `SecureRandom` (2013) + +**What happened.** Android's Java `SecureRandom` implementation had +a bug where, under certain conditions, the OpenSSL PRNG it wrapped +**wasn't properly seeded** from `/dev/urandom`. Different apps could +generate the same "random" values. + +**Consequence.** Bitcoin wallet apps generated **colliding ECDSA +private keys**. Funds drained from multiple wallets that, unbeknownst +to their owners, shared the same secret. Estimated ~55 BTC moved +before disclosure. + +**Lesson.** Seeding is the whole game. A "secure" RNG that isn't +seeded is a deterministic function. And the platform you trust to +seed it might not, silently. + +--- + +## 5. Juniper ScreenOS Dual_EC Backdoor (CVE-2015-7755, 2015) + +**What happened.** Juniper's NetScreen firewalls used the Dual_EC +PRNG (already widely suspected to contain an NSA backdoor via chosen +constants `P` and `Q`). At some point between 2012 and 2014, an +**unauthorized commit** to ScreenOS replaced the `Q` constant with a +different value — installing *someone else's* backdoor on top of +the existing one. + +**Consequence.** Anyone holding the matching private discrete log of +the swapped `Q` could decrypt VPN traffic from any Juniper ScreenOS +firewall worldwide. Active for **~3 years** before Juniper disclosed +it. To this day, attribution is murky. + +**Lesson.** Even reading a vendored crypto implementation isn't +enough — you need to know which constants are sensitive and verify +them against the standard. The bug is invisible to code review +unless you're already paranoid about the specific lines that matter. + +--- + +## 6. MEGA Cloud Storage (2022) + +**What happened.** Cryptographers at ETH Zürich +([Backendal, Haller, Paterson 2022](https://mega-awry.io/)) +analyzed MEGA's homegrown end-to-end encryption protocol. + +They found: +- **RSA key recovery** from ~512 logins, by exploiting MEGA's + unauthenticated CBC-mode decryption oracle. +- **Plaintext recovery** for arbitrary user files. +- **Framing attack** letting MEGA insert files into a user's storage + that appear to have been encrypted by the user. + +**Consequence.** Every claim MEGA made about "we can't read your +files" was false against an attacker willing to log in 512 times. +The protocol had been deployed since 2013 — **~9 years undetected**. + +**Lesson.** "We use AES" is not a security argument. Protocol design +is where crypto fails, and protocols need adversarial review by +actual cryptographers, not just engineers who read the AES spec. + +--- + +## 7. Telegram MTProto (2015, 2020, 2021, ongoing) + +**What happened.** Telegram rolled their own end-to-end protocol +("MTProto") instead of using an audited primitive like the Signal +protocol or even just TLS + a vetted ratchet. + +Academic findings: +- **2015** (Jakobsen & Orlandi): MTProto v1 lacks IND-CCA security; + trivial chosen-ciphertext distinguishers exist. +- **2020** (Albrecht et al.): MTProto v2 has subtle padding/IV + issues, attacks on message reordering. +- **2021**: more findings on the protocol's auth mechanisms. + +**Consequence.** Telegram's "secret chats" have repeatedly been +shown to fall short of the security guarantees an end-to-end +encrypted protocol should provide. Telegram's response is usually +to dispute findings, fix quietly, and move on. + +**Lesson.** "We did it ourselves so we can verify it ourselves" is +the opposite of how cryptographic trust works. Public, audited +protocols accrue attacker-attention; private ones accrue *only* +their authors' attention. + +--- + +## 8. CryptoCat (2013) + +**What happened.** A browser-based encrypted-chat tool. The +group-chat implementation derived group keys from a custom PRNG. +The PRNG had only ~2^54 effective entropy due to a bug in how +random values were generated and mixed. + +**Consequence.** Every group conversation in CryptoCat for +approximately **7 months** was decryptable by anyone who recorded +the ciphertexts and was willing to brute-force the keyspace. ~54 +bits is a few hours on modest hardware. + +**Lesson.** Browser crypto is hard. JavaScript randomness sources +are limited. Custom mixing functions are landmines. If you must do +crypto in a browser, use `window.crypto.subtle` and nothing else. + +--- + +## 9. Bonus Round — Honorable Mentions + +- **Heartbleed (CVE-2014-0160).** OpenSSL itself. Bounds-check bug + in the heartbeat extension leaked up to 64 KB of server memory + per request — including private keys. Not a *reimplementation* + bug, but evidence that even the canonical lib has had its day. + +- **WPA2 KRACK (2017).** Protocol-level reinstallation attack on + the 4-way handshake. Affected every Wi-Fi device. Bug was in the + spec, not anyone's impl. + +- **DROWN, BEAST, CRIME, POODLE, Lucky13, Logjam, Sweet32.** A + decade of TLS attacks, most exploiting padding oracles, downgrade + paths, or compression side-channels that the original protocol + designers didn't anticipate. + +- **OpenBSD's `getentropy` saga.** Even OpenBSD — known for being + pickier than anyone about crypto correctness — has had to revise + their RNG architecture multiple times. If they can't get it right + on the first try, neither can you. + +- **Trezor / Ledger / etc. hardware wallets.** Several CVEs from + rolling their own ECC code, mostly around side channels and + fault injection. + +- **Cloudflare's golang Ed25519 reimpl (2019).** A pure-Go Ed25519 + that mishandled small-order points. Caught early by review — + but it was caught *because* multiple reviewers were paranoid + about this *exact* class of bug. Most projects aren't reviewed + that carefully. + +--- + +## 10. Practical Rule for Jerboa + +| What you're implementing | Roll your own? | +|------------------------------------------|----------------| +| Hash functions (SHA-256, MD5, Blake3) | OK — verifiable against test vectors, no secrets in flight | +| HMAC | OK if built atop a vetted hash, with constant-time compare | +| AEAD (ChaCha20-Poly1305, AES-GCM) | **No.** Nonce/IV handling is the trap | +| Public-key (RSA, ECDSA, Ed25519, X25519) | **No.** Side channels, point validation, parameter choice | +| Signatures, KDFs, password hashing | **No.** Use `ring`, `libsodium`, `argon2` | +| TLS / Noise / any handshake protocol | **Absolutely not.** Use `rustls` | +| Random number generation | **No.** Use OS CSPRNG (`getrandom(2)`) directly, full stop | + +**The rule of thumb:** if a *secret* (key, nonce, password, signature +private half) flows through your code, link a vetted library. If only +public bytes flow through (digests, MACs you're verifying, base64, +PEM parsing), pure Jerboa is fine and arguably safer than FFI. + +This is why `(std crypto)`'s MD5 and SHA-256 in pure Scheme is the +right call, while `ed25519.rs` and `x25519.rs` and `tls.rs` staying +in `jerboa-native-rs` is also the right call. The boundary is *which +operations touch secrets*, not *which language is fashionable*. + +--- + +## 11. Further Reading + +- [Cryptography Engineering](https://www.schneier.com/books/cryptography-engineering/) — Ferguson, Schneier, Kohno +- [Real World Cryptography](https://nostarch.com/real-world-cryptography) — David Wong +- [mega-awry.io](https://mega-awry.io/) — the MEGA writeup; a model of how to disclose a protocol break +- [The Galois Curve25519 verification](https://github.com/mit-plv/fiat-crypto) — what it actually takes to ship "obviously correct" crypto +- [The Matrix.org breach (2019)](https://matrix.org/blog/2019/05/08/post-mortem-and-remediations-for-apr-11-incident) — for what reimplementing crypto for performance buys you