Security: SAML XSW auth bypass, reactor UAF, request-size DoS, authz + crypto hardening

[junjihashimoto]

Security review of the current branch turned up several issues across the auth layer and the (this-session-new) FFI HTTP backends. This PR fixes them, in the reviewed priority order, and adds regression tests. All changes build clean; security_spec 82/82, pure_spec 36/36, and 7 new SAML XSW tests pass.

🔴 SAML XML Signature Wrapping → authentication bypass

Auth/Saml.lean — validate verified a signature with xmlsec1 but then read identity from the first <Assertion> in document order, with nothing tying the two together. An attacker keeps the legitimately-signed assertion where xmlsec1 is happy and injects a forged assertion first; parseResponse consumes the forgery → full auth bypass (the classic XSW class: Google/SAML 2012, Duo 2018).

Fix: checkNoWrapping enforces invariants a minimal string parser can guarantee — exactly one <Assertion> in the document, and a <Signature> whose Reference URI is #<AssertionID>. Since xmlsec1 checks against the IdP cert only, success now means the single assertion we parse is the one the IdP signed. 7 unit tests added (wrapping / wrong-reference / unsigned all rejected; legit single signed assertion accepted).

Same file: fixed-name /tmp/saml_response.xml → IO.FS.withTempDir (concurrent validations were clobbering each other + symlink vector); String.fromUTF8! → fromUTF8? (malformed input panicked the server = DoS).

🔴 Reactor use-after-free (remotely reachable)

c/leantea_reactor.c — binds INADDR_ANY. When one fd was both readable and writable in a single kevent()/epoll_wait() batch, on_readable could conn_close()+free the connection and then on_writable() dereferenced freed memory. Fix: deferred free — conn_close marks the conn closing and parks it on a per-reactor dead list; reactor_reap() frees once per batch after all events dispatch; both loops skip a closing conn. Verified 1.3M requests under wrk -c256, no crash.

🔴 Unbounded-memory DoS (all three backends)

No cap on Content-Length or header accumulation → giant Content-Length or a never-terminating header stream (slowloris) grew the read buffer to OOM. The Http.lean "1 MB cap" doc comment described a limit that was never implemented. Fix: 64 KB header / 8 MB request caps enforced in each read loop (reactor C, FastServer, libuv Server); parse_content_length saturated to kill a signed-overflow UB. Verified: 20 MB body dropped, server survives, on both FFI backends. Doc corrected to the real limits.

🟠 Authorization was opt-in → SecureRoute

Auth/Proof.lean — Proof/AuthRoute enforce authz on routes you choose to wrap, but a route added through a plain Handler simply had no check. Fix: SecureRoute forces every entry to be .needs c (proof enforced) or .anyone (explicitly public) — no unstated third case, so a forgotten guard doesn't typecheck and an open endpoint is a greppable .anyone. dispatchSecure routes the list. (Doesn't force an app to use it — a convention — but removes the silent-omission failure mode within the router.)

🟠 Predictable temp files in openssl shell-out

Crypto/Jwt.lean, Auth/Passkey.lean — the RS256/ECDSA fallback path (native libcrypto backend off) wrote to /tmp/jwt_*_{nowSec} / fixed /tmp/passkey_*: epoch-second suffix collides under concurrency, fixed names race outright, both invite symlink pre-creation (CWE-377/367); JWT data file carried the payload at 0644. Fix: IO.FS.withTempDir everywhere; dropped a pointless attacker-data write in the Passkey registration stub.

🟡 PBKDF2 default too low

Crypto/Password.lean — 20 000 iterations is well under OWASP's floor. Raised to 100 000 (pure-Lean-verifiable in login-acceptable time) and documented the native LEANTEA_CRYPTO=1 path for reaching 600 000 without a pure-Lean CPU cost.

README accuracy

"Eight primitives" → nine (CSP was shipped but unlisted); "one inlined JS file / Web Speech API only" corrected (runtime JS served separately, fetch/History/DOM used); "Typed RPC (Servant-style)" → "Shared-endpoint RPC (Servant-inspired)" with an honest note that a Handler is still List String → IO String and typed Endpoint α β is roadmap; removed a reference to a nonexistent examples/Sheet/Api.lean.

Test plan

• lake build clean (176 targets)
• security_spec 82/82
• pure_spec 36/36 (Password/JWT)
• auth_spec SAML group incl. 7 new XSW tests pass (the 5 failing entries are the pre-existing OAuth2-round-trip tests that need a live IdP subprocess + curl — unrelated to this change)
• All three HTTP backends serve 200; reactor + FastServer drop a 20 MB body and survive
• Reactor UAF: 1.3M requests under wrk -t8 -c256, no crash

Not addressed here (follow-ups)

• SAML: encrypted assertions / exotic canonicalisation still warrant a real XML-DSig library; the string-parser hardening covers the common wrapping vectors, not everything.
• resolveRole : Session → Capability remains an app-supplied trust boundary by design.