diff --git a/CHANGELOG.md b/CHANGELOG.md index 8e5b08d..5236ba5 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,6 +1,22 @@ # Changelog -All notable changes to lean-grpc are documented here. The package version is the Lake/`Grpc.version` semver (currently **1.0.0**). Git tags such as `v1.0.0` are created manually by maintainers when publishing. +All notable changes to lean-grpc are documented here. The package version is the Lake/`Grpc.version` semver (currently **1.1.0**). Git tags such as `v1.1.0` are created manually by maintainers when publishing. + +## [1.1.0] — 2026-08-04 + +Additive IAM surface for enterprise mTLS AuthN (lean-compliance G1–G4). + +- **Peer identity:** `Grpc.Native.Tls.peerIdentity?` extracts verified client cert fields (RFC 2253 subject DN, CN, DNS/URI SANs, SHA-256 fingerprint, serial) via OpenSSL after mTLS handshake. +- **Request context:** `ServerCallContext` + `registerWithContext` / `registerTypedWithContext` pass `peerIdentity`, inbound metadata, and `methodPath` into unary handlers. Legacy `register` remains (ignores context). +- **TLS serve:** `Tls.serveH2` takes a per-connection handler factory; failed accepts/handshakes are logged and the listen loop continues. +- **Interceptors:** `registerUnaryWithContext`, `requirePeerIdentity` (fail closed when `mtlsRequired` and identity missing). +- **Tests:** `tlsLoopback` covers dual-cert identity binding, metadata non-forgery, h2c → `none`, accept-loop survival. +- **Codegen:** `protoc-gen-lean4-grpc` emits `register{Svc}{Method}WithContext` alongside body-only registrars. +- **Examples:** MirrorForge `Stamp` uses `registerUnaryWithContext` (Bearer metadata + body-token fallback; optional env-gated TLS/mTLS). +- **Docs:** cookbook mTLS → `ctx.peerIdentity`; API reference; security PKI note. +- **Deferred:** streaming handlers with context; trusted-proxy identity mode; JWT/OIDC validation inside lean-grpc. + +Migration: additive API — bump consumer pin from `v1.0.0` to `v1.1.0`. Prefer `registerWithContext` for AuthN; do not trust client-supplied subject metadata. ## [1.0.0] — 2026-08-02 diff --git a/Examples/Helloworld/Generated.lean b/Examples/Helloworld/Generated.lean index 728b66c..d93996d 100644 --- a/Examples/Helloworld/Generated.lean +++ b/Examples/Helloworld/Generated.lean @@ -65,4 +65,10 @@ def registerGreeterSayHello (s : Grpc.Server) let (resp, st) ← h req return (HelloReply.encode resp, st) +/-- Register a typed unary handler with `ServerCallContext` for `Greeter/SayHello`. -/ +def registerGreeterSayHelloWithContext (s : Grpc.Server) + (h : Grpc.ServerCallContext → HelloRequest → IO (HelloReply × Grpc.Status)) : Grpc.Server := + Grpc.Server.registerTypedWithContext s "helloworld.Greeter" "SayHello" + HelloRequest.decode HelloReply.encode h + end helloworld diff --git a/Examples/MirrorForge/Client.lean b/Examples/MirrorForge/Client.lean index 42de7de..001d0e6 100644 --- a/Examples/MirrorForge/Client.lean +++ b/Examples/MirrorForge/Client.lean @@ -25,6 +25,26 @@ private def containsService (services : Array String) (name : String) : Bool := if s == name then return true return false +/-- Dial options: h2c by default; set `TLS_CA` (+ optional client `TLS_CERT`/`TLS_KEY`) for TLS/mTLS. -/ +private def dialOptions : IO Grpc.Credentials.DialOptions := do + match ← IO.getEnv "TLS_CA" with + | none => pure {} + | some ca => + let cert := (← IO.getEnv "TLS_CERT").getD "" + let key := (← IO.getEnv "TLS_KEY").getD "" + let serverName := (← IO.getEnv "TLS_SERVER_NAME").getD "127.0.0.1" + let tls : Grpc.Tls.Config := { + caPath := some (System.FilePath.mk ca) + serverName := some serverName + certPath := if cert.isEmpty then none else some (System.FilePath.mk cert) + keyPath := if key.isEmpty then none else some (System.FilePath.mk key) + } + pure { channel := .tls tls } + +/-- Preferred Stamp credentials: Bearer metadata (body token still sent for h2c fallback demos). -/ +private def stampAuthMd : Grpc.Metadata := + Grpc.Interceptor.bearerMetadata accessToken + def main (args : List String) : IO UInt32 := do let host := args[0]?.getD "127.0.0.1" let portA := (args[1]?.getD "50201").toNat?.getD 50201 |>.toUInt16 @@ -41,17 +61,20 @@ def main (args : List String) : IO UInt32 := do if hedgeCfg.hedging.isSome then pass "act.hedge_config" "parsed" else fail "act.hedge_config" "missing hedgingPolicy") + let opts ← dialOptions IO.println "mirrorForge: dialing…" - let chRR ← Grpc.Channel.dial s!"dns:///{host}:{portA.toNat}" {} rrCfg - let chRetry ← Grpc.Channel.dial s!"{host}:{portA.toNat}" {} retryCfg + let chRR ← Grpc.Channel.dial s!"dns:///{host}:{portA.toNat}" opts rrCfg + let chRetry ← Grpc.Channel.dial s!"{host}:{portA.toNat}" opts retryCfg IO.println "mirrorForge: dialed" - -- Act I: interceptor-wrapped Stamp + -- Act I: interceptor-wrapped Stamp (Bearer metadata + body token) let clientLog ← IO.mkRef (#[] : Array String) let stampReq := StampRequest.encode { token := accessToken, billet := "ingot-1" } IO.println "mirrorForge: stamp_1…" - let stamp1 ← Grpc.Interceptor.callUnary chRR serviceName "Stamp" - #[Grpc.Interceptor.loggingClient clientLog] stampReq + let stampInvoker : Grpc.Interceptor.ClientUnaryInvoker := fun r => + Grpc.Channel.unary chRR serviceName "Stamp" r stampAuthMd + let stamp1 ← Grpc.Interceptor.applyClient serviceName "Stamp" + #[Grpc.Interceptor.loggingClient clientLog] stampInvoker stampReq IO.println s!"mirrorForge: stamp_1 status={stamp1.status.code.toUInt32}" checks := checks.push (expectOk "act.stamp_1" stamp1.status.code) let reply1 ← IO.ofExcept (StampReply.decode stamp1.message) @@ -67,7 +90,7 @@ def main (args : List String) : IO UInt32 := do -- Act II: round-robin across two forges let stamp2 ← Grpc.Channel.unary chRR serviceName "Stamp" - (StampRequest.encode { token := accessToken, billet := "ingot-2" }) + (StampRequest.encode { token := accessToken, billet := "ingot-2" }) stampAuthMd checks := checks.push (expectOk "act.stamp_2" stamp2.status.code) let reply2 ← IO.ofExcept (StampReply.decode stamp2.message) checks := checks.push ( @@ -76,7 +99,7 @@ def main (args : List String) : IO UInt32 := do else fail "act.round_robin" s!"both hit {reply1.forgeId} (is the second forge up?)") - -- Act III: bad token → UNAUTHENTICATED + -- Act III: bad token → UNAUTHENTICATED (no Bearer, wrong body token) let bad ← Grpc.Channel.unary chRR serviceName "Stamp" (StampRequest.encode { token := "nope", billet := "x" }) checks := checks.push ( @@ -121,7 +144,7 @@ def main (args : List String) : IO UInt32 := do -- Act VIII: Binary log let sink ← Grpc.BinaryLog.newSink let logged ← Grpc.BinaryLog.logUnaryCall sink 7 chRR serviceName "Stamp" - (StampRequest.encode { token := accessToken, billet := "logged" }) + (StampRequest.encode { token := accessToken, billet := "logged" }) stampAuthMd checks := checks.push (expectOk "act.binlog.call" logged.status.code) let ev ← Grpc.BinaryLog.events sink checks := checks.push ( @@ -149,7 +172,7 @@ def main (args : List String) : IO UInt32 := do -- Act XI: SlowStamp (plain unary; hedging races use background tasks that can -- keep the process alive, so we only assert the config parse + a slow RPC OK). let slow ← Grpc.Channel.unary chRetry serviceName "SlowStamp" - (StampRequest.encode { token := accessToken, billet := "anneal" }) + (StampRequest.encode { token := accessToken, billet := "anneal" }) stampAuthMd checks := checks.push (expectOk "act.slow_stamp" slow.status.code) let mut failed : Nat := 0 diff --git a/Examples/MirrorForge/README.md b/Examples/MirrorForge/README.md index b1aaed5..8b2ef49 100644 --- a/Examples/MirrorForge/README.md +++ b/Examples/MirrorForge/README.md @@ -8,9 +8,9 @@ Two forge processes (`alpha` / `beta`) sit behind a round-robin channel. The cli | Act | What it exercises | |---|---| -| Stamp ×2 + interceptor | Unary + client logging interceptor + forge mark | +| Stamp ×2 + interceptor | Unary + client logging interceptor + forge mark; **Bearer metadata** (body token fallback) via `registerUnaryWithContext` | | Round-robin | `LEAN_GRPC_RESOLVE_ADDRS` + `loadBalancingPolicy=round_robin` → different `forgeId`s | -| Auth reject | Body token gate → `UNAUTHENTICATED` | +| Auth reject | Missing/wrong credentials → `UNAUTHENTICATED` | | Quench + retry | First `UNAVAILABLE`, client `retryPolicy` recovers | | Health Check/Watch | Standard health service | | Reflection v1alpha + v1 | `list_services` includes forge + health | @@ -27,3 +27,20 @@ Two forge processes (`alpha` / `beta`) sit behind a round-robin channel. The cli ``` Exit `0` = all checks passed. + +## Optional TLS / mTLS + +Default listen is h2c. To exercise 1.1.0 peer identity: + +```bash +# Server (each forge): +TLS_CERT=certs/server.crt TLS_KEY=certs/server.key TLS_CLIENT_CA=certs/ca.crt \ + FORGE_ID=alpha GRPC_PORT=50201 ./.lake/build/bin/mirrorForgeServer + +# Client: +TLS_CA=certs/ca.crt TLS_CERT=certs/client.crt TLS_KEY=certs/client.key \ + TLS_SERVER_NAME=127.0.0.1 \ + ./.lake/build/bin/mirrorForgeClient 127.0.0.1 50201 50202 +``` + +With `TLS_CLIENT_CA` set, Stamp runs `requirePeerIdentity` and embeds the peer CN in the stamp mark (`{forgeId}:{cn}:{billet}`). diff --git a/Examples/MirrorForge/Server.lean b/Examples/MirrorForge/Server.lean index e40bdab..7481302 100644 --- a/Examples/MirrorForge/Server.lean +++ b/Examples/MirrorForge/Server.lean @@ -7,7 +7,22 @@ import Examples.MirrorForge.Protocol open Examples.MirrorForge.Protocol -/-- One forge mirror. Set `FORGE_ID` / `GRPC_PORT` (defaults: alpha / 50201). -/ +/-- Accept forge credentials from Bearer metadata **or** body `token` (fallback for + existing h2c MirrorForge clients). Under mTLS, `requirePeerIdentity` may also + sit on the interceptor chain. -/ +private def authorized (ctx : Grpc.ServerCallContext) (bodyToken : String) : Bool := + match ctx.metadata.get? "authorization" with + | some auth => + auth == s!"Bearer {accessToken}" || bodyToken == accessToken + | none => + bodyToken == accessToken + +/-- One forge mirror. Set `FORGE_ID` / `GRPC_PORT` (defaults: alpha / 50201). + + TLS (optional): + * `TLS_CERT` / `TLS_KEY` — serve with in-process TLS+ALPN `h2` + * `TLS_CLIENT_CA` — require and verify client certs (mTLS); Stamp uses + `requirePeerIdentity` and embeds peer CN in the stamp mark when present -/ def main : IO Unit := do let port := ((← IO.getEnv "GRPC_PORT").getD "50201").toNat?.getD 50201 |>.toUInt16 let forgeId := (← IO.getEnv "FORGE_ID").getD "alpha" @@ -22,25 +37,39 @@ def main : IO Unit := do let flakyLeft ← IO.mkRef (1 : Nat) -- first Quench fails with UNAVAILABLE let logSink ← IO.mkRef (#[] : Array String) - let chain : Array Grpc.Interceptor.ServerUnary := #[ - Grpc.Interceptor.loggingServer logSink - ] + let cert := (← IO.getEnv "TLS_CERT").getD "" + let key := (← IO.getEnv "TLS_KEY").getD "" + let clientCa ← IO.getEnv "TLS_CLIENT_CA" + let useTls := !cert.isEmpty && !key.isEmpty + let mtls := useTls && clientCa.isSome + + let mut chain : Array Grpc.Interceptor.ServerUnaryWithContext := + #[Grpc.Interceptor.loggingServerWithContext logSink] + if mtls then + chain := chain.push Grpc.Interceptor.requirePeerIdentity let mut s := Grpc.Server.empty - -- Stamp: token-gated unary through interceptor chain - s := Grpc.Interceptor.registerUnary s serviceName "Stamp" chain fun reqBytes => do + -- Stamp: context-aware unary (Bearer metadata preferred; body token fallback) + s := Grpc.Interceptor.registerUnaryWithContext s serviceName "Stamp" chain fun ctx reqBytes => do let req ← IO.ofExcept (StampRequest.decode reqBytes) - if req.token != accessToken then + if !(authorized ctx req.token) then Grpc.Channelz.recordFailure counters return (ByteArray.empty, Grpc.Status.unauthenticated "bad forge token") if req.billet.isEmpty then Grpc.Channelz.recordFailure counters return (ByteArray.empty, Grpc.Status.invalidArgument "empty billet") let report ← orcaRef.get + let peerCn := + match ctx.peerIdentity with + | some id => id.commonName + | none => "" + let mark := + if peerCn.isEmpty then s!"{forgeId}:{req.billet}" + else s!"{forgeId}:{peerCn}:{req.billet}" let reply := StampReply.encode { forgeId - mark := s!"{forgeId}:{req.billet}" + mark cpuLoad := report.cpuUtilization } Grpc.Channelz.recordSuccess counters @@ -79,5 +108,15 @@ def main : IO Unit := do s := Grpc.Channelz.register s counters | _ => pure () - IO.println s!"MirrorForge[{forgeId}] on 127.0.0.1:{port.toNat}" - Grpc.Server.serveH2c s { host := "127.0.0.1", port } + if useTls then + let tlsCfg : Grpc.Tls.Config := { + certPath := some (System.FilePath.mk cert) + keyPath := some (System.FilePath.mk key) + clientCaPath := clientCa.map System.FilePath.mk + } + let mtlsNote := if mtls then " (mTLS)" else "" + IO.println s!"MirrorForge[{forgeId}] TLS+ALPN on 127.0.0.1:{port.toNat}{mtlsNote}" + Grpc.Server.serveTls s tlsCfg { host := "127.0.0.1", port } + else + IO.println s!"MirrorForge[{forgeId}] on 127.0.0.1:{port.toNat}" + Grpc.Server.serveH2c s { host := "127.0.0.1", port } diff --git a/Grpc.lean b/Grpc.lean index e34ec3c..adbfd34 100644 --- a/Grpc.lean +++ b/Grpc.lean @@ -11,6 +11,7 @@ import Grpc.StatusDetails import Grpc.Compression import Grpc.Message import Grpc.Metadata +import Grpc.PeerIdentity import Grpc.Server import Grpc.Client import Grpc.Stream @@ -38,5 +39,5 @@ import Grpc.Grpclb import Grpc.Interceptor namespace Grpc -def version : String := "1.0.0" +def version : String := "1.1.0" end Grpc diff --git a/Grpc/Codegen/Emit.lean b/Grpc/Codegen/Emit.lean index 1479998..f02758f 100644 --- a/Grpc/Codegen/Emit.lean +++ b/Grpc/Codegen/Emit.lean @@ -450,6 +450,11 @@ def emitServiceTyped (pkg : String) (svc : ServiceDescriptor) : Except String St out := out ++ " | .ok req =>\n" out := out ++ " let (resp, st) ← h req\n" out := out ++ s!" return ({respTy}.encode resp, st)\n\n" + out := out ++ s!"/-- Register a typed unary handler with `ServerCallContext` for `{svc.name}/{m.name}`. -/\n" + out := out ++ s!"def register{svc.name}{m.name}WithContext (s : Grpc.Server)\n" + out := out ++ s!" (h : Grpc.ServerCallContext → {reqTy} → IO ({respTy} × Grpc.Status)) : Grpc.Server :=\n" + out := out ++ s!" Grpc.Server.registerTypedWithContext s \"{full}\" \"{m.name}\"\n" + out := out ++ s!" {reqTy}.decode {respTy}.encode h\n\n" return out /-- Emit one `.lean` file's worth of message structs + typed client/server code for a single diff --git a/Grpc/Interceptor.lean b/Grpc/Interceptor.lean index cbfce8d..5504cc0 100644 --- a/Grpc/Interceptor.lean +++ b/Grpc/Interceptor.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. -/ import Grpc.Server import Grpc.Channel +import Grpc.PeerIdentity /-! # Client/server interceptor chains for unary calls. @@ -27,6 +28,27 @@ def registerUnary (s : Server) (service method : String) (chain : Array ServerUn (h : UnaryHandler) : Server := Server.register s service method (applyServer service method chain h) +/-- Context-aware server unary interceptor. -/ +abbrev ServerUnaryWithContext := + String → String → UnaryHandlerWithContext → UnaryHandlerWithContext + +/-- Fold a chain of context-aware server interceptors around `base`, outermost-first. -/ +def applyServerWithContext (service method : String) (chain : Array ServerUnaryWithContext) + (base : UnaryHandlerWithContext) : UnaryHandlerWithContext := + chain.foldr (fun mw next => mw service method next) base + +/-- Register a context-aware unary method wrapped with `chain`. -/ +def registerUnaryWithContext (s : Server) (service method : String) + (chain : Array ServerUnaryWithContext) (h : UnaryHandlerWithContext) : Server := + Server.registerWithContext s service method (applyServerWithContext service method chain h) + +/-- Fail closed under mTLS: when `ctx.mtlsRequired` and `peerIdentity` is missing, return + `UNAUTHENTICATED` instead of invoking `next`. -/ +def requirePeerIdentity : ServerUnaryWithContext := fun _service _method next ctx req => do + if ctx.mtlsRequired && ctx.peerIdentity.isNone then + return (ByteArray.empty, Status.unauthenticated "mtls_required") + next ctx req + /-- Client-side unary invoker: request bytes → `CallResult` (matches `Channel.unary`'s core shape, modulo the extra dialing options `Channel.unary` takes). -/ abbrev ClientUnaryInvoker := ByteArray → IO CallResult @@ -54,6 +76,18 @@ def loggingServer (sink : IO.Ref (Array String)) : ServerUnary := fun service me sink.modify (·.push s!"< {service}/{method} resp={resp.size}B status={st.code.toUInt32}") return (resp, st) +/-- Context-aware variant of `loggingServer` (logs peer CN when present). -/ +def loggingServerWithContext (sink : IO.Ref (Array String)) : ServerUnaryWithContext := + fun service method next ctx req => do + let peer := + match ctx.peerIdentity with + | some id => id.commonName + | none => "-" + sink.modify (·.push s!"> {service}/{method} req={req.size}B peer={peer}") + let (resp, st) ← next ctx req + sink.modify (·.push s!"< {service}/{method} resp={resp.size}B status={st.code.toUInt32}") + return (resp, st) + /-- Ready-made client interceptor: same as `loggingServer`, mirrored for the call site. -/ def loggingClient (sink : IO.Ref (Array String)) : ClientUnary := fun service method next req => do sink.modify (·.push s!"> {service}/{method} req={req.size}B") diff --git a/Grpc/Metadata.lean b/Grpc/Metadata.lean index 0550099..c18cf2c 100644 --- a/Grpc/Metadata.lean +++ b/Grpc/Metadata.lean @@ -159,7 +159,7 @@ def methodGet : Hpack.HeaderField := ⟨ascii ":method", ascii "GET"⟩ def schemeHttp : Hpack.HeaderField := ⟨ascii ":scheme", ascii "http"⟩ def schemeHttps : Hpack.HeaderField := ⟨ascii ":scheme", ascii "https"⟩ def teTrailers : Hpack.HeaderField := ⟨ascii "te", ascii "trailers"⟩ -def userAgent (version : String := "1.0.0") : Hpack.HeaderField := +def userAgent (version : String := "1.1.0") : Hpack.HeaderField := ⟨ascii "user-agent", ascii s!"grpc-lean/{version}"⟩ def http415 : Array Hpack.HeaderField := diff --git a/Grpc/Native/Tls.lean b/Grpc/Native/Tls.lean index 7a087d8..ad03755 100644 --- a/Grpc/Native/Tls.lean +++ b/Grpc/Native/Tls.lean @@ -3,6 +3,7 @@ Copyright © 2026, Riley Betts Ltd (rileybetts.ai) Released under Apache 2.0 license as described in the file LICENSE. -/ import H2.Transport +import Grpc.PeerIdentity namespace Grpc.Native.Tls @@ -44,6 +45,11 @@ opaque recv (c : @& Conn) (maxBytes : @& Nat) : IO (Option ByteArray) @[extern "lean_grpc_tls_close"] opaque close (c : @& Conn) : IO Unit +/-- Extract verified peer certificate identity after a TLS(/mTLS) handshake. + Returns `none` when the peer presented no certificate. -/ +@[extern "lean_grpc_tls_peer_identity"] +opaque peerIdentity? (c : @& Conn) : IO (Option PeerIdentity) + /-- ByteTransport over an in-process TLS connection. -/ def transport (c : Conn) : H2.ByteTransport where send := fun b => send c b diff --git a/Grpc/PeerIdentity.lean b/Grpc/PeerIdentity.lean new file mode 100644 index 0000000..ca53c9b --- /dev/null +++ b/Grpc/PeerIdentity.lean @@ -0,0 +1,37 @@ +/- +Copyright © 2026, Riley Betts Ltd (rileybetts.ai) +Released under Apache 2.0 license as described in the file LICENSE. +-/ +import Grpc.Metadata + +namespace Grpc + +/-- Verified TLS peer certificate identity. + Fields come **only** from the peer cert on the TLS connection (via OpenSSL), + never from client-supplied gRPC metadata. + + `subjectDn` uses OpenSSL RFC 2253 one-line form (`XN_FLAG_RFC2253`). -/ +structure PeerIdentity where + subjectDn : String + commonName : String + dnsSans : Array String + uriSans : Array String + fingerprintSha256 : String + serial : String := "" + deriving Inhabited, Repr + +/-- Per-RPC server context for unary handlers registered with `registerWithContext`. + + * `peerIdentity` — `some` after mTLS when a client cert was presented and verified; + `none` on h2c, TLS without client cert, or when no peer cert is available. + * `metadata` — inbound request headers (HTTP/2 lowercased names; excludes `:pseudo`). + * `methodPath` — e.g. `/svc/Method`. + * `mtlsRequired` — `true` when the listener was configured with `clientCaPath`. -/ +structure ServerCallContext where + peerIdentity : Option PeerIdentity := none + metadata : Metadata := {} + methodPath : String := "" + mtlsRequired : Bool := false + deriving Inhabited + +end Grpc diff --git a/Grpc/Server.lean b/Grpc/Server.lean index f4429e1..a6a6799 100644 --- a/Grpc/Server.lean +++ b/Grpc/Server.lean @@ -10,6 +10,7 @@ import Proto import Grpc.Status import Grpc.Message import Grpc.Metadata +import Grpc.PeerIdentity import Grpc.Stream import Grpc.Compression import Grpc.Tls @@ -19,8 +20,11 @@ namespace Grpc /-- Unary handler: request bytes → response bytes + status. -/ abbrev UnaryHandler := ByteArray → IO (ByteArray × Status) +/-- Unary handler with per-RPC `ServerCallContext` (peer identity + inbound metadata). -/ +abbrev UnaryHandlerWithContext := ServerCallContext → ByteArray → IO (ByteArray × Status) + inductive MethodHandler where - | unary (h : UnaryHandler) + | unary (h : UnaryHandlerWithContext) | serverStream (h : Stream.ServerStreamHandler) | clientStream (h : Stream.ClientStreamHandler) | bidi (h : Stream.BidiStreamHandler) @@ -39,9 +43,14 @@ namespace Server def empty : Server := ⟨#[], 4 * 1024 * 1024⟩ -def register (s : Server) (service method : String) (h : UnaryHandler) : Server := +/-- Register a unary method that receives `ServerCallContext` (mTLS peer identity + metadata). -/ +def registerWithContext (s : Server) (service method : String) (h : UnaryHandlerWithContext) : Server := { s with methods := s.methods.push ⟨service, method, .unary h⟩ } +/-- Body-only unary register (ignores context). Prefer `registerWithContext` for AuthN. -/ +def register (s : Server) (service method : String) (h : UnaryHandler) : Server := + registerWithContext s service method (fun _ctx req => h req) + def registerServerStream (s : Server) (service method : String) (h : Stream.ServerStreamHandler) : Server := { s with methods := s.methods.push ⟨service, method, .serverStream h⟩ } @@ -62,6 +71,17 @@ def registerTyped (s : Server) (service method : String) let (resp, st) ← h req return (encode resp, st) +/-- Typed unary register with `ServerCallContext`. -/ +def registerTypedWithContext (s : Server) (service method : String) + (decode : ByteArray → Except String α) (encode : β → ByteArray) + (h : ServerCallContext → α → IO (β × Status)) : Server := + registerWithContext s service method fun ctx reqBytes => do + match decode reqBytes with + | .error e => return (ByteArray.empty, Status.invalidArgument e) + | .ok req => + let (resp, st) ← h ctx req + return (encode resp, st) + /-- Typed server-streaming register (still batch: one request → array of responses). -/ def registerServerStreamTyped (s : Server) (service method : String) (decode : ByteArray → Except String α) (encode : β → ByteArray) @@ -110,6 +130,16 @@ private def headerAscii (h : Hpack.HeaderField) : String × String := (String.ofList (h.name.toList.map (fun b => Char.ofNat b.toNat)), String.ofList (h.value.toList.map (fun b => Char.ofNat b.toNat))) +/-- Collect non-pseudo request headers into `Metadata` (HTTP/2 names are lowercased). -/ +private def metadataFromHeaders (headers : Array Hpack.HeaderField) : Metadata := + Id.run do + let mut m := Metadata.empty + for h in headers do + let (n, v) := headerAscii h + if !n.startsWith ":" then + m := m.add n v + return m + /-- Deprecated alias — use `Metadata.parseTimeoutMs`. -/ def parseTimeoutMs (t : String) : Option Nat := Metadata.parseTimeoutMs t @@ -119,9 +149,11 @@ private def encodeManyIO (msgs : Array ByteArray) (alg : Compression.Algorithm) out := Bytes.Pool.pushBytes out (← Message.encodeIO m alg) return out -/-- Build the transport-agnostic `H2.StreamHandler` for `s`, shared by the - plaintext (`serveH2c`) and TLS (`serveTls`) entry points below. -/ -def handlerFor (s : Server) : H2.StreamHandler := fun _streamId headers data endStream headersSent => do +/-- Build the transport-agnostic `H2.StreamHandler` for `s`. + `peerIdentity` is connection-scoped (from mTLS); `mtlsRequired` is true when + the listener was configured with `clientCaPath`. -/ +def handlerFor (s : Server) (peerIdentity : Option PeerIdentity := none) + (mtlsRequired : Bool := false) : H2.StreamHandler := fun _streamId headers data endStream headersSent => do if headersSent && !endStream && data.isEmpty then return { finished := false } -- Resolve path early so incremental bidi can respond before half-close. @@ -202,10 +234,16 @@ def handlerFor (s : Server) : H2.StreamHandler := fun _streamId headers data end let mut respHeaders := Metadata.http200 if respAlg != .identity then respHeaders := respHeaders.push (Metadata.grpcEncoding respAlg.name) + let ctx : ServerCallContext := { + peerIdentity + metadata := metadataFromHeaders headers + methodPath := path + mtlsRequired + } match mh with | .unary h => let req := payloads.getD 0 ByteArray.empty - let (resp, st) ← h req + let (resp, st) ← h ctx req let body ← if st.code != .ok && resp.isEmpty then pure ByteArray.empty else Message.encodeIO resp respAlg @@ -265,12 +303,14 @@ def handlerFor (s : Server) : H2.StreamHandler := fun _streamId headers data end } def serveH2c (s : Server) (cfg : H2.ServerConfig := {}) : IO Unit := - H2.Server.listen cfg (handlerFor s) + H2.Server.listen cfg (handlerFor s none false) /-- Serve with in-process TLS+ALPN `h2` (see `Grpc.Tls.serveH2` for the - plaintext/mTLS decision based on `tlsCfg`). -/ + plaintext/mTLS decision based on `tlsCfg`). Peer identity is extracted per + accepted connection and threaded into unary context handlers. -/ def serveTls (s : Server) (tlsCfg : Tls.Config) (cfg : H2.ServerConfig := {}) : IO Unit := - Tls.serveH2 tlsCfg cfg (handlerFor s) + let mtlsRequired := tlsCfg.clientCaPath.isSome + Tls.serveH2 tlsCfg cfg fun peerId => handlerFor s peerId mtlsRequired end Server end Grpc diff --git a/Grpc/Tls.lean b/Grpc/Tls.lean index 57989ff..ad40a6c 100644 --- a/Grpc/Tls.lean +++ b/Grpc/Tls.lean @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. import H2 import Grpc.Resolver import Grpc.Native.Tls +import Grpc.PeerIdentity namespace Grpc.Tls @@ -57,8 +58,13 @@ def connectH2 (host : String) (port : UInt16) (cfg : Config := {}) : IO H2.Clien H2.Client.connectTransport (Grpc.Native.Tls.transport conn) /-- Serve with in-process TLS+ALPN when cert/key are set; otherwise h2c (+ optional sidecar). - TLS listen binds loopback only (see native `INADDR_LOOPBACK`). -/ -partial def serveH2 (cfg : Config) (h2cfg : H2.ServerConfig) (handler : H2.StreamHandler) : IO Unit := do + TLS listen binds loopback only (see native `INADDR_LOOPBACK`). + + `mkHandler` receives the verified peer identity for each accepted connection + (`none` when the client presented no certificate). Failed accepts/handshakes + are logged and the listen loop continues. -/ +partial def serveH2 (cfg : Config) (h2cfg : H2.ServerConfig) + (mkHandler : Option PeerIdentity → H2.StreamHandler) : IO Unit := do match cfg.certPath, cfg.keyPath with | some cert, some key => let clientCa := (cfg.clientCaPath.map (·.toString)).getD "" @@ -66,17 +72,26 @@ partial def serveH2 (cfg : Config) (h2cfg : H2.ServerConfig) (handler : H2.Strea let mtlsNote := if cfg.clientCaPath.isSome then " (mTLS: client cert required)" else "" IO.println s!"H2 TLS+ALPN listening on 127.0.0.1:{h2cfg.port}{mtlsNote}" while true do - let conn ← Grpc.Native.Tls.accept listener - discard <| IO.asTask (prio := .dedicated) do + let acceptResult ← try - H2.serveTransport (Grpc.Native.Tls.transport conn) handler + pure (Sum.inl (← Grpc.Native.Tls.accept listener)) catch e => - IO.eprintln s!"tls conn error: {e}" + pure (Sum.inr e) + match acceptResult with + | .inr e => + IO.eprintln s!"tls accept error: {e}" + | .inl conn => + let peerId ← Grpc.Native.Tls.peerIdentity? conn + discard <| IO.asTask (prio := .dedicated) do + try + H2.serveTransport (Grpc.Native.Tls.transport conn) (mkHandler peerId) + catch e => + IO.eprintln s!"tls conn error: {e}" | _, _ => match ← IO.getEnv "LEAN_GRPC_TLS_INSECURE_FALLBACK" with - | some "1" => H2.Server.listen h2cfg handler + | some "1" => H2.Server.listen h2cfg (mkHandler none) | _ => IO.eprintln s!"Tls.serveH2: serving h2c on {h2cfg.host}:{h2cfg.port}; set certPath/keyPath for in-process TLS, or use sidecar. {envoySidecarNotes}" - H2.Server.listen h2cfg handler + H2.Server.listen h2cfg (mkHandler none) end Grpc.Tls diff --git a/README.md b/README.md index b88876d..d4cc1c0 100644 --- a/README.md +++ b/README.md @@ -6,7 +6,7 @@ General-purpose **Lean 4 gRPC library**: HPACK + HTTP/2 + gRPC framing on `Std.Async.TCP`. -Standalone Lake package (**1.0.0**). Consumers depend via git tag or, after indexing, [Reservoir](https://reservoir.lean-lang.org/). +Standalone Lake package (**1.1.0**). Consumers depend via git tag or, after indexing, [Reservoir](https://reservoir.lean-lang.org/). **Docs:** [rileybetts.ai/oss/lean-grpc](https://rileybetts.ai/oss/lean-grpc) (curated) · [docs/](docs/README.md) (full in-repo index) @@ -20,7 +20,7 @@ In your `lakefile.lean`: ```lean require «lean-grpc» from git - "https://github.com/RileyBetts/lean-grpc.git" @ "v1.0.0" + "https://github.com/RileyBetts/lean-grpc.git" @ "v1.1.0" ``` Then `import Grpc`. After Reservoir lists the package you can use `require «lean-grpc»` without a git URL. Packaging details and the maintainer release checklist: [docs/packaging.md](docs/packaging.md). @@ -42,7 +42,7 @@ Then `import Grpc`. After Reservoir lists the package you can use `require «lea | [Formal proofs](docs/proofs.md) | Compile-time theorems for pure codecs | | [TLS / Envoy](docs/tls-envoy.md) | In-process OpenSSL and sidecars | | [CHANGELOG](CHANGELOG.md) | Version history | -| [ROADMAP](ROADMAP.md) | What v1.0.0 shipped vs open proof/hardening follow-ups | +| [ROADMAP](ROADMAP.md) | What v1.1.0 shipped vs open proof/hardening follow-ups | | [CONTRIBUTING](CONTRIBUTING.md) | Dev setup and PR expectations | | [SECURITY](SECURITY.md) | Vulnerability reporting (`security@rileybetts.ai`) | | [Code of Conduct](CODE_OF_CONDUCT.md) | Community standards | diff --git a/ROADMAP.md b/ROADMAP.md index bef21cd..d108469 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -1,6 +1,6 @@ # Roadmap -lean-grpc **v1.0.0** is the current package tip (Lake / `Grpc.version`, git tag `v1.0.0`): an interop-tested Lean 4 gRPC stack with a CI-gated **`Proofs`** library for selected pure codecs. It is **not** a machine-checked end-to-end PROTOCOL-HTTP2 / TLS / session proof, and it does **not** yet meet every item that earlier drafts listed under “v1.0.0 complete.” +lean-grpc **v1.1.0** is the current package tip (Lake / `Grpc.version`): an interop-tested Lean 4 gRPC stack with a CI-gated **`Proofs`** library for selected pure codecs, plus additive mTLS peer-identity / request-context APIs for enterprise AuthN. It is **not** a machine-checked end-to-end PROTOCOL-HTTP2 / TLS / session proof. This document records what shipped, what is still open, and the next proof/hardening tranches. @@ -25,6 +25,17 @@ First public packaging baseline (interop + Lake/Reservoir layout). Formal Lean p | Dial / LB / retry, health, reflection, channelz | Present; ops demos gated | | ADC / xDS ADS | Mock / FakeAds CI; live Google paths allowlisted | +## Shipped — v1.1.0 (IAM) + +Additive server AuthN plumbing for verified mTLS peer identity (see [feature/lean-grpc-iam-requirements.md](feature/lean-grpc-iam-requirements.md), [docs/cookbook-interceptors.md](docs/cookbook-interceptors.md)). + +| Included | Deferred | +|---|---| +| Native peer cert extract (DN/CN/SANs/fingerprint) | Streaming handlers with `ServerCallContext` | +| `registerWithContext` / `ServerCallContext` | Trusted-proxy identity mode | +| Dual-cert + metadata non-forgery loopback tests | JWT/OIDC validation inside lean-grpc | +| Accept-loop continues after failed TLS handshake | Full SPIFFE/SPIRE workload API | + ## Shipped — v1.0.0 (honest scope) Product/packaging release with **selected** compile-time proofs. See [docs/proofs.md](docs/proofs.md). @@ -40,7 +51,7 @@ Product/packaging release with **selected** compile-time proofs. See [docs/proof **Explicit non-goals (unchanged):** ALTS / GCE channel credentials, HTTP CONNECT proxying, full `cacheable_unary` proxy infrastructure, end-to-end session proofs. -## Toward v1.1.x / later +## Toward v1.2.x / later Work is grouped so each tranche can ship as a minor release without waiting for a full ConnState + Huffman proof stack. @@ -75,6 +86,7 @@ Close remaining audit follow-ups so later minors are not “proved but soft”: - Keep README / SECURITY honesty: “executable + interop CI + *selected* Lean proofs; FFI trusted” - Reservoir indexing polish ([docs/packaging.md](docs/packaging.md); hosted docs at [rileybetts.ai/oss/lean-grpc](https://rileybetts.ai/oss/lean-grpc)) - Allowlists remain unless separately delivered (ALTS, live ADC, CONNECT) +- Streaming `ServerCallContext` (parity with unary IAM) ### D — Nice-to-have (not blockers) @@ -87,24 +99,25 @@ Close remaining audit follow-ups so later minors are not “proved but soft”: ## Milestone sketch ```text -v0.5.0 ──► v1.0.0 ──► v1.1.x ──► v1.2.x - shipped interop + ConnState + Huffman trie / - selected Proofs general frame/msg bootstrap JSON / - (CI) + provenance roundtrips fuzz seeds - (fixtures → ∀) +v0.5.0 ──► v1.0.0 ──► v1.1.0 ──► v1.2.x + shipped interop + mTLS peer identity + ConnState + + selected Proofs ServerCallContext general frame/msg + (CI) + provenance (unary IAM) roundtrips / + Huffman trie ``` Dates are intentionally omitted; order matters more than calendar. ## What versions mean -| Claim | v1.0.0 | Later 1.x target | -|---|---|---| -| Interop-tested general-purpose gRPC over h2c/TLS | **Yes** | Maintain | -| Selected critical pure codecs machine-checked in Lean | **Yes** (partial; see [docs/proofs.md](docs/proofs.md)) | Broaden ∀ coverage | -| `H2.ConnState` properties machine-checked | **No** | Yes (P1) | -| Full PROTOCOL-HTTP2 / gRPC / TLS stack proved | **No** | **No** (non-goal) | -| ALTS / live Google control plane | **No** (allowlisted) | Unless separately delivered | +| Claim | v1.0.0 | v1.1.0 | Later 1.x target | +|---|---|---|---| +| Interop-tested general-purpose gRPC over h2c/TLS | **Yes** | Maintain | Maintain | +| mTLS verified peer identity in unary handlers | **No** | **Yes** | Streaming context | +| Selected critical pure codecs machine-checked in Lean | **Yes** (partial; see [docs/proofs.md](docs/proofs.md)) | Maintain | Broaden ∀ coverage | +| `H2.ConnState` properties machine-checked | **No** | **No** | Yes (P1) | +| Full PROTOCOL-HTTP2 / gRPC / TLS stack proved | **No** | **No** | **No** (non-goal) | +| ALTS / live Google control plane | **No** (allowlisted) | **No** | Unless separately delivered | ## How to contribute diff --git a/SECURITY.md b/SECURITY.md index 801fac5..420cea9 100644 --- a/SECURITY.md +++ b/SECURITY.md @@ -4,7 +4,7 @@ Security fixes are applied to the published tip (`main` / `development` as released). There is no long-term LTS train yet. -**Supported version:** the latest **tagged** release (e.g. `v1.0.0`). Maintainers create tags manually — see [docs/packaging.md](docs/packaging.md). Prefer GitHub Security Advisories for private reports when enabled. +**Supported version:** the latest **tagged** release (e.g. `v1.1.0`). Maintainers create tags manually — see [docs/packaging.md](docs/packaging.md). Prefer GitHub Security Advisories for private reports when enabled. ## Reporting a vulnerability @@ -20,9 +20,9 @@ You may also open a private [GitHub Security Advisory](https://github.com/RileyB | Area | Notes | |---|---| -| TLS / mTLS | OpenSSL via `native/tls_ffi.c`; empty `caPath` uses the **system trust store** + hostname verify. Set `Tls.Config.insecureSkipVerify` (stderr WARN) only for fixtures | +| TLS / mTLS | OpenSSL via `native/tls_ffi.c`; empty `caPath` uses the **system trust store** + hostname verify. Set `Tls.Config.insecureSkipVerify` (stderr WARN) only for fixtures. With `clientCaPath`, verified peer identity is exposed via `ServerCallContext.peerIdentity` (RFC 2253 DN / SANs) — trust equals the configured client CA PKI. Do **not** treat client metadata subject headers as AuthN | | ADC token HTTPS | `httpsPost` verifies peer+hostname by default; env redirects / cleartext require `LEAN_GRPC_ALLOW_ADC_OVERRIDE=1` | -| h2c | Cleartext — bind to localhost or mesh-only networks in production | +| h2c | Cleartext — bind to localhost or mesh-only networks in production; `peerIdentity` is always `none` | | `LEAN_GRPC_TLS_INSECURE_FALLBACK=1` | Disables TLS — never in production | | Other env overrides | `LEAN_GRPC_TOKEN_*`, `LEAN_GRPC_GCE_METADATA`, `LEAN_GRPC_RESOLVE_ADDRS` (+ `ALLOW_*`), `LEAN_GRPC_XDS_INSECURE`, `LEAN_GRPC_ZLIB_HELPER` — admin/test-only | | Compression | Decompressed size capped by `maxMsgSize` (default 4 MiB) in Message/Server paths and native zlib `max_out` | diff --git a/Tests/TlsLoopback.lean b/Tests/TlsLoopback.lean index 81128f4..838d95d 100644 --- a/Tests/TlsLoopback.lean +++ b/Tests/TlsLoopback.lean @@ -5,15 +5,17 @@ Released under Apache 2.0 license as described in the file LICENSE. import Grpc import Proto -/-- In-process TLS + mTLS loopback: spawns `tlsServer` (see `Tests/TlsServer.lean`) - with a self-signed CA/server/client cert chain generated on the fly via the - system `openssl` CLI, then verifies: +/-- In-process TLS + mTLS + IAM identity loopback: spawns `tlsServer` with a + self-signed CA/server/client cert chain generated via `openssl`, then verifies: 1. Plain TLS (server cert only) succeeds without a client cert. 2. mTLS (server requires a client cert) rejects a client that presents none. - 3. mTLS succeeds when the client presents a certificate signed by the - configured client CA. - Skips (prints a note and exits 0) if `openssl` is unavailable, since some - sandboxes don't ship it. -/ + 3. mTLS succeeds when the client presents a certificate signed by the CA; + handler observes `peerIdentity.commonName` / URI SAN. + 4. Two different client certs → two different peer identities. + 5. Attacker metadata `x-client-subject` does not forge `peerIdentity`. + 6. h2c → `peerIdentity = none`. + 7. Failed handshake against mTLS listener does not kill the accept loop. + Skips (exit 0) if `openssl` is unavailable. -/ private def run (cmd : String) (args : Array String) : IO Unit := do let out ← IO.Process.output { cmd, args } @@ -26,6 +28,10 @@ private def haveOpenssl : IO Bool := do return out.exitCode == 0 catch _ => return false +private def writeFile (path : System.FilePath) (contents : String) : IO Unit := + IO.FS.writeFile path contents + +/-- Generate CA, server, and two distinct client certs (CN + URI SAN). -/ private def genCerts (dir : System.FilePath) : IO Unit := do IO.FS.createDirAll dir let d := dir.toString @@ -38,38 +44,78 @@ private def genCerts (dir : System.FilePath) : IO Unit := do run "openssl" #["x509", "-req", "-in", s!"{d}/server.csr", "-CA", s!"{d}/ca.crt", "-CAkey", s!"{d}/ca.key", "-CAcreateserial", "-out", s!"{d}/server.crt", "-days", "825", "-sha256"] - run "openssl" #["genrsa", "-out", s!"{d}/client.key", "2048"] - run "openssl" #["req", "-new", "-key", s!"{d}/client.key", "-out", s!"{d}/client.csr", - "-subj", "/CN=lean-grpc-test-client"] - run "openssl" #["x509", "-req", "-in", s!"{d}/client.csr", "-CA", s!"{d}/ca.crt", - "-CAkey", s!"{d}/ca.key", "-CAcreateserial", "-out", s!"{d}/client.crt", - "-days", "825", "-sha256"] -private def spawnServer (binDir dir : System.FilePath) (port : UInt16) (requireClientCa : Bool) : - IO (IO.Process.Child {}) := do + -- Client A: CN=oms-desk-a + SPIFFE-shaped URI SAN + writeFile (dir / "client_a_ext.cnf") + "subjectAltName=URI:spiffe://lean-grpc.test/oms-desk-a\n" + run "openssl" #["genrsa", "-out", s!"{d}/client_a.key", "2048"] + run "openssl" #["req", "-new", "-key", s!"{d}/client_a.key", "-out", s!"{d}/client_a.csr", + "-subj", "/CN=oms-desk-a"] + run "openssl" #["x509", "-req", "-in", s!"{d}/client_a.csr", "-CA", s!"{d}/ca.crt", + "-CAkey", s!"{d}/ca.key", "-CAcreateserial", "-out", s!"{d}/client_a.crt", + "-days", "825", "-sha256", "-extfile", s!"{d}/client_a_ext.cnf"] + + -- Client B: CN=admin + different URI SAN + writeFile (dir / "client_b_ext.cnf") + "subjectAltName=URI:spiffe://lean-grpc.test/admin\n" + run "openssl" #["genrsa", "-out", s!"{d}/client_b.key", "2048"] + run "openssl" #["req", "-new", "-key", s!"{d}/client_b.key", "-out", s!"{d}/client_b.csr", + "-subj", "/CN=admin"] + run "openssl" #["x509", "-req", "-in", s!"{d}/client_b.csr", "-CA", s!"{d}/ca.crt", + "-CAkey", s!"{d}/ca.key", "-CAcreateserial", "-out", s!"{d}/client_b.crt", + "-days", "825", "-sha256", "-extfile", s!"{d}/client_b_ext.cnf"] + + -- Backward-compat names used by plain mTLS case + run "cp" #[s!"{d}/client_a.crt", s!"{d}/client.crt"] + run "cp" #[s!"{d}/client_a.key", s!"{d}/client.key"] + +private def spawnServer (binDir dir : System.FilePath) (port : UInt16) + (requireClientCa : Bool) (h2c : Bool := false) : IO (IO.Process.Child {}) := do let d := dir.toString - let env := - #[("GRPC_PORT", some (toString port.toNat)), - ("TLS_CERT", some s!"{d}/server.crt"), - ("TLS_KEY", some s!"{d}/server.key")] ++ - (if requireClientCa then #[("TLS_CLIENT_CA", some s!"{d}/ca.crt")] else #[]) + let mut env : Array (String × Option String) := + #[("GRPC_PORT", some (toString port.toNat))] + if h2c then + env := env.push ("TLS_H2C", some "1") + else + env := env ++ + #[("TLS_CERT", some s!"{d}/server.crt"), + ("TLS_KEY", some s!"{d}/server.key")] + if requireClientCa then + env := env.push ("TLS_CLIENT_CA", some s!"{d}/ca.crt") IO.Process.spawn { cmd := (binDir / "tlsServer").toString, env } -private def emptyCall (port : UInt16) (cfg : Grpc.Tls.Config) : IO Grpc.CallResult := do - let conn ← Grpc.Tls.connectH2 "127.0.0.1" port cfg +private def field (body : String) (key : String) : String := + let keyEq := key ++ "=" + Id.run do + for line in body.splitOn "\n" do + if line.startsWith keyEq then + return (line.drop keyEq.length).toString + return "" + +private def bodyString (res : Grpc.CallResult) : IO String := do + match String.fromUTF8? res.message with + | some s => pure s + | none => throw (IO.userError "identity echo: non-utf8 body") + +private def emptyCall (port : UInt16) (cfg : Grpc.Tls.Config) + (extra : Array Hpack.HeaderField := #[]) (useHttps : Bool := true) : IO Grpc.CallResult := do + let conn ← + if useHttps then + Grpc.Tls.connectH2 "127.0.0.1" port cfg + else + H2.Client.connectH2c "127.0.0.1" port Grpc.Client.unaryCall conn "grpc.testing.TestService" "EmptyCall" "127.0.0.1" ByteArray.empty - (useHttps := true) + extra (useHttps := useHttps) -/-- Retry a dial+call a few times with backoff, tolerating the spawned server not - having bound its listen socket yet on a slow/loaded machine. -/ -private partial def emptyCallRetry (port : UInt16) (cfg : Grpc.Tls.Config) (attempts : Nat := 5) : +private partial def emptyCallRetry (port : UInt16) (cfg : Grpc.Tls.Config) + (extra : Array Hpack.HeaderField := #[]) (useHttps : Bool := true) (attempts : Nat := 8) : IO Grpc.CallResult := do try - emptyCall port cfg + emptyCall port cfg extra useHttps catch e => if attempts ≤ 1 then throw e IO.sleep 300 - emptyCallRetry port cfg (attempts - 1) + emptyCallRetry port cfg extra useHttps (attempts - 1) def main : IO Unit := do if !(← haveOpenssl) then @@ -79,16 +125,20 @@ def main : IO Unit := do genCerts dir let binDir ← IO.appDir let serverName := some "127.0.0.1" + let caPath := some (dir / "ca.crt") -- 1. Plain TLS (server cert only, no client-CA requirement). let port1 : UInt16 := 50061 let srv1 ← spawnServer binDir dir port1 false try IO.sleep 300 - let cfg : Grpc.Tls.Config := { caPath := some (dir / "ca.crt"), serverName } + let cfg : Grpc.Tls.Config := { caPath, serverName } let res ← emptyCallRetry port1 cfg if res.status.code != .ok then throw (IO.userError s!"plain tls status {res.status.code.toUInt32}") + let body ← bodyString res + if field body "peer_none" != "true" then + throw (IO.userError s!"plain tls expected peer_none: {body}") finally srv1.kill @@ -97,7 +147,7 @@ def main : IO Unit := do let srv2 ← spawnServer binDir dir port2 true try IO.sleep 600 - let cfg : Grpc.Tls.Config := { caPath := some (dir / "ca.crt"), serverName } + let cfg : Grpc.Tls.Config := { caPath, serverName } let mut rejected := false try discard <| emptyCall port2 cfg @@ -107,21 +157,93 @@ def main : IO Unit := do finally srv2.kill - -- 3. mTLS required, client presents a cert signed by the trusted CA → succeeds. + -- 3. mTLS + client A → handler observes CN / URI SAN. let port3 : UInt16 := 50063 let srv3 ← spawnServer binDir dir port3 true try IO.sleep 300 - let cfg : Grpc.Tls.Config := { - caPath := some (dir / "ca.crt") - certPath := some (dir / "client.crt") - keyPath := some (dir / "client.key") + let cfgA : Grpc.Tls.Config := { + caPath + certPath := some (dir / "client_a.crt") + keyPath := some (dir / "client_a.key") serverName } - let res ← emptyCallRetry port3 cfg + let res ← emptyCallRetry port3 cfgA if res.status.code != .ok then - throw (IO.userError s!"mtls status {res.status.code.toUInt32}") + throw (IO.userError s!"mtls A status {res.status.code.toUInt32}") + let body ← bodyString res + if field body "cn" != "oms-desk-a" then + throw (IO.userError s!"mtls A unexpected cn: {body}") + if field body "uri" != "spiffe://lean-grpc.test/oms-desk-a" then + throw (IO.userError s!"mtls A unexpected uri: {body}") + if field body "peer_none" != "false" then + throw (IO.userError s!"mtls A expected peer: {body}") + if (field body "fp").isEmpty then + throw (IO.userError s!"mtls A missing fingerprint: {body}") + + -- 4. Same server, client B → different identity. + let cfgB : Grpc.Tls.Config := { + caPath + certPath := some (dir / "client_b.crt") + keyPath := some (dir / "client_b.key") + serverName + } + let resB ← emptyCallRetry port3 cfgB + if resB.status.code != .ok then + throw (IO.userError s!"mtls B status {resB.status.code.toUInt32}") + let bodyB ← bodyString resB + if field bodyB "cn" != "admin" then + throw (IO.userError s!"mtls B unexpected cn: {bodyB}") + if field bodyB "uri" != "spiffe://lean-grpc.test/admin" then + throw (IO.userError s!"mtls B unexpected uri: {bodyB}") + if field body "cn" == field bodyB "cn" then + throw (IO.userError "mtls: expected distinct CNs for client A vs B") + if field body "fp" == field bodyB "fp" then + throw (IO.userError "mtls: expected distinct fingerprints for client A vs B") + + -- 5. Metadata forgery must not appear in peerIdentity (only in raw metadata). + let forged : Array Hpack.HeaderField := + #[⟨Grpc.Metadata.ascii "x-client-subject", Grpc.Metadata.ascii "admin"⟩] + let resF ← emptyCallRetry port3 cfgA forged + let bodyF ← bodyString resF + if field bodyF "cn" != "oms-desk-a" then + throw (IO.userError s!"forge: peer cn changed by metadata: {bodyF}") + if field bodyF "md_x_client_subject" != "admin" then + throw (IO.userError s!"forge: metadata not visible: {bodyF}") + if (field bodyF "subject").contains "admin" && !(field bodyF "subject").contains "oms-desk-a" then + throw (IO.userError s!"forge: subject looks forged: {bodyF}") + + -- 7. Accept-loop survival: bad handshake must not kill the server. + let mut badRejected := false + try + discard <| emptyCall port3 { caPath, serverName } + catch _ => + badRejected := true + if !badRejected then + throw (IO.userError "accept-loop: expected failed handshake without client cert") + let resAfter ← emptyCallRetry port3 cfgA + if resAfter.status.code != .ok then + throw (IO.userError "accept-loop: server died after failed handshake") + let bodyAfter ← bodyString resAfter + if field bodyAfter "cn" != "oms-desk-a" then + throw (IO.userError s!"accept-loop: bad identity after recovery: {bodyAfter}") finally srv3.kill + -- 6. h2c → peerIdentity = none + let port4 : UInt16 := 50064 + let srv4 ← spawnServer binDir dir port4 false (h2c := true) + try + IO.sleep 300 + let res ← emptyCallRetry port4 {} #[] (useHttps := false) + if res.status.code != .ok then + throw (IO.userError s!"h2c status {res.status.code.toUInt32}") + let body ← bodyString res + if field body "peer_none" != "true" then + throw (IO.userError s!"h2c expected peer_none: {body}") + if field body "mtls_required" != "false" then + throw (IO.userError s!"h2c expected mtls_required=false: {body}") + finally + srv4.kill + IO.println "tlsLoopback OK" diff --git a/Tests/TlsServer.lean b/Tests/TlsServer.lean index 2f88b58..a59c619 100644 --- a/Tests/TlsServer.lean +++ b/Tests/TlsServer.lean @@ -5,23 +5,57 @@ Released under Apache 2.0 license as described in the file LICENSE. import Grpc import Proto -/-- In-process TLS (optionally mTLS) `Grpc.Server`, configured entirely from - the environment so `TlsLoopback` can spawn it as a subprocess: +/-- In-process TLS (optionally mTLS) `Grpc.Server`, configured from the environment + so `TlsLoopback` can spawn it as a subprocess: * `GRPC_PORT` — listen port (default 50060) - * `TLS_CERT` / `TLS_KEY` — server certificate/key (PEM) + * `TLS_CERT` / `TLS_KEY` — server certificate/key (PEM); omit both for h2c * `TLS_CLIENT_CA` — when set, requires and verifies a client certificate - signed by this CA (mTLS) -/ + signed by this CA (mTLS) + * `TLS_H2C=1` — force plaintext h2c (peerIdentity must be none) + + `EmptyCall` is registered with `registerWithContext` and returns a UTF-8 + identity echo body for IAM loopback assertions. -/ + +private def utf8 (s : String) : ByteArray := s.toUTF8 + +private def echoIdentity (ctx : Grpc.ServerCallContext) : ByteArray := + let cn := + match ctx.peerIdentity with + | some id => id.commonName + | none => "" + let uri := + match ctx.peerIdentity with + | some id => id.uriSans.getD 0 "" + | none => "" + let subject := + match ctx.peerIdentity with + | some id => id.subjectDn + | none => "" + let fp := + match ctx.peerIdentity with + | some id => id.fingerprintSha256 + | none => "" + let forged := (ctx.metadata.get? "x-client-subject").getD "" + let peerNone := if ctx.peerIdentity.isNone then "true" else "false" + let mtls := if ctx.mtlsRequired then "true" else "false" + utf8 s!"cn={cn}\nuri={uri}\nsubject={subject}\nfp={fp}\nmd_x_client_subject={forged}\npeer_none={peerNone}\nmtls_required={mtls}\n" + def main : IO Unit := do let port := ((← IO.getEnv "GRPC_PORT").getD "50060").toNat?.getD 50060 |>.toUInt16 + let h2c := (← IO.getEnv "TLS_H2C") == some "1" let cert := (← IO.getEnv "TLS_CERT").getD "" let key := (← IO.getEnv "TLS_KEY").getD "" let clientCa ← IO.getEnv "TLS_CLIENT_CA" let mut s := Grpc.Server.empty - s := Grpc.Server.register s "grpc.testing.TestService" "EmptyCall" fun _ => do - return (ByteArray.empty, { code := .ok }) - let tlsCfg : Grpc.Tls.Config := { - certPath := some (System.FilePath.mk cert) - keyPath := some (System.FilePath.mk key) - clientCaPath := clientCa.map System.FilePath.mk - } - Grpc.Server.serveTls s tlsCfg { host := "127.0.0.1", port } + s := Grpc.Server.registerWithContext s "grpc.testing.TestService" "EmptyCall" fun ctx _ => do + return (echoIdentity ctx, { code := .ok }) + if h2c || cert.isEmpty || key.isEmpty then + IO.println s!"H2c identity server on 127.0.0.1:{port}" + Grpc.Server.serveH2c s { host := "127.0.0.1", port } + else + let tlsCfg : Grpc.Tls.Config := { + certPath := some (System.FilePath.mk cert) + keyPath := some (System.FilePath.mk key) + clientCaPath := clientCa.map System.FilePath.mk + } + Grpc.Server.serveTls s tlsCfg { host := "127.0.0.1", port } diff --git a/docs/README.md b/docs/README.md index 318f67d..5292623 100644 --- a/docs/README.md +++ b/docs/README.md @@ -21,7 +21,7 @@ User and contributor docs for the Lean 4 gRPC stack. | [Formal proofs](proofs.md) | Compile-time `Proofs` library for pure codecs / maps | | [TLS / Envoy](tls-envoy.md) | In-process OpenSSL and optional sidecars | | [CHANGELOG](../CHANGELOG.md) | Package version history | -| [ROADMAP](../ROADMAP.md) | What v1.0.0 shipped vs open proof/hardening follow-ups | +| [ROADMAP](../ROADMAP.md) | What v1.1.0 shipped vs open proof/hardening follow-ups | | [CONTRIBUTING](../CONTRIBUTING.md) | Dev setup, tests, PR expectations | | [SECURITY](../SECURITY.md) | Vulnerability reporting | | [Code of Conduct](../CODE_OF_CONDUCT.md) | Community standards | diff --git a/docs/api-reference.md b/docs/api-reference.md index efccc9e..a9e5525 100644 --- a/docs/api-reference.md +++ b/docs/api-reference.md @@ -1,6 +1,6 @@ # API reference -Lean module catalogue for consumers. Signatures are summarized; see source under `Grpc/`, `H2/`, `Proto/` for full definitions. Version string: `Grpc.version` (currently `1.0.0`). +Lean module catalogue for consumers. Signatures are summarized; see source under `Grpc/`, `H2/`, `Proto/` for full definitions. Version string: `Grpc.version` (currently `1.1.0`). Import umbrella: `import Grpc` (pulls status, channel, server, credentials, TLS, xDS, ops, etc.). Add `import Proto` for bundled message codecs. @@ -87,23 +87,42 @@ Low-level unary on an `H2.ClientConn` (scheme http/https, user-agent, compressio Unary middleware: - `registerUnary` / `callUnary` +- `registerUnaryWithContext` / `applyServerWithContext` - `applyServer` / `applyClient` -- Built-ins: `loggingServer`, `loggingClient` +- Built-ins: `loggingServer`, `loggingClient`, `loggingServerWithContext`, `requirePeerIdentity`, `bearerMetadata` --- ## Server +### `Grpc.PeerIdentity` / `Grpc.ServerCallContext` + +Verified mTLS peer certificate identity (OpenSSL; subject DN is **RFC 2253**): + +| Field | Notes | +|---|---| +| `subjectDn` | Full subject DN | +| `commonName` | CN if present; else empty | +| `dnsSans` / `uriSans` | SAN lists (URI SANs for SPIFFE-style IDs) | +| `fingerprintSha256` | Hex SHA-256 of DER cert | +| `serial` | Hex serial | + +`ServerCallContext`: `peerIdentity`, inbound `metadata` (non-pseudo headers), `methodPath`, `mtlsRequired`. + +`Grpc.Native.Tls.peerIdentity?` extracts identity from an accepted TLS connection. + ### `Grpc.Server` | API | Purpose | |---|---| | `empty` | Empty registry | -| `register` | Unary `ByteArray → IO (ByteArray × Status)` | -| `registerServerStream` / `registerClientStream` / `registerBidi` | Streaming (raw bytes) | -| `registerTyped` / `registerServerStreamTyped` / `registerClientStreamTyped` / `registerBidiTyped` | Streaming/unary with decode/encode adapters | -| `serveH2c` | Listen h2c | -| `serveTls` | Listen TLS+ALPN (via `Tls.Config`) | +| `register` | Unary `ByteArray → IO (ByteArray × Status)` (ignores context) | +| `registerWithContext` | Unary with `ServerCallContext` (peer identity + metadata) | +| `registerTyped` / `registerTypedWithContext` | Typed unary adapters | +| `registerServerStream` / `registerClientStream` / `registerBidi` | Streaming (raw bytes; context deferred) | +| `registerServerStreamTyped` / `registerClientStreamTyped` / `registerBidiTyped` | Streaming with decode/encode adapters | +| `serveH2c` | Listen h2c (`peerIdentity = none`) | +| `serveTls` | Listen TLS+ALPN; per-connection peer identity → context handlers | | `maxMsgSize` | Inbound limit | Bad `content-type` → HTTP **415**. Unknown method / zero timeout → trailers-only gRPC status. @@ -131,7 +150,8 @@ Bad `content-type` → HTTP **415**. Unknown method / zero timeout → trailers- `certPath`, `keyPath`, `caPath`, `clientCaPath`, `serverName`, `alpn` (default `["h2"]`). - Client mTLS: set `certPath` + `keyPath` -- Server mTLS: set `clientCaPath` on serve +- Server mTLS: set `clientCaPath` on serve — verified peer identity is available via `registerWithContext` / `ServerCallContext.peerIdentity` +- `Tls.serveH2` takes `mkHandler : Option PeerIdentity → H2.StreamHandler`; failed accepts/handshakes are logged and the listen loop continues Env: `LEAN_GRPC_TLS_PROXY`, `LEAN_GRPC_TLS_INSECURE_FALLBACK=1` (dev only). diff --git a/docs/architecture.md b/docs/architecture.md index a8a5af2..199d2c9 100644 --- a/docs/architecture.md +++ b/docs/architecture.md @@ -73,6 +73,8 @@ DialOptions ADC (`Grpc.Adc`) fetches a token (service-account JWT exchange or GCE metadata) and injects `authorization: Bearer …`. Live Google calls need real credentials; CI uses `scripts/mock-adc-server.py`. +Server-side mTLS: when `Tls.Config.clientCaPath` is set, `serveTls` extracts the verified peer certificate per connection (`Native.Tls.peerIdentity?`) and threads it into unary handlers via `ServerCallContext` / `registerWithContext`. Identity never comes from client metadata. + ## Discovery and load balancing ```text diff --git a/docs/conformance.md b/docs/conformance.md index 7259db8..1362a7c 100644 --- a/docs/conformance.md +++ b/docs/conformance.md @@ -90,7 +90,9 @@ Notes: - mTLS: `Grpc.Tls.Config.certPath`/`keyPath` present a client certificate on dial; `Grpc.Tls.Config.clientCaPath` makes `serveTls`/`Grpc.Tls.serveH2` require and verify a client certificate. Covered end-to-end by `tlsLoopback` (plain TLS, mTLS-reject-without-cert, - mTLS-accept-with-cert), skipped only if `openssl` is unavailable in the environment. + mTLS-accept-with-cert, dual-cert peer-identity binding, metadata non-forgery, h2c → + `peerIdentity = none`, accept-loop survival), skipped only if `openssl` is unavailable. + Unary handlers read verified identity via `registerWithContext` / `ServerCallContext.peerIdentity`. - ADC composition: `Grpc.Adc.dialOptions` builds `Credentials.DialOptions` combining TLS channel credentials with an ADC-derived per-RPC Bearer token, for calling real Google APIs. - xDS ADS now resolves the full chain a real xDS-enabled client would: `Grpc.XdsAds.resolveChain` @@ -121,9 +123,10 @@ Notes: preferred/primary discovery+LB path in this library; grpclb exists for interop with older balancers that only speak the plain server-list protocol. - Interceptors: `Grpc.Interceptor` provides composable client/server unary interceptor chains - (`applyClient`/`applyServer`, `callUnary`/`registerUnary`) plus ready-made logging - interceptors; additional cross-cutting concerns (auth, metrics, retries) compose the same - way by adding more `ClientUnary`/`ServerUnary` elements to the chain array. + (`applyClient`/`applyServer`, `callUnary`/`registerUnary`) plus context-aware + `registerUnaryWithContext` / `requirePeerIdentity` and ready-made logging interceptors; + additional cross-cutting concerns (auth, metrics, retries) compose the same way by adding + more `ClientUnary`/`ServerUnary` (or `ServerUnaryWithContext`) elements to the chain array. - Soak: `Bench/Soak.lean` (`benchSoak`) now understands the standard `--soak_*` flags used by grpc's `rpc_soak`/`channel_soak` tools (`soak_iterations`, `soak_max_failures`, `soak_per_iteration_max_acceptable_latency_ms`, `soak_min_time_ms_between_rpcs`, diff --git a/docs/cookbook-interceptors.md b/docs/cookbook-interceptors.md index db9443e..dfb9b62 100644 --- a/docs/cookbook-interceptors.md +++ b/docs/cookbook-interceptors.md @@ -57,9 +57,10 @@ let ch ← Grpc.Channel.dial "api.example.com:443" { } ``` -## mTLS +## mTLS → read `ctx.peerIdentity` in the handler -Client presents a certificate; server requires and verifies one: +Client presents a certificate; server requires and verifies one, then exposes the +**verified** peer identity to unary handlers via `ServerCallContext`: ```lean -- Client @@ -73,6 +74,23 @@ let ch ← Grpc.Channel.dial "localhost:50051" { } -- Server +let mut s := Grpc.Server.empty +s := Grpc.Server.registerWithContext s "demo.Svc" "Ping" fun ctx req => do + match ctx.peerIdentity with + | none => + -- Under mTLS (`clientCaPath` set) this should be unreachable after a + -- successful handshake; treat as miswire / UNAUTHENTICATED. + pure (ByteArray.empty, .unauthenticated "mtls_required") + | some id => + -- Map id.uriSans / id.commonName → principal via local policy. + -- Subject DN is OpenSSL RFC 2253 form. + pure (req, .ok) + +-- Optional interceptor that fails closed when mTLS was configured but identity is missing: +s := Grpc.Interceptor.registerUnaryWithContext s "demo.Svc" "Secure" + #[Grpc.Interceptor.requirePeerIdentity] fun ctx req => do + pure (req, .ok) + Grpc.Server.serveTls s { certPath := some "certs/server.pem" keyPath := some "certs/server.key" @@ -80,10 +98,25 @@ Grpc.Server.serveTls s { } { host := "127.0.0.1", port := 50051 } ``` -End-to-end coverage: `tlsLoopback` (plain TLS, reject without client cert, accept with client cert). +**Do not** treat inbound metadata such as `x-client-subject`, `x-forwarded-client-cert`, +or a self-declared `principalId` in the request body as AuthN. Those values are +attacker-controlled unless you terminate TLS at a **trusted** proxy and document a +separate trusted-proxy identity mode (not provided by lean-grpc today). Identity +fields are only as trustworthy as the `clientCaPath` private CA / PKI. + +End-to-end coverage: `tlsLoopback` (plain TLS, reject without client cert, accept +with client cert, dual-cert identity binding, metadata non-forgery, h2c → `none`, +accept-loop survival after failed handshake). + +Working example: `Examples/MirrorForge/` — `Stamp` uses `registerUnaryWithContext` +(Bearer metadata preferred, body token fallback). Set `TLS_CERT`/`TLS_KEY`/ +`TLS_CLIENT_CA` on the server and `TLS_CA` (+ client cert) on the client for mTLS; +see `Examples/MirrorForge/README.md`. + +Streaming handlers do not yet receive `ServerCallContext` (follow-on). ## See also - [TLS / Envoy](tls-envoy.md) - `Tests/OpsSmoke.lean` — interceptor + health/reflection/channelz smoke -- `Tests/TlsLoopback.lean` — mTLS loopback +- `Tests/TlsLoopback.lean` — mTLS + peer-identity loopback diff --git a/docs/cookbook-unary.md b/docs/cookbook-unary.md index ce23ce6..6b7b71e 100644 --- a/docs/cookbook-unary.md +++ b/docs/cookbook-unary.md @@ -34,6 +34,20 @@ def main : IO Unit := do Grpc.Server.serveH2c s { host := "127.0.0.1", port := 50051 } ``` +### With `ServerCallContext` (mTLS peer identity / inbound metadata) + +Generated stubs also emit `register*WithContext`: + +```lean +s := helloworld.registerGreeterSayHelloWithContext s fun ctx req => do + match ctx.peerIdentity with + | none => pure ({ message := "" }, .unauthenticated "mtls_required") + | some id => + pure ({ message := s!"Hello, {req.name} (from {id.commonName})" }, .ok) +``` + +See [Cookbook: interceptors & auth](cookbook-interceptors.md) for mTLS `serveTls` and MirrorForge. + ## Client ```lean diff --git a/docs/getting-started.md b/docs/getting-started.md index 0337439..3c65df1 100644 --- a/docs/getting-started.md +++ b/docs/getting-started.md @@ -4,7 +4,7 @@ This guide gets a Lean 4 unary gRPC server and client running on h2c with **type **Requirements:** Lean 4.32+ (see `lean-toolchain`), OpenSSL headers for the `Grpc` library (`libssl-dev` or `./scripts/fetch-openssl-headers.sh`). Peer gzip optionally uses a zlib helper (`./scripts/build_native.sh`) or system `gzip`. -Package version: **1.0.0** (`lakefile.lean` / `Grpc.version`). +Package version: **1.1.0** (`lakefile.lean` / `Grpc.version`). ## Build the repo @@ -151,12 +151,12 @@ In your `lakefile.lean`: ```lean require «lean-grpc» from git - "https://github.com/RileyBetts/lean-grpc.git" @ "v1.0.0" + "https://github.com/RileyBetts/lean-grpc.git" @ "v1.1.0" ``` Then `import Grpc` (and `Proto` if you use the bundled codecs). Public libs: `Bytes`, `Hpack`, `H2`, `Proto`, `Grpc`. Linking OpenSSL (`-lssl -lcrypto`) is pulled in via the `Grpc` Lake library (not via Bytes/Hpack/H2 alone). For peer gzip against foreign stacks, set `LEAN_GRPC_ZLIB_HELPER` after `./scripts/build_native.sh`. Full packaging notes: [packaging.md](packaging.md). Hosted docs: [rileybetts.ai/oss/lean-grpc](https://rileybetts.ai/oss/lean-grpc). -After [Reservoir](https://reservoir.lean-lang.org/) indexes the package you can use `require «lean-grpc»` without a git URL. Pin a commit SHA if the `v1.0.0` tag is not yet on the remote you use. +After [Reservoir](https://reservoir.lean-lang.org/) indexes the package you can use `require «lean-grpc»` without a git URL. Pin a commit SHA if the `v1.1.0` tag is not yet on the remote you use. ## Next steps diff --git a/docs/packaging.md b/docs/packaging.md index 7c083dc..9b23819 100644 --- a/docs/packaging.md +++ b/docs/packaging.md @@ -65,7 +65,7 @@ lake build ```lean require «lean-grpc» from git - "https://github.com/RileyBetts/lean-grpc.git" @ "v1.0.0" + "https://github.com/RileyBetts/lean-grpc.git" @ "v1.1.0" ``` Then `import Grpc` (and `Proto` if using bundled codecs). @@ -76,7 +76,7 @@ Then `import Grpc` (and `Proto` if using bundled codecs). require «lean-grpc» -- once listed on reservoir.lean-lang.org ``` -Package version in-tree is **1.0.0** (`lakefile.lean`, `Grpc.version`). Hosted docs: [rileybetts.ai/oss/lean-grpc](https://rileybetts.ai/oss/lean-grpc). Creating the git tag on origin is a separate maintainer step (below). +Package version in-tree is **1.1.0** (`lakefile.lean`, `Grpc.version`). Hosted docs: [rileybetts.ai/oss/lean-grpc](https://rileybetts.ai/oss/lean-grpc). Creating the git tag on origin is a separate maintainer step (below). ## Maintainer release checklist @@ -89,8 +89,8 @@ Documented only — do **not** automate tagging from CI or agent runs. 5. **Manual version tagging (maintainer only):** on `main`, when you choose to publish: ```bash - git tag -a v1.0.0 -m "lean-grpc 1.0.0" - git push origin v1.0.0 + git tag -a v1.1.0 -m "lean-grpc 1.1.0" + git push origin v1.1.0 ``` Agents and CI must not create or push tags. diff --git a/docs/tls-envoy.md b/docs/tls-envoy.md index 58f7d58..0953a95 100644 --- a/docs/tls-envoy.md +++ b/docs/tls-envoy.md @@ -15,15 +15,21 @@ let ch ← Grpc.Channel.dial "api.example.com:443" { } ``` -Server with certs: +Server with certs (handler factory receives optional peer identity per connection): ```lean Grpc.Tls.serveH2 { certPath := some "server.pem" keyPath := some "server.key" -} h2cfg handler + clientCaPath := some "client-ca.pem" -- mTLS +} h2cfg fun peerId => + Grpc.Server.handlerFor s peerId (mtlsRequired := true) ``` +Prefer `Grpc.Server.serveTls`, which wires peer identity into `registerWithContext` handlers automatically. Identity fields are only as trustworthy as the `clientCaPath` CA; rotate and protect that private CA like any production AuthN root. + +Failed TLS handshakes are logged (`tls accept error: …`) and the accept loop continues — misbehaving clients / readiness probes do not take down the listener. + Interop: `./scripts/interop-tls-go-lean.sh` (Lean client → Go TLS server, **no** `LEAN_GRPC_TLS_PROXY`). Build needs OpenSSL headers (`libssl-dev`, or `./scripts/fetch-openssl-headers.sh` when headers are missing). diff --git a/docs/website-sync.md b/docs/website-sync.md index 334bf51..0eeee9c 100644 --- a/docs/website-sync.md +++ b/docs/website-sync.md @@ -36,7 +36,7 @@ stay aligned with `README.md` / `SECURITY.md` here. 1. Polish / merge lean-grpc docs on `development` → `main`. 2. Promote website pages; stage then production deploy. 3. Ensure the GitHub repo is public, Apache-2.0 detected, Security Advisories on, ≥2 stars. -4. Maintainer tags `v1.0.0` manually (see [packaging.md](packaging.md)). +4. Maintainer tags `v1.1.0` manually (see [packaging.md](packaging.md)). 5. Wait for Reservoir’s daily crawl; verify the package page and homepage link. 6. Prefer bare `require «lean-grpc»` in README/site copy once indexed. diff --git a/feature/lean-grpc-iam-requirements.md b/feature/lean-grpc-iam-requirements.md new file mode 100644 index 0000000..dd28a5b --- /dev/null +++ b/feature/lean-grpc-iam-requirements.md @@ -0,0 +1,192 @@ +# lean-grpc IAM requirements (from lean-compliance) + +**Status:** working requirements handoff — not an official lean-compliance `docs/` claim. +**Date:** 2026-08-04 +**Consumer:** lean-compliance enterprise AuthN (audit §1 / §5) +**lean-grpc pin today:** `https://github.com/RileyBetts/lean-grpc.git` @ `v1.0.0` (`rev` `33334dec…` in `lean/lake-manifest.json`) + +## 1. Why this exists + +lean-compliance’s production entrypoint is a Lean gRPC server (`lean_compliance_server`) built on lean-grpc. Enterprise AuthN requires: + +1. TLS (and mTLS) on the listen path — **partially available today** via `Grpc.Server.serveTls` + `Tls.Config.clientCaPath`. +2. A **verified caller identity** derived from the peer certificate, passed into application handlers — **not available today**. + +Without (2), mTLS only proves “some cert signed by our CA connected.” It does **not** let lean-compliance map that connection to `oms-desk-a` vs `admin`. Application code would still trust a self-declared `principalId` on the wire — the Critical gap in [`enterprise_readiness_audit.md`](enterprise_readiness_audit.md) §1. + +This document specifies what lean-grpc must expose so lean-compliance can stop trusting client-supplied principals outside development. + +## 2. Current lean-grpc surface (verified against vendored tree) + +| Capability | Status | Evidence | +|---|---|---| +| Plaintext h2c serve | Present | `Grpc.Server.serveH2c` | +| TLS serve (server cert/key) | Present | `Grpc.Server.serveTls`, `Tls.Config.certPath` / `keyPath` | +| mTLS verify client cert | Present | `Tls.Config.clientCaPath` → native `SSL_VERIFY_PEER \| SSL_VERIFY_FAIL_IF_NO_PEER_CERT` | +| Client mTLS dial | Present | `Tls.Config` client `certPath`/`keyPath`; cookbook mTLS section | +| Loopback TLS/mTLS tests | Present | `Tests/TlsServer.lean`, `Tests/TlsLoopback.lean` (per docs) | +| Peer certificate subject/SAN exposed to Lean | **Missing** | No `SSL_get_peer_certificate` / X509 subject API in `native/tls_ffi.c` or `Grpc.Native.Tls` | +| Request context on unary handlers | **Missing** | `UnaryHandler := ByteArray → IO (ByteArray × Status)` — body only; no metadata, no peer identity | +| Server interceptor access to peer identity | **Missing** | `Grpc.Interceptor.ServerUnary` wraps the same body-only handler | +| Inbound `authorization` metadata to handler | **Missing / incomplete** | Client can *send* bearer metadata; server handler does not receive a typed request context with headers | + +## 3. Goals (must) + +### G1 — Peer identity after mTLS + +After a successful mTLS handshake (`clientCaPath` set and client cert verified), lean-grpc must make the verified client identity available to Lean application code for that RPC. + +**Minimum identity fields:** + +| Field | Required | Notes | +|---|---|---| +| `subject_dn` | Must | Full subject DN string (OpenSSL one-line or RFC 2253 — pick one and document) | +| `common_name` | Must | CN if present; else empty | +| `dns_sans` | Must | Zero or more DNS SANs | +| `uri_sans` | Must | Zero or more URI SANs (SPIFFE IDs matter for service accounts) | +| `fingerprint_sha256` | Should | Hex SHA-256 of DER cert; useful for pin/allowlist debugging | +| `serial` | Nice | Hex serial | + +Identity must come **only** from the verified peer cert on the TLS connection — never from client-supplied gRPC metadata that claims to be the subject. + +### G2 — Request context on server handlers + +Replace (or overload) body-only unary registration with a context-aware API, e.g.: + +```lean +structure ServerCallContext where + peerIdentity : Option PeerIdentity -- none on h2c / TLS without client cert + metadata : Metadata -- inbound headers (lowercased keys) + methodPath : String -- e.g. /lean_compliance.v1.ComplianceGate/AssessOrder + -- optional later: remoteAddr, deadline remaining, compression + +abbrev UnaryHandlerWithContext := + ServerCallContext → ByteArray → IO (ByteArray × Status) +``` + +Requirements: + +- Existing `UnaryHandler` / `register` may remain for back-compat, but new `registerWithContext` (name flexible) must be first-class and used by health/reflection without breaking them. +- Streaming handlers (server/client/bidi) need the same context availability in a follow-on if not in v1 of this work — document if deferred. +- `peerIdentity = none` when: plaintext h2c; TLS without `clientCaPath`; or client presented no cert (should not happen if mTLS required — fail handshake instead). + +### G3 — Fail closed on mTLS misconfiguration + +When `clientCaPath` is set: + +- Handshake **must** fail if client omits cert or cert fails verify (already intended). +- Application must be able to distinguish “authenticated peer” (`some identity`) from “should be impossible” and treat missing identity under mTLS as `UNAUTHENTICATED` / internal miswire — not as anonymous success. + +### G4 — Tests lean-compliance will rely on + +Upstream CI (or published test binary patterns) must cover: + +1. TLS without client cert + `clientCaPath` set → connection rejected. +2. mTLS with valid client cert → handler observes `peerIdentity.common_name` / SAN matching fixture cert. +3. Two different client certs → two different `peerIdentity` values in handler. +4. h2c path → `peerIdentity = none`. +5. Attacker-controlled metadata header `x-client-subject: admin` does **not** appear in `peerIdentity` (only in raw `metadata` if sent — app must ignore it for AuthN). + +## 4. Non-goals (out of scope for this handoff) + +- lean-compliance RBAC policy evaluation (roles, fund/account scopes) — stays in lean-compliance. +- Full SPIFFE/SPIRE workload API integration (URI SAN extraction is enough for apps to map SPIFFE IDs). +- JWT/OIDC token validation inside lean-grpc (optional future; not blocking lean-compliance mTLS AuthN). +- Changing ALPN/`h2` behavior unrelated to identity. +- Fixing all items in lean-grpc `docs/security-review-2026-08.md` — only IAM-relevant items below are in scope for this ask. + +## 5. Suggested API shape (informative, not mandatory) + +Lean-compliance can adapt to equivalent designs; this is a concrete target to reduce bikeshedding. + +### Native FFI (`tls_ffi.c` / `Grpc.Native.Tls`) + +```c +/* After accept + handshake; returns 1 if peer cert present and verified path used. */ +int lean_grpc_tls_peer_identity( + lean_grpc_ssl_conn *c, + char *subject_dn, size_t subject_dn_len, + char *cn, size_t cn_len, + /* SAN lists: NUL-separated or JSON blob — document encoding */ + char *dns_sans, size_t dns_sans_len, + char *uri_sans, size_t uri_sans_len, + char *fp_sha256_hex, size_t fp_len +); +``` + +Or return a Lean object built in FFI. Prefer not requiring apps to parse ASN.1 in Lean. + +### Lean transport plumbing + +Today `Tls.serveH2` accepts a connection and calls `H2.serveTransport (Grpc.Native.Tls.transport conn) handler` with an `H2.StreamHandler` that does **not** receive `conn`. Identity must be: + +- attached to the transport / connection object, and +- threaded into `Grpc.Server.handlerFor` so unary dispatch can build `ServerCallContext`. + +This is the core engineering change: **connection-scoped state → per-RPC context**. + +### Example app usage (lean-compliance intent) + +```lean +s := Grpc.Server.registerWithContext s "lean_compliance.v1.ComplianceGate" "AssessOrder" fun ctx req => do + match ctx.peerIdentity with + | none => pure (errBody, .unauthenticated "mtls_required") + | some id => + -- map id.uri_sans / id.common_name → principal_id via local policy + handleAssess (principalFrom id) req +``` + +## 6. Compatibility & versioning + +- Prefer additive APIs (`registerWithContext`) so existing examples keep compiling. +- If `UnaryHandler` signature must change, ship a **minor/major bump** lean-compliance can pin (`v1.1.0` or `v2.0.0`) and document migration in lean-grpc CHANGELOG. +- lean-compliance currently requires `@ "v1.0.0"` — will bump pin once the IAM release tags. + +## 7. Documentation lean-grpc should ship with the feature + +1. Cookbook update: “mTLS → read `ctx.peerIdentity` in handler” (extend `docs/cookbook-interceptors.md`). +2. Explicit warning: **do not** treat inbound metadata `x-forwarded-client-cert` / custom subject headers as AuthN unless the operator runs a **trusted TLS-terminating proxy** and lean-grpc documents a separate “trusted proxy identity” mode (optional; not required for lean-compliance in-process mTLS path). +3. Security notes: identity fields are only as trustworthy as the `clientCaPath` PKI; document private CA operational expectations briefly. + +## 8. Acceptance criteria (Definition of Done for lean-grpc) + +- [x] Native API extracts subject DN, CN, DNS SANs, URI SANs from verified peer cert. +- [x] Server unary handler (context API) can read `peerIdentity` for mTLS connections. +- [x] Automated test proves two client certs yield two identities inside the handler. +- [x] Automated test proves metadata cannot forge `peerIdentity`. +- [x] Cookbook + API reference updated. +- [ ] Tagged release lean-compliance can depend on. *(in-tree **1.1.0**; maintainer tags `v1.1.0` manually)* + +## 9. Priority / sequencing relative to lean-compliance + +| lean-compliance phase | lean-grpc dependency | +|---|---| +| Phase 2a — wire `serveTls` + env cert paths | **None** — use existing `serveTls` / `clientCaPath` | +| Phase 2b — stop trusting wire `principalId` | **Blocked on G1+G2** (this document) | +| Interim workaround | TLS-terminating sidecar injects identity metadata — **not preferred**; only if lean-grpc IAM slips; requires trusted-network assumptions documented in ops | + +**Ask:** Please treat G1+G2 as P0 for any consumer needing enterprise IAM on Lean gRPC servers. Phase 2a in lean-compliance can proceed in parallel; Phase 2b merges after the lean-grpc tag exists (or after a temporary sidecar stopgap explicitly labeled interim). + +## 10. Related lean-grpc security-review items (optional stretch) + +From vendored `docs/security-review-2026-08.md`, these amplify IAM trust if fixed in the same release train — not hard blockers for the identity API itself: + +- Hostname verify gaps on sensitive TLS dial paths. +- Documented insecure escapes (`insecureSkipVerify`, h2c fallbacks) remaining easy to leave on in production. + +lean-compliance will refuse insecure listen modes outside development on its side; library-level hard refusals would still help all consumers. + +## 10. Contact / consumer expectations + +When the feature lands, lean-compliance will: + +1. Bump `require «lean-grpc»` to the new tag. +2. Map `uri_sans` / `common_name` → `principal_id` via `config/rbac.yaml` (`cert_subjects` / `spiffe_ids`). +3. Ignore request-body `principalId` whenever `LEAN_COMPLIANCE_ENV` ∈ {staging, production}. +4. Add interop tests: Python/grpcio mTLS client ↔ Lean server identity binding. + +**Also file upstream:** failed TLS handshake / plaintext TCP connect against an mTLS listener currently aborts the accept loop (`uncaught exception: tls accept: SSL_accept failed`). Accept errors should be logged and the loop continued — otherwise readiness probes and misbehaving clients take down the server. + +**Also file upstream:** failed TLS handshake / plaintext TCP connect against an mTLS listener currently aborts the accept loop (`uncaught exception: tls accept: SSL_accept failed`). Accept errors should be logged and the loop continued — otherwise readiness probes and misbehaving clients take down the server. + +Questions for lean-grpc maintainers can be filed against this file’s §3–§8 checklist. diff --git a/lakefile.lean b/lakefile.lean index be7dfa9..766c683 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -7,7 +7,7 @@ open Lake DSL open System package «lean-grpc» where - version := v!"1.0.0" + version := v!"1.1.0" keywords := #["grpc", "http2", "hpack", "protobuf", "networking"] description := "Pure Lean 4 gRPC stack (HTTP/2 + HPACK + gRPC) on Std.Async" homepage := "https://rileybetts.ai/oss/lean-grpc" diff --git a/native/tls_ffi.c b/native/tls_ffi.c index b85dbf3..82ed987 100644 --- a/native/tls_ffi.c +++ b/native/tls_ffi.c @@ -8,10 +8,13 @@ #include #include #include +#include #include #include #include #include +#include +#include #include #include #include @@ -372,6 +375,138 @@ LEAN_EXPORT lean_obj_res lean_grpc_tls_close(b_lean_obj_arg conn_obj, lean_obj_a return lean_io_result_mk_ok(lean_box(0)); } +static lean_object *mk_string_n(const char *s, size_t n) { + return lean_mk_string_from_bytes(s, n); +} + +static lean_object *mk_string_cstr(const char *s) { + return lean_mk_string(s ? s : ""); +} + +static void hex_encode(const unsigned char *in, size_t n, char *out) { + static const char *hex = "0123456789abcdef"; + for (size_t i = 0; i < n; ++i) { + out[i * 2] = hex[(in[i] >> 4) & 0xf]; + out[i * 2 + 1] = hex[in[i] & 0xf]; + } + out[n * 2] = '\0'; +} + +static lean_object *array_push_str(lean_object *arr, const char *s, size_t n) { + return lean_array_push(arr, mk_string_n(s, n)); +} + +/* Extract verified peer certificate identity into Grpc.PeerIdentity (6 String/Array fields). + Returns Option.none when no peer certificate is present. */ +LEAN_EXPORT lean_obj_res lean_grpc_tls_peer_identity(b_lean_obj_arg conn_obj, lean_obj_arg world) { + (void)world; + lean_grpc_ssl_conn *c = (lean_grpc_ssl_conn *)lean_get_external_data(conn_obj); + if (!c || !c->ssl) return lean_io_result_mk_ok(lean_box(0)); /* none */ + X509 *cert = SSL_get_peer_certificate(c->ssl); + if (!cert) return lean_io_result_mk_ok(lean_box(0)); /* none */ + + lean_object *subject_dn = mk_string_cstr(""); + lean_object *common_name = mk_string_cstr(""); + lean_object *dns_sans = lean_mk_empty_array(); + lean_object *uri_sans = lean_mk_empty_array(); + lean_object *fp_hex = mk_string_cstr(""); + lean_object *serial_hex = mk_string_cstr(""); + + /* Subject DN — RFC 2253 */ + { + BIO *bio = BIO_new(BIO_s_mem()); + if (bio) { + if (X509_NAME_print_ex(bio, X509_get_subject_name(cert), 0, XN_FLAG_RFC2253) >= 0) { + char *p = NULL; + long len = BIO_get_mem_data(bio, &p); + if (p && len > 0) { + lean_dec(subject_dn); + subject_dn = mk_string_n(p, (size_t)len); + } + } + BIO_free(bio); + } + } + + /* Common Name */ + { + char cn[256]; + int n = X509_NAME_get_text_by_NID(X509_get_subject_name(cert), NID_commonName, cn, (int)sizeof(cn)); + if (n > 0) { + lean_dec(common_name); + common_name = mk_string_n(cn, (size_t)n); + } + } + + /* DNS / URI SANs */ + { + GENERAL_NAMES *sans = (GENERAL_NAMES *)X509_get_ext_d2i(cert, NID_subject_alt_name, NULL, NULL); + if (sans) { + int count = sk_GENERAL_NAME_num(sans); + for (int i = 0; i < count; ++i) { + GENERAL_NAME *gn = sk_GENERAL_NAME_value(sans, i); + if (!gn) continue; + ASN1_STRING *as = NULL; + if (gn->type == GEN_DNS) + as = gn->d.dNSName; + else if (gn->type == GEN_URI) + as = gn->d.uniformResourceIdentifier; + if (!as) continue; + const unsigned char *data = ASN1_STRING_get0_data(as); + int len = ASN1_STRING_length(as); + if (!data || len <= 0) continue; + if (gn->type == GEN_DNS) + dns_sans = array_push_str(dns_sans, (const char *)data, (size_t)len); + else + uri_sans = array_push_str(uri_sans, (const char *)data, (size_t)len); + } + GENERAL_NAMES_free(sans); + } + } + + /* SHA-256 fingerprint of DER cert */ + { + unsigned char md[EVP_MAX_MD_SIZE]; + unsigned int md_len = 0; + if (X509_digest(cert, EVP_sha256(), md, &md_len) == 1 && md_len > 0) { + char hex[EVP_MAX_MD_SIZE * 2 + 1]; + hex_encode(md, md_len, hex); + lean_dec(fp_hex); + fp_hex = mk_string_cstr(hex); + } + } + + /* Serial number (hex) */ + { + const ASN1_INTEGER *ser = X509_get0_serialNumber(cert); + BIGNUM *bn = ser ? ASN1_INTEGER_to_BN(ser, NULL) : NULL; + if (bn) { + char *hex = BN_bn2hex(bn); + if (hex) { + lean_dec(serial_hex); + serial_hex = mk_string_cstr(hex); + OPENSSL_free(hex); + } + BN_free(bn); + } + } + + X509_free(cert); + + /* PeerIdentity structure: 6 object fields */ + lean_object *id = lean_alloc_ctor(0, 6, 0); + lean_ctor_set(id, 0, subject_dn); + lean_ctor_set(id, 1, common_name); + lean_ctor_set(id, 2, dns_sans); + lean_ctor_set(id, 3, uri_sans); + lean_ctor_set(id, 4, fp_hex); + lean_ctor_set(id, 5, serial_hex); + + lean_object *some = lean_alloc_ctor(1, 1, 0); + lean_ctor_set(some, 0, id); + return lean_io_result_mk_ok(some); +} + /* ---- ADC helpers (Phase 2) ---- */ static lean_obj_res mk_byte_array(const uint8_t *data, size_t n) {