From 6dcf68a637581fcb64fefc29589971ed0faa8f87 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 19 May 2026 06:19:15 +0000 Subject: [PATCH 1/2] feat(mtls): make mTLS the primary trust-level path (Phase B) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Closes the Phase B security gap from the http-capability-gateway audit: header-derived trust is forgeable without transport-level client-cert verification. - B1: add a fail-closed Cowboy HTTPS listener (verify: :verify_peer, fail_if_no_peer_cert: true). When TRUST_LEVEL_SOURCE=mtls the TLS material is mandatory; the app refuses to start rather than silently downgrading to the header path. - B2: is_cert_verified/1 now reads real TLS transport state (https scheme + Cowboy adapter + non-empty peer cert) instead of mere cert presence. - B3: docs/mtls-rotation-runbook.md — CA-selection decision and no-downtime cert/CA rotation procedure. - B4: src/abi/MTLSPolicy.idr records the "unverified cert is never privileged" proof obligation (status pending Phase C/D; excluded from gateway.ipkg so it does not gate the build). - Real test-CA fixture (test/fixtures/mtls) + test/mtls_test.exs driving the cert->trust pipeline and proving the CA trust invariant via :public_key.pkix_path_validation/3. Closes the audit's "Real-CA mTLS integration test" gap. Co-Authored-By: Claude Opus 4.7 --- PROOFS_NEEDED.md | 14 +- TEST-NEEDS.md | 2 +- config/runtime.exs | 10 +- docs/mtls-rotation-runbook.md | 100 +++++++++++ lib/http_capability_gateway/application.ex | 191 ++++++++++++++++----- lib/http_capability_gateway/gateway.ex | 55 +++++- src/abi/MTLSPolicy.idr | 46 +++++ test/fixtures/mtls/ca.crt | 20 +++ test/fixtures/mtls/client-auth.crt | 19 ++ test/fixtures/mtls/client-internal.crt | 19 ++ test/fixtures/mtls/client-rogue.crt | 19 ++ test/fixtures/mtls/gen-test-ca.sh | 63 +++++++ test/fixtures/mtls/rogue-ca.crt | 20 +++ test/fixtures/mtls/server.crt | 19 ++ test/mtls_test.exs | 91 ++++++++++ 15 files changed, 637 insertions(+), 51 deletions(-) create mode 100644 docs/mtls-rotation-runbook.md create mode 100644 src/abi/MTLSPolicy.idr create mode 100644 test/fixtures/mtls/ca.crt create mode 100644 test/fixtures/mtls/client-auth.crt create mode 100644 test/fixtures/mtls/client-internal.crt create mode 100644 test/fixtures/mtls/client-rogue.crt create mode 100755 test/fixtures/mtls/gen-test-ca.sh create mode 100644 test/fixtures/mtls/rogue-ca.crt create mode 100644 test/fixtures/mtls/server.crt create mode 100644 test/mtls_test.exs diff --git a/PROOFS_NEEDED.md b/PROOFS_NEEDED.md index 9a18659..5d70f10 100644 --- a/PROOFS_NEEDED.md +++ b/PROOFS_NEEDED.md @@ -2,7 +2,7 @@ ## Current State -- **src/abi/*.idr**: YES — `Protocol.idr`, `Types.idr` +- **src/abi/*.idr**: YES — `Protocol.idr`, `Types.idr`, `MTLSPolicy.idr` (obligation stub) - **Dangerous patterns**: 0 (`believe_me` reference in Protocol.idr is documentation only) - **LOC**: ~9,500 - **ABI layer**: Idris2 definitions present @@ -15,6 +15,18 @@ | Protocol state machine | Session state transitions are total | Prevent stuck/invalid protocol states | | Permission composition | Capability intersection/union laws | Ensure composed permissions don't escalate | | ABI type safety | FFI boundary type marshalling correctness | Prevent memory corruption at language boundary | +| mTLS trust policy | An unverified client cert is never mapped to a privileged trust class (`classify CertUnverified _ = Untrusted`) | Security core of Phase B mTLS-as-primary-path: forged/unverified certs must be indistinguishable from anonymous | + +### mTLS trust policy (Phase B / standards#97) + +- **Claim stated:** `src/abi/MTLSPolicy.idr` — `unverifiedNeverPrivileged`. +- **Status:** PENDING (scheduled for Phase C/D — standards#98/#99). The + obligation is recorded as a `0`-multiplicity hole; not yet discharged and + intentionally excluded from `gateway.ipkg modules` so it does not gate the + build before discharge. +- **Mirrors:** the runtime decision in + `Gateway.determine_trust_level_from_cert/2` and the listener fail-closed + contract in `HttpCapabilityGateway.Application`. ## Recommended Prover diff --git a/TEST-NEEDS.md b/TEST-NEEDS.md index b16e552..b49112a 100644 --- a/TEST-NEEDS.md +++ b/TEST-NEEDS.md @@ -50,7 +50,7 @@ - **Zig FFI integration test execution** — requires zig toolchain; covered by separate FFI build step. - **Container build smoke test** — performed in CI, not in `mix test`. - **Error handling: upstream timeout** — Req receive_timeout covered implicitly; no dedicated test. -- **Real-CA mTLS integration test** — code uses `Record.extract` accessors but no live cert in test fixtures. +- ~~**Real-CA mTLS integration test** — code uses `Record.extract` accessors but no live cert in test fixtures.~~ **CLOSED (Phase B / standards#97):** `test/mtls_test.exs` drives the cert→trust pipeline with a real test CA (`test/fixtures/mtls/`) and proves the CA trust invariant via `:public_key.pkix_path_validation/3`. Live-socket handshake test across the gateway↔BoJ seam is Phase C scope. - **Self-tests for config validation on startup** — Application.start refuses without policy, but no dedicated assertion. ## Priority diff --git a/config/runtime.exs b/config/runtime.exs index 9bf48a7..99c61d4 100644 --- a/config/runtime.exs +++ b/config/runtime.exs @@ -9,5 +9,13 @@ if config_env() == :prod do backend_url: System.get_env("BACKEND_URL"), port: String.to_integer(System.get_env("PORT") || "4000"), trust_level_header: System.get_env("TRUST_LEVEL_HEADER") || "x-trust-level", - trust_level_source: System.get_env("TRUST_LEVEL_SOURCE") || "header" + trust_level_source: System.get_env("TRUST_LEVEL_SOURCE") || "header", + + # mTLS listener (Phase B). When TRUST_LEVEL_SOURCE=mtls these three paths + # MUST all be set and readable or the application refuses to start + # (fail-closed -- see HttpCapabilityGateway.Application.http_listeners/1). + tls_port: String.to_integer(System.get_env("GATEWAY_TLS_PORT") || "4443"), + mtls_ca_cert_path: System.get_env("MTLS_CA_CERT_PATH"), + gateway_cert_path: System.get_env("GATEWAY_CERT_PATH"), + gateway_key_path: System.get_env("GATEWAY_KEY_PATH") end diff --git a/docs/mtls-rotation-runbook.md b/docs/mtls-rotation-runbook.md new file mode 100644 index 0000000..ae1e8f2 --- /dev/null +++ b/docs/mtls-rotation-runbook.md @@ -0,0 +1,100 @@ + + +# mTLS CA Selection & Certificate Rotation Runbook + +**Phase:** B (`hyperpolymath/standards#97`) — mTLS as the primary trust-level path +**Applies to:** `http-capability-gateway` deployed as BoJ tier-2 (ADR 0004) +**Companion:** `boj-server` `docs/integration/http-capability-gateway-plan.md` §Phase B + +--- + +## 1. CA selection decision + +Phase B deliverable B3 requires a committed decision on which CA roots the +mTLS trust chain. The options evaluated in the integration plan: + +| Option | Decision | +|---|---| +| 1. BoJ-own CA (self-signed root, generated at deploy) | **Adopted for initial wiring.** No external dependency; the gateway and the BoJ gnosis-handler container are the only relying parties, so a dedicated single-purpose root is the smallest trust base. | +| 2. Estate SDP CA | Deferred. Adopt once an estate-wide SDP CA exists; migration is a CA-file swap (§4) with no gateway code change. | +| 3. Cloudflare Origin CA (AOP parity) | Complementary, not a replacement. Cloudflare Authenticated Origin Pulls protect the edge→origin hop; the gateway mTLS protects the gateway→BoJ hop. Both may run; they trust different roots. | + +**Authenticated Origin Pulls parity.** The gateway's HTTPS listener is +configured with `verify: :verify_peer` and `fail_if_no_peer_cert: true` +(`HttpCapabilityGateway.Application.tls_socket_opts/0`). A client that does +not present a certificate chaining to `MTLS_CA_CERT_PATH` is rejected at the +TLS handshake — the gateway mirrors the Cloudflare AOP "reject unauthenticated +origin clients" model one tier inward. + +## 2. Environment contract + +The gateway reads TLS material from three environment variables. When +`TRUST_LEVEL_SOURCE=mtls` all three are **mandatory**: if any is missing or +unreadable the application refuses to start (fail-closed — it never silently +downgrades to the forgeable header path). + +| Variable | Meaning | +|---|---| +| `MTLS_CA_CERT_PATH` | PEM CA bundle the client cert chain is verified against | +| `GATEWAY_CERT_PATH` | The gateway's own TLS server certificate | +| `GATEWAY_KEY_PATH` | Private key for `GATEWAY_CERT_PATH` | +| `GATEWAY_TLS_PORT` | HTTPS listener port (default `4443`) | +| `TRUST_LEVEL_SOURCE` | `mtls` to make the HTTPS listener mandatory | + +Trust mapping (`Gateway.determine_trust_level_from_cert/2`): a verified client +cert with `OU=Internal Services` → `internal`; any other verified client cert +→ `authenticated`; unverified / no TLS → `untrusted`. + +## 3. Certificate generation + +Production certificates are generated by estate tooling. The shape required: + +- **CA**: a long-lived (e.g. 5y) RSA-2048+ or EC-P256 self-signed root. +- **Gateway server cert**: SAN must cover the gateway's service name. +- **Client certs** (one per calling service): subject `OU` carries the + trust class. `OU=Internal Services` grants `internal`. Subjects MUST be + UTF8String-encoded — the gateway's RDN matcher only reads `utf8String` + attribute values (see `test/fixtures/mtls/gen-test-ca.sh` for the exact + `string_mask = utf8only` recipe used by the test CA). + +## 4. Rotation without downtime + +The gateway re-reads TLS files only on listener (re)start. Rotate with a +rolling restart, not an in-process reload: + +1. **Stage new material** alongside the old (new paths or a versioned dir). +2. **Cross-sign / dual-trust window.** If rotating the *CA*, publish a + `MTLS_CA_CERT_PATH` bundle containing **both** the old and new roots. + Both old and new client certs validate during the overlap. +3. **Roll the gateway.** Update the gateway deployment env to the new + `GATEWAY_CERT_PATH`/`GATEWAY_KEY_PATH`; k9-svc performs a rolling replace. + The old replica drains in-flight requests before exit (circuit breaker + trips closed on the old replica, not the seam). +4. **Roll the BoJ-side client certs** the same way against the dual-trust + bundle. +5. **Retire the old root.** Once every client presents a new-root cert, + publish a `MTLS_CA_CERT_PATH` bundle containing only the new root and + roll the gateway once more. + +At no point is there a window where the gateway accepts an unverified client: +each step keeps `verify: :verify_peer` + `fail_if_no_peer_cert: true` in force. + +## 5. Failure & rollback + +| Symptom | Likely cause | Action | +|---|---|---| +| Gateway refuses to start, log `mTLS listener configuration invalid` | A TLS path is unset/unreadable under `TRUST_LEVEL_SOURCE=mtls` | Restore the path or roll back the deployment env to the previous material | +| All clients get TLS handshake failure after a rotation | CA bundle replaced before clients rotated | Re-publish the dual-trust bundle (step 2) and re-roll | +| A specific service gets `untrusted` unexpectedly | Client cert subject not UTF8String, or wrong `OU` | Re-issue that client cert per §3 | + +Full traffic-bypass rollback (re-route around the gateway entirely) is the +`docs/integration/gateway-rollback-runbook.md` Phase E deliverable; this +runbook covers only the certificate/CA layer. + +## 6. Test fixtures + +`test/fixtures/mtls/` contains a self-contained **test** CA (root, gateway +server cert, an internal-OU client, an ordinary client, and a rogue-CA client +that must fail verification). Regenerate with +`test/fixtures/mtls/gen-test-ca.sh`. These keys are committed deliberately for +the test suite and chain to nothing trusted in production. diff --git a/lib/http_capability_gateway/application.ex b/lib/http_capability_gateway/application.ex index dcccfca..737c46e 100644 --- a/lib/http_capability_gateway/application.ex +++ b/lib/http_capability_gateway/application.ex @@ -38,46 +38,58 @@ defmodule HttpCapabilityGateway.Application do # Start HTTP server and other children port = Application.get_env(:http_capability_gateway, :port, 4000) - children = [ - # Prometheus metrics exporter - {TelemetryMetricsPrometheus.Core, metrics: telemetry_metrics()}, - - # VeriSimDB async audit log client -- started early so that the - # ETS buffer table (:capgw_verisimdb_buffer) exists before the - # first request arrives. Writes are fire-and-forget casts. - {VeriSimDB, []}, - - # Circuit breaker FSM -- started BEFORE Minikaran and the HTTP - # server so its ETS table (:gateway_circuit_breaker) exists before - # the first request arrives. The gateway calls allow?/1 on every - # request, so the table must be available from startup. - {CircuitBreaker, []}, - - # Minikaran traffic anomaly detector -- started BEFORE the HTTP - # server so its telemetry handlers are attached before the first - # request arrives. This ensures zero observation loss at startup. - {Minikaran, name: Minikaran}, - - # HTTP server with our Gateway router - {Plug.Cowboy, scheme: :http, plug: HttpCapabilityGateway.Gateway, options: [port: port]} - ] - - opts = [strategy: :one_for_one, name: HttpCapabilityGateway.Supervisor] - - Logger.info("Starting HTTP Capability Gateway", port: port) - - # Attach Minikaran telemetry handlers after supervision tree starts. - # We use a callback to ensure handlers are attached only after - # the Minikaran GenServer is alive and ready to receive casts. - result = Supervisor.start_link(children, opts) - - case result do - {:ok, _pid} -> - Minikaran.TelemetryHandler.attach() - result - - error -> - error + # Build the listener child specs. When trust_level_source is "mtls", + # a valid TLS listener is mandatory; http_listeners/1 returns + # {:error, reason} and the application refuses to start (fail-closed) + # rather than silently falling back to the forgeable header path. + with {:ok, listeners} <- http_listeners(port) do + children = + [ + # Prometheus metrics exporter + {TelemetryMetricsPrometheus.Core, metrics: telemetry_metrics()}, + + # VeriSimDB async audit log client -- started early so that the + # ETS buffer table (:capgw_verisimdb_buffer) exists before the + # first request arrives. Writes are fire-and-forget casts. + {VeriSimDB, []}, + + # Circuit breaker FSM -- started BEFORE Minikaran and the HTTP + # server so its ETS table (:gateway_circuit_breaker) exists before + # the first request arrives. The gateway calls allow?/1 on every + # request, so the table must be available from startup. + {CircuitBreaker, []}, + + # Minikaran traffic anomaly detector -- started BEFORE the HTTP + # server so its telemetry handlers are attached before the first + # request arrives. This ensures zero observation loss at startup. + {Minikaran, name: Minikaran} + ] ++ listeners + + opts = [strategy: :one_for_one, name: HttpCapabilityGateway.Supervisor] + + Logger.info("Starting HTTP Capability Gateway", port: port) + + # Attach Minikaran telemetry handlers after supervision tree starts. + # We use a callback to ensure handlers are attached only after + # the Minikaran GenServer is alive and ready to receive casts. + result = Supervisor.start_link(children, opts) + + case result do + {:ok, _pid} -> + Minikaran.TelemetryHandler.attach() + result + + error -> + error + end + else + {:error, reason} -> + Logger.error( + "mTLS listener configuration invalid; refusing to start (fail-closed)", + error: inspect(reason) + ) + + {:error, {:listener_config_invalid, reason}} end {:error, reason} -> @@ -86,6 +98,105 @@ defmodule HttpCapabilityGateway.Application do end end + # Build the HTTP/HTTPS listener child specs. + # + # The plaintext HTTP listener is always started: it serves the development + # header-trust path and unauthenticated public routes. The mTLS HTTPS + # listener is started in addition whenever TLS material is configured. + # + # Trust-level-source contract (the Phase B security invariant): + # + # * "header" (default) -- HTTP listener only. Header trust is for + # development and for public routes behind a trusted edge. + # + # * "mtls" -- the HTTPS listener with `verify: :verify_peer` and + # `fail_if_no_peer_cert: true` is MANDATORY. If the TLS material is + # missing or unreadable we return {:error, _} so the application + # refuses to start. We never silently downgrade an mTLS deployment to + # the forgeable header path. + defp http_listeners(port) do + http = {Plug.Cowboy, scheme: :http, plug: HttpCapabilityGateway.Gateway, options: [port: port]} + + trust_source = Application.get_env(:http_capability_gateway, :trust_level_source, "header") + + case tls_socket_opts() do + {:ok, tls_opts} -> + tls_port = Application.get_env(:http_capability_gateway, :tls_port, 4443) + + https = + {Plug.Cowboy, + scheme: :https, + plug: HttpCapabilityGateway.Gateway, + options: [port: tls_port] ++ tls_opts} + + Logger.info("mTLS listener enabled", tls_port: tls_port, verify: :verify_peer) + {:ok, [http, https]} + + :no_tls when trust_source == "mtls" -> + {:error, + "trust_level_source is \"mtls\" but TLS material is not configured. " <> + "Set MTLS_CA_CERT_PATH, GATEWAY_CERT_PATH and GATEWAY_KEY_PATH."} + + :no_tls -> + {:ok, [http]} + + {:error, _reason} = err when trust_source == "mtls" -> + err + + {:error, reason} -> + Logger.warning( + "TLS material configured but unreadable; starting HTTP listener only", + error: inspect(reason) + ) + + {:ok, [http]} + end + end + + # Resolve the Cowboy TLS socket options from the environment. + # + # Returns: + # * {:ok, opts} -- all three paths set and the files exist + # * :no_tls -- no TLS material configured at all + # * {:error, reason} -- partially configured or files missing + # + # `verify: :verify_peer` + `fail_if_no_peer_cert: true` makes the TLS + # handshake itself reject any client that does not present a certificate + # chaining to `cacertfile`. A request that reaches the Plug pipeline over + # this listener has therefore already had its client certificate chain + # verified by the transport (see Gateway.is_cert_verified/1). + defp tls_socket_opts do + ca = Application.get_env(:http_capability_gateway, :mtls_ca_cert_path) + cert = Application.get_env(:http_capability_gateway, :gateway_cert_path) + key = Application.get_env(:http_capability_gateway, :gateway_key_path) + + cond do + is_nil(ca) and is_nil(cert) and is_nil(key) -> + :no_tls + + is_nil(ca) or is_nil(cert) or is_nil(key) -> + {:error, + "incomplete TLS configuration: MTLS_CA_CERT_PATH, GATEWAY_CERT_PATH " <> + "and GATEWAY_KEY_PATH must all be set together"} + + true -> + missing = Enum.reject([ca, cert, key], &File.exists?/1) + + if missing == [] do + {:ok, + [ + cacertfile: ca, + certfile: cert, + keyfile: key, + verify: :verify_peer, + fail_if_no_peer_cert: true + ]} + else + {:error, "TLS files not found: #{Enum.join(missing, ", ")}"} + end + end + end + # Load policy from file or BoJ catalog, validate, and compile. # Resolution order: # 1. BOJ_CARTRIDGES_ROOT env var — catalog mode (auto-policy from cartridge.json) diff --git a/lib/http_capability_gateway/gateway.ex b/lib/http_capability_gateway/gateway.ex index 83da774..89e6592 100644 --- a/lib/http_capability_gateway/gateway.ex +++ b/lib/http_capability_gateway/gateway.ex @@ -604,7 +604,12 @@ defmodule HttpCapabilityGateway.Gateway do # that would break if OTP ever extends the record layout. This is the # production-grade replacement for the earlier approximation that matched # on {:Certificate, _, subject, _, _, _, _}. - defp extract_cert_subject(cert_der) when is_binary(cert_der) do + # + # `@doc false` (public but internal): exposed so the mTLS test suite can + # drive it with real test-CA DER without a live TLS socket. Not part of + # the supported public API. + @doc false + def extract_cert_subject(cert_der) when is_binary(cert_der) do try do cert = :public_key.pkix_decode_cert(cert_der, :otp) @@ -670,18 +675,52 @@ defmodule HttpCapabilityGateway.Gateway do end) end - # Check if certificate was verified - defp is_cert_verified(conn) do - # In a real implementation, check if certificate passed verification - # For now, assume verified if certificate is present + # Check whether the client certificate was actually verified by the + # TLS transport -- NOT merely present. + # + # The mTLS listener is configured (Application.tls_socket_opts/0) with + # `verify: :verify_peer` and `fail_if_no_peer_cert: true`. With that + # configuration the TLS handshake itself rejects any peer that does not + # present a certificate chaining to the configured CA. Chain validation + # is therefore a transport-level guarantee: a request can only reach this + # Plug pipeline over the HTTPS listener if its client certificate already + # verified during the handshake. + # + # The previous implementation returned `true` whenever ANY certificate + # was present. That is forgeable: a request arriving over the plaintext + # HTTP listener could carry an attacker-supplied DER blob and be treated + # as verified. We now fail closed unless ALL of the following hold: + # + # 1. the request arrived over TLS (`conn.scheme == :https`), so it came + # through the verify_peer listener and not the plaintext one; + # 2. the adapter is the Cowboy adapter (the only adapter that can have + # performed the TLS peer verification); + # 3. a non-empty peer certificate is present (redundant given + # verify_peer + fail_if_no_peer_cert, but checked explicitly as + # defence in depth and to reject empty/:undefined cert values). + # + # We deliberately do NOT reach into Cowboy's opaque request map to + # re-derive the SSL session: chain validation already happened at the + # handshake, Cowboy does not surface a post-handshake "verify result" + # field, and depending on undocumented internal keys would be fragile + # across Cowboy versions. The scheme + adapter + cert-presence triple is + # the sound, stable signal. + defp is_cert_verified(%Plug.Conn{scheme: :https, adapter: {Plug.Cowboy.Conn, _req}} = conn) do case get_peer_cert(conn) do - {:ok, _} -> true + {:ok, cert} when is_binary(cert) and byte_size(cert) > 0 -> true _ -> false end end - # Determine trust level from certificate attributes - defp determine_trust_level_from_cert(subject, verified) do + defp is_cert_verified(_conn), do: false + + # Determine trust level from certificate attributes. + # + # `@doc false` (public but internal): exposed for the mTLS test suite so + # the cert->trust mapping can be proven against real test-CA certs. Not + # part of the supported public API. + @doc false + def determine_trust_level_from_cert(subject, verified) do cond do # Internal services: verified cert from internal CA with specific OU verified and Map.get(subject, :organizational_unit) == "Internal Services" -> diff --git a/src/abi/MTLSPolicy.idr b/src/abi/MTLSPolicy.idr new file mode 100644 index 0000000..76a2f0a --- /dev/null +++ b/src/abi/MTLSPolicy.idr @@ -0,0 +1,46 @@ +-- SPDX-License-Identifier: PMPL-1.0-or-later +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- Phase B (standards#97) deliverable B4: the mTLS trust-policy proof +-- OBLIGATION, stated in Idris2 terms. The proof itself is NOT due in +-- Phase B -- status is "pending Phase C/D" in PROOFS_NEEDED.md. This +-- module is intentionally NOT listed in gateway.ipkg `modules`; it +-- records the claim so it cannot be lost, without gating the build. +-- +-- No `believe_me`. The obligation is left as a `0 Postulate` documented +-- below; discharging it is the Phase C/D task. + +module MTLSPolicy + +||| Transport-level verification status as established by the Cowboy TLS +||| listener configured with `verify: :verify_peer` and +||| `fail_if_no_peer_cert: true`. +data Verified = CertVerified | CertUnverified + +||| The trust classes the gateway forwards as `X-Trust-Level`, mirroring +||| HttpCapabilityGateway.SafeTrust (proven/SafeTrust.idr). +data Trust = Untrusted | Authenticated | Internal + +||| The organizational-unit string carried in the client certificate +||| subject. `IsInternalOU` marks `OU = "Internal Services"`. +data OU = IsInternalOU | OtherOU + +||| The gateway's cert -> trust decision function, as implemented in +||| Gateway.determine_trust_level_from_cert/2. +classify : Verified -> OU -> Trust +classify CertUnverified _ = Untrusted +classify CertVerified IsInternalOU = Internal +classify CertVerified OtherOU = Authenticated + +||| PROOF OBLIGATION (pending Phase C/D): +||| +||| No certificate that failed transport verification can ever be mapped +||| to a privileged trust class. Formally: for every organizational unit +||| `ou`, `classify CertUnverified ou = Untrusted`. +||| +||| This is the security core of mTLS-as-primary-path: header forgery and +||| unverified client certs are indistinguishable from anonymous traffic. +||| The statement is total and decidable; the discharge is scheduled with +||| the Phase C end-to-end verification work. +0 unverifiedNeverPrivileged : (ou : OU) -> classify CertUnverified ou = Untrusted +unverifiedNeverPrivileged ou = ?unverifiedNeverPrivileged_rhs diff --git a/test/fixtures/mtls/ca.crt b/test/fixtures/mtls/ca.crt new file mode 100644 index 0000000..edcee4d --- /dev/null +++ b/test/fixtures/mtls/ca.crt @@ -0,0 +1,20 @@ +-----BEGIN CERTIFICATE----- +MIIDSzCCAjOgAwIBAgIUGc/btNpawJeQQpTHr4nJjRPudrYwDQYJKoZIhvcNAQEL +BQAwNTEYMBYGA1UECgwPQm9KIFRlc3QgRXN0YXRlMRkwFwYDVQQDDBBCb0ogVGVz +dCBSb290IENBMB4XDTI2MDUxOTA2MTQyOFoXDTM2MDUxNjA2MTQyOFowNTEYMBYG +A1UECgwPQm9KIFRlc3QgRXN0YXRlMRkwFwYDVQQDDBBCb0ogVGVzdCBSb290IENB +MIIBIjANBgkqhkiG9w0BAQEFAAOCAQ8AMIIBCgKCAQEAtSr4s4Vc3DIjIUBURJAS +1eI33QEOQ8syLXHd9d9Gxcp6RcoM47k+aCGwPJYAj/iAGFe3CKzjzS9ziPpqoDAE +JKsZaXKe0sMv5wVNyILoeV+Qs/f66CxXBkNPsPddNi+wIG48OSN+azUP/CakN6Dq +0If3+AVu7w2c7uiiDEIGRKZIPXaIkGdOOwKjihRn9tqJVCJ6as/dXilZ9zpWamUh +sGRP/batshoLQVz+fwRyga0foXge3wr6VuJnSGiYTN4AqaN8pn5V8TST/X/i+x/g ++V5gdwgL0QX5rhBAfPa2OBvoPcooxvlHTZMMwgjxCyUJL7LsUC5RLSbsDd8XDT7B +JwIDAQABo1MwUTAdBgNVHQ4EFgQUVI6CQzUur1K2zTiP48bnBOO7BekwHwYDVR0j +BBgwFoAUVI6CQzUur1K2zTiP48bnBOO7BekwDwYDVR0TAQH/BAUwAwEB/zANBgkq +hkiG9w0BAQsFAAOCAQEAdZ2NhEm4KKLrbhe6YkDWwJnaUynFYMmJ18UxT+RBkgkb +ggAWVPTQAJnrd414WSPCFqtJkEmncLdW2qVR6VVrNsSRkT14mdkSpyfTPSc4XYRP +RDROVgRhHq0Iiqaaxe1FTfZ6H8RrkrFgFiacyhJT105laH5pW768upX+ONqgsxnb +Q8dVYU2UtPM42oq5cjoSAla6CRbgqN4t45IiGOXU65mAh++8ERXDCFkJ2jXOsPYW +WESAWPUakvTHZ9T2wfwnQLdHffeJPKxy5SA3ux5yG2fcP3pOC/Sh+//PFpgbLn4q +27Y5oQN3D00rUEqiqZrhB8utxsGAPr46mhIDrLoxmA== +-----END CERTIFICATE----- diff --git a/test/fixtures/mtls/client-auth.crt b/test/fixtures/mtls/client-auth.crt new file mode 100644 index 0000000..faff6d0 --- /dev/null +++ b/test/fixtures/mtls/client-auth.crt @@ -0,0 +1,19 @@ +-----BEGIN CERTIFICATE----- +MIIDBTCCAe0CFHjnRnDfdurz/kIofy3EDsFa5fyNMA0GCSqGSIb3DQEBCwUAMDUx +GDAWBgNVBAoMD0JvSiBUZXN0IEVzdGF0ZTEZMBcGA1UEAwwQQm9KIFRlc3QgUm9v +dCBDQTAeFw0yNjA1MTkwNjE0MjlaFw0zNjA1MTYwNjE0MjlaMEkxGDAWBgNVBAoM +D0JvSiBUZXN0IEVzdGF0ZTEUMBIGA1UECwwLQXBwbGljYXRpb24xFzAVBgNVBAMM +DnJlZ3VsYXItY2xpZW50MIIBIjANBgkqhkiG9w0BAQEFAAOCAQ8AMIIBCgKCAQEA +veWLmiWussaJmE35eS/oRJ+RQDyABFLF4CFbXjZJ3MRO/rnu2nn7RB5b0xRKxN7g +l9KAFUwRK/0y3WSzYMzdQ17fLcJXoZloZK1bCmIGst8h1JVjkYzaBfMlACH9o7vk +FCAotDhk/uwukt5edfNF30x2SadAQQexureoYLpIuVUk4RguHN5AxlVUHyJUoKYf +ta0vOWe4c3ji6XWqhXY7XMJiOm0DqMipK6nnw8qMX2sVPGnsIaJnlCVhrIzWTZ6g +ElJbgkExYpurKDejwdM8Aq2p+gCp9fQOLLD37iF77QN9RlfIEQVuBjwoi8ke5zer +IItoad7Qa9wZl0xcx2aeRQIDAQABMA0GCSqGSIb3DQEBCwUAA4IBAQA9h4EgvMRI +NsvJEV71cugN3Y7R4YeO3FrR7ladaqlOv60qG6ySFzlv3ju0xhEc2/5SAU4Wo/77 +BGwIfezdSfseaM0jv2F61Q0g8L2Wz6/dZ7MRkIB8FipAntzIu8TlsGO30lpRtWjd +mhzbOogYYvQPM6QigNmDiJzdMKU+Qtor9NDP4L369GQK3+6N5PMAfKAWJ7H7ViD9 +IrByxM2wg0kLFVE/Z3sAFCM25auI9NorVU1bTzg5AREtEdQoIIYkgmxCIIjEWtuI +EssvGXUPIIaKwkaBDDTSl1QawPDA6xWqYulypCnTzfcPfW0nWL6yAjvmn7K1Js2K +c1DvZKgKuVx2 +-----END CERTIFICATE----- diff --git a/test/fixtures/mtls/client-internal.crt b/test/fixtures/mtls/client-internal.crt new file mode 100644 index 0000000..5543835 --- /dev/null +++ b/test/fixtures/mtls/client-internal.crt @@ -0,0 +1,19 @@ +-----BEGIN CERTIFICATE----- +MIIDCTCCAfECFHjnRnDfdurz/kIofy3EDsFa5fyMMA0GCSqGSIb3DQEBCwUAMDUx +GDAWBgNVBAoMD0JvSiBUZXN0IEVzdGF0ZTEZMBcGA1UEAwwQQm9KIFRlc3QgUm9v +dCBDQTAeFw0yNjA1MTkwNjE0MjlaFw0zNjA1MTYwNjE0MjlaME0xGDAWBgNVBAoM +D0JvSiBUZXN0IEVzdGF0ZTEaMBgGA1UECwwRSW50ZXJuYWwgU2VydmljZXMxFTAT +BgNVBAMMDGludGVybmFsLXN2YzCCASIwDQYJKoZIhvcNAQEBBQADggEPADCCAQoC +ggEBAMabEajfD9V1LmW2EMjghiuNZObjXSYC9z+SGgjFEcAj2eUq+5IupcLWrBGa +CjvvB9MloaBdv5zT+5tJlHCmycH1/s7J89hBe2AFfDkwtQKfbsyHEYFVqkMz2kCc +ju6GVaMVLFvnaZYSWi8ampK59hCZADxexYqjMcWGyY3s1sbZNECP4fSwuEX6i6zC +pyE6BRgSjbH5WD6/pF6LBv+fOg9wIPdQrqqwK7OfZUBZvt28u8w5J+Mm1ZogILsH +IjtlW7/z3tgxBC96QcMCXNb2K9XRCPkbjsEnfDa7BSxGRmfycec8vCV9O7yUymCQ +YoJd+120ZlTMy4pJnD3vDCl7x40CAwEAATANBgkqhkiG9w0BAQsFAAOCAQEApVz7 +KICAZJTuUiItVz63qRB4hvSnDCuPBM8SINdn/of0BpSdJls/ObqXQZhKfGixQWJ4 +7srs8m7TwMK1G0ehLVukXh8R0eMnPKwPYtpcxXFJz48oDfniyJfzlchJnd24viaM +LD+jBDNDuktfWU9Coi9rLbhzF6Z4+7Q32w0Z58TXJdD4k7EBhGX3CkmYkIgVssw0 +5pu6r8h6c6KNmINEZFGrMQG+dNvQbckH9czPzhiQw54gOQlq+QJ1jEPTdmvN+DXi +/a8LO27vCqNed2XdEa2nmMxeLKAP81FV8naKrpD4P+0Zr1Nilpa6334TMnub+y0Q +56JagpFlpCm1DYJ8uA== +-----END CERTIFICATE----- diff --git a/test/fixtures/mtls/client-rogue.crt b/test/fixtures/mtls/client-rogue.crt new file mode 100644 index 0000000..608dd79 --- /dev/null +++ b/test/fixtures/mtls/client-rogue.crt @@ -0,0 +1,19 @@ +-----BEGIN CERTIFICATE----- +MIIDBzCCAe8CFBc6es5DOlIVBXR69dkLjdSmOukdMA0GCSqGSIb3DQEBCwUAMDcx +GDAWBgNVBAoMD0JvSiBUZXN0IEVzdGF0ZTEbMBkGA1UEAwwSUm9ndWUgVW50cnVz +dGVkIENBMB4XDTI2MDUxOTA2MTQyOVoXDTM2MDUxNjA2MTQyOVowSTEYMBYGA1UE +CgwPQm9KIFRlc3QgRXN0YXRlMRowGAYDVQQLDBFJbnRlcm5hbCBTZXJ2aWNlczER +MA8GA1UEAwwIYXR0YWNrZXIwggEiMA0GCSqGSIb3DQEBAQUAA4IBDwAwggEKAoIB +AQDSf1JxZvctiuOhYChef1Ng5IRW70DNVlSkJSCxLzde8Rah7yr7FEYI6dO6fZyv +8ANjp43GbM1gBh9bflPnyGVKSTTShEycOPVTjP/1yRjCFL6ttMYMV3SLEr8eD+Ni +Vfzj4hcW2ATdZV2+FBCpotFGRoqAHDx/5AE/CLriwOAzMR826EepcaM44eCy8mZw +r/0Kdw4oy2J+bstPTvNsBQVkyUoiWHdTGsb2Hw6scFeN/pRM1HhIvABr6rpDWEom +RiZnvkPiuBYr08AnsH5bBHXydyTyUn65L5tPNjPKs4CfRgMdPf51vpD7p5zincTs +OYN3OhI9v7HaWAn0aCGEAqVPAgMBAAEwDQYJKoZIhvcNAQELBQADggEBAHaRWXoM +l8+un18Ems0iOp3IXaQy7tpCK+yKWgNGArjiGX+HMLqQLVOhGS84hqBR2o5IjJVg +QceEqHcms/OJY7WlaJoSbWVH3BTiz2Su/3245isDzkcjocI4MBQxhRZH1vd2bbob +2Ci006CtQws+Xn8T9VHNzAm7VDQqA2PZInjEeBBpYrXs6oiTAMM4vylG5yZNgas+ +sFEQgBpZ6k9at0otvFnxZ3bxV6lDqOYkYCRIMVsfBIJSOmjJGPPkB7YjQ81gjzcS +YDe7CTjn16s4Y7nTS5wkIyYnR0BiUMjUCTENqJ3ZK4OcDEGK6pnl75FUrAvl7Zq5 +syC6ne9ZN8NHrp4= +-----END CERTIFICATE----- diff --git a/test/fixtures/mtls/gen-test-ca.sh b/test/fixtures/mtls/gen-test-ca.sh new file mode 100755 index 0000000..09d07f9 --- /dev/null +++ b/test/fixtures/mtls/gen-test-ca.sh @@ -0,0 +1,63 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: PMPL-1.0-or-later +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# Regenerate the mTLS test fixtures used by test/mtls_test.exs. +# +# THIS IS A TEST CA. The keys in this directory are intentionally committed +# so the suite needs no key material at runtime. They MUST NEVER be used for +# anything other than the gateway test suite. They chain to a throwaway root +# that is trusted by nothing in production. +# +# Subjects are forced to UTF8String (string_mask=utf8only) because the +# gateway's extract_subject_fields/1 only matches {:utf8String, value} RDNs. +# +# Generated artefacts: +# ca.crt / ca.key -- the test root CA +# server.crt / server.key -- the gateway's own TLS server cert +# client-internal.crt/.key -- client cert, OU="Internal Services" +# client-auth.crt/.key -- client cert, ordinary OU (authenticated) +# rogue-ca.crt / rogue-ca.key -- an unrelated CA (not the trust root) +# client-rogue.crt/.key -- client signed by rogue-ca (must NOT verify) +set -euo pipefail +cd "$(dirname "$0")" + +DAYS=3650 +SUBJ_BASE="/O=BoJ Test Estate" + +cfg() { # $1=cn $2=ou + cat </dev/null + openssl req -x509 -new -key "${1}.key" -days "$DAYS" -utf8 \ + -subj "${SUBJ_BASE}/CN=${2}" -out "${1}.crt" +} + +gen_leaf() { # $1=prefix $2=cn $3=ou $4=ca-prefix + openssl genrsa -out "${1}.key" 2048 2>/dev/null + openssl req -new -key "${1}.key" -utf8 -config <(cfg "$2" "$3") -out "${1}.csr" + openssl x509 -req -in "${1}.csr" -CA "${4}.crt" -CAkey "${4}.key" \ + -CAcreateserial -days "$DAYS" -out "${1}.crt" 2>/dev/null + rm -f "${1}.csr" +} + +gen_ca ca "BoJ Test Root CA" +gen_ca rogue-ca "Rogue Untrusted CA" +gen_leaf server "gateway.test.local" "Gateway" ca +gen_leaf client-internal "internal-svc" "Internal Services" ca +gen_leaf client-auth "regular-client" "Application" ca +gen_leaf client-rogue "attacker" "Internal Services" rogue-ca + +rm -f ca.srl rogue-ca.srl +echo "Test mTLS fixtures regenerated in $(pwd)" diff --git a/test/fixtures/mtls/rogue-ca.crt b/test/fixtures/mtls/rogue-ca.crt new file mode 100644 index 0000000..d2eb8a1 --- /dev/null +++ b/test/fixtures/mtls/rogue-ca.crt @@ -0,0 +1,20 @@ +-----BEGIN CERTIFICATE----- +MIIDTzCCAjegAwIBAgIUSdsK8VGVtio/NWeVOIAv0riw+FYwDQYJKoZIhvcNAQEL +BQAwNzEYMBYGA1UECgwPQm9KIFRlc3QgRXN0YXRlMRswGQYDVQQDDBJSb2d1ZSBV +bnRydXN0ZWQgQ0EwHhcNMjYwNTE5MDYxNDI4WhcNMzYwNTE2MDYxNDI4WjA3MRgw +FgYDVQQKDA9Cb0ogVGVzdCBFc3RhdGUxGzAZBgNVBAMMElJvZ3VlIFVudHJ1c3Rl +ZCBDQTCCASIwDQYJKoZIhvcNAQEBBQADggEPADCCAQoCggEBAKOQnsHucl2i1vZC +WEsfL9AayJL+sewFKIMliGaPX/c/zblT65AfBlzWNfkFKA1sW8cD295VVIu0IiKJ +72LDI4M0IswHgLPRQupn286Ow7dlFEgfbDoS6hMHzsJ9z1TDHmeu/1fi/105IW/t +LwGudCWweYHLANGCR7sFEUhSR8QFLCf6xxaHq6L5dmuLYS/tcrOqyFUOgxG8KYzi +uSuMxRT3uh5VOj1ZSHHe/28055JkgbRkBU264Ps6nhFrOiyMq1BGrMsGgk86q0SP +woLYyd6pTy+bBbhFIaqp8a2qGHs3QdgpVbesX5rpDWhwZo3FAHvcpPHq1z9pK0d9 +vZbLlkkCAwEAAaNTMFEwHQYDVR0OBBYEFAV8XNFE+xF3lt9/3jYyCAmnpELwMB8G +A1UdIwQYMBaAFAV8XNFE+xF3lt9/3jYyCAmnpELwMA8GA1UdEwEB/wQFMAMBAf8w +DQYJKoZIhvcNAQELBQADggEBAB5aPcMSFkDRBlqE2zQbNGH3qx3d7S+ECzU7rle6 +YPfsi6IlZdq2HRsaI9Pk99Q6EU4Jron8OOtmIAcWKwx2oJeWXJcVTKeu1XRdR2td +XuqhXGInwkWrIQqd0lD+/hlsQja3hUVEysaw8tmIl8m18W+2Ex1bGkmtCNldRAbj +E9+5mNzU2tSnmQfCuxQXPCqXTtsjMyrRU+CwpuF7A2ZgJAsHu+qJ9YjUoyV7BDK9 +gjQ/Bk2sheP5NrzrZKnbqMm16lpjhI5aedW1MOewQr5riEzLDDhARB88hohJOKxd +mdr9l1ertRfhl9ktS2hn8Vw9zObBtODk98F7SXuyyQDzJ1U= +-----END CERTIFICATE----- diff --git a/test/fixtures/mtls/server.crt b/test/fixtures/mtls/server.crt new file mode 100644 index 0000000..4af229e --- /dev/null +++ b/test/fixtures/mtls/server.crt @@ -0,0 +1,19 @@ +-----BEGIN CERTIFICATE----- +MIIDBTCCAe0CFHjnRnDfdurz/kIofy3EDsFa5fyLMA0GCSqGSIb3DQEBCwUAMDUx +GDAWBgNVBAoMD0JvSiBUZXN0IEVzdGF0ZTEZMBcGA1UEAwwQQm9KIFRlc3QgUm9v +dCBDQTAeFw0yNjA1MTkwNjE0MjhaFw0zNjA1MTYwNjE0MjhaMEkxGDAWBgNVBAoM +D0JvSiBUZXN0IEVzdGF0ZTEQMA4GA1UECwwHR2F0ZXdheTEbMBkGA1UEAwwSZ2F0 +ZXdheS50ZXN0LmxvY2FsMIIBIjANBgkqhkiG9w0BAQEFAAOCAQ8AMIIBCgKCAQEA +wiJtm+tsUL4QaSLyadC3XeYIO+3UqteidoC1PzY5fPqXqpXEUwxbj86FQ/imGMFu +ey9nlYUx0OCWlPSnGxssYotoouzG8+KuzAeYUWIuX354BBE4dziUXjovMolu+j9u +HkQo3PeEMs3cOUFZHNJyzow5qGxT6RfxPPZi9TgfPWZT/ySJ5Sk1iILT/8Wf2H7U +Ex2uli3VxfyKYNnnoSIMDa9fSjlyMl0YifK2xZBf2Dpz0tn3/eqksTqjJsy/k3xC +6VZ6xeCRKVWYBNYkLfzlnUYGiu80RNe4Fz28rBJdnmWzW3ZqbbIayJzaY0kbsv8X +OxMI+l0CjUEQHAkJBs7aAwIDAQABMA0GCSqGSIb3DQEBCwUAA4IBAQAHlo3COoU6 +wYz5NAkFmB2mRz6/q1sDzHfmfVLhMPESabyLzoZRPJkh+oLq6altSKL/v7N+u0be +fXs1o0v7TShsxRvvQ3jFa7RsuWoLbZn9onJGF8YR43ODjYeNVGXwzvsda0frpjkX +6MO7j6ffqA9Ey5CSrETcPjmZDiLjL5ZRDSRVmmOx4W5xed3YFfnLKtHyOMg7Tcpf +eV/r1QryYD0cJPB+CXN8UM0FHRuScceEBqBFFWsVu5G4UP9bmcAhylG/YUWpq8T/ +sHaiBB8qxwGYekr5gaJQxOoiRLrrFYeKlJCAvrbs0RcpYnUUnZ3jtZF8KkxHp5XP +29inTKVGuQR8 +-----END CERTIFICATE----- diff --git a/test/mtls_test.exs b/test/mtls_test.exs new file mode 100644 index 0000000..9de9de5 --- /dev/null +++ b/test/mtls_test.exs @@ -0,0 +1,91 @@ +# SPDX-License-Identifier: PMPL-1.0-or-later +defmodule HttpCapabilityGateway.MTLSTest do + @moduledoc """ + Phase B (standards#97) -- mTLS as the primary trust-level path. + + These tests drive the certificate -> trust-level pipeline with a REAL + test certificate authority (test/fixtures/mtls, regenerated by + gen-test-ca.sh) rather than a hand-rolled tuple. They need no live TLS + socket: the cert-parsing and trust-decision logic is exercised directly + with DER decoded from the committed fixtures, and the CA trust invariant + is proven at the crypto layer via :public_key.pkix_path_validation/3. + + The live mTLS handshake (verify_peer / fail_if_no_peer_cert) is a + transport-level guarantee asserted by the listener configuration in + HttpCapabilityGateway.Application; an end-to-end socket test across the + gateway <-> BoJ seam is Phase C (standards#98) scope per the integration + plan. + """ + + use ExUnit.Case, async: true + + alias HttpCapabilityGateway.Gateway + + @fixtures Path.join(__DIR__, "fixtures/mtls") + + defp der(name) do + [{:Certificate, der, :not_encrypted} | _] = + @fixtures + |> Path.join(name) + |> File.read!() + |> :public_key.pem_decode() + + der + end + + describe "extract_cert_subject/1 against the real test CA" do + test "pulls O, OU, CN from an internal-services client cert" do + assert {:ok, subject} = Gateway.extract_cert_subject(der("client-internal.crt")) + assert subject.organization == "BoJ Test Estate" + assert subject.organizational_unit == "Internal Services" + assert subject.common_name == "internal-svc" + end + + test "pulls a non-internal OU from an ordinary authenticated client cert" do + assert {:ok, subject} = Gateway.extract_cert_subject(der("client-auth.crt")) + assert subject.organizational_unit == "Application" + assert subject.common_name == "regular-client" + end + + test "returns a clean error on malformed DER instead of crashing" do + assert {:error, :decode_failed} = Gateway.extract_cert_subject(<<0, 1, 2, 3, 4, 5>>) + end + end + + describe "determine_trust_level_from_cert/2" do + test "verified internal-services cert -> internal" do + {:ok, subject} = Gateway.extract_cert_subject(der("client-internal.crt")) + assert Gateway.determine_trust_level_from_cert(subject, true) == "internal" + end + + test "verified ordinary cert -> authenticated" do + {:ok, subject} = Gateway.extract_cert_subject(der("client-auth.crt")) + assert Gateway.determine_trust_level_from_cert(subject, true) == "authenticated" + end + + test "unverified cert is never trusted, even with the internal OU" do + {:ok, subject} = Gateway.extract_cert_subject(der("client-internal.crt")) + assert Gateway.determine_trust_level_from_cert(subject, false) == "untrusted" + end + end + + describe "CA trust invariant (transport verify_peer at the crypto layer)" do + test "a client cert chaining to the configured CA path-validates" do + assert {:ok, _} = + :public_key.pkix_path_validation( + der("ca.crt"), + [der("client-internal.crt")], + [] + ) + end + + test "a client cert signed by an unrelated CA is rejected" do + assert {:error, _} = + :public_key.pkix_path_validation( + der("ca.crt"), + [der("client-rogue.crt")], + [] + ) + end + end +end From 1eb50b5a780f74d4a0f09140d0e738afcb1a41df Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 19 May 2026 12:58:34 +0000 Subject: [PATCH 2/2] fix(abi): drop literal believe_me token from MTLSPolicy.idr comment Hypatia code_safety greps the literal token; the comment asserted the absence of the primitive but tripped the scanner (CWE-704, 1 occurrence). Rephrased -- no behaviour change, the module uses no bypass primitive. Co-Authored-By: Claude Opus 4.7 --- src/abi/MTLSPolicy.idr | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/abi/MTLSPolicy.idr b/src/abi/MTLSPolicy.idr index 76a2f0a..01bd9bd 100644 --- a/src/abi/MTLSPolicy.idr +++ b/src/abi/MTLSPolicy.idr @@ -7,8 +7,9 @@ -- module is intentionally NOT listed in gateway.ipkg `modules`; it -- records the claim so it cannot be lost, without gating the build. -- --- No `believe_me`. The obligation is left as a `0 Postulate` documented --- below; discharging it is the Phase C/D task. +-- No verification-bypass primitives are used. The obligation is left as a +-- `0`-multiplicity metavariable (an open hole) documented below; +-- discharging it is the Phase C/D task. module MTLSPolicy