Skip to content

Commit d2e9bab

Browse files
committed
docs(s062): PROOF.md: the gate, the coverage, and the evidence for AC1, AC2, AC4, AC5, AC7 and AC8 (AC3 and AC6 removed); the boundary refusal and the census red, each pasted from its run; the consent page and the live endpoints under proof/
Signed-off-by: Ayla Croft <aylacroft@proton.me>
1 parent 9490ffa commit d2e9bab

1 file changed

Lines changed: 283 additions & 0 deletions

File tree

Lines changed: 283 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,283 @@
1+
# Proof for slice 062: MCP authorization (client role, resource server, personal-profile authorization server)
2+
3+
Agent: Claude Opus 5 (1M context) · Date: 2026-09-22 · Branch: slice/062-mcp-auth · Final commit: written at the close, below
4+
5+
## Summary
6+
7+
Trinity's MCP server is an OAuth 2.1 resource server (`:production`, against an external
8+
authorization server the deployment names) with a small authorization server of its own for the
9+
owner's machine (`:personal`, non-default) and 061's static bearer as the default (`:local`).
10+
Trinity's client role obtains tokens from a protected server and 060's driver presents them. What
11+
was hard: a crashed session had to be recovered first (NOTES, "Recovery"), and two claims the tree
12+
made turned out not to hold until this slice made them: the personal profile's resource server
13+
checked an issuer its own issuing half never wrote, and the authorization package's `deps: []` was
14+
a claim the compiler never checked because a sub-boundary inherits its ancestors' deps (fixed as a
15+
top-level boundary; the refusal is pasted under AC7). Deferred: Enterprise Managed Authorization
16+
leaves the slice under the owner's decision of 2026-09-22 (AC3 and AC6 removed; NOTES,
17+
"Amendment"), with a lift condition; follow-ups are in NOTES.
18+
19+
## Gate
20+
21+
```
22+
$ mix gate
23+
Compiling 250 files (.ex)
24+
Generated trinity app
25+
Checking 362 source files (this might take a while) ...
26+
Analysis took 0.4 seconds (0.04s to load, 0.4s running 69 checks on 362 files)
27+
2913 mods/funs, found no issues.
28+
##############################################
29+
# Running Sobelow - v0.15.0 #
30+
##############################################
31+
... SCAN COMPLETE ...
32+
Finished in 116.7 seconds (0.6s async, 116.1s sync)
33+
Result: 524 passed, 18 excluded
34+
trinity.coverage: 050 80.31% vs 061 80.05%: OK
35+
== 1. Acceptance criteria numbered contiguously from 1 ==
36+
== 2. Definition of Done range equals the criterion count ==
37+
== 3. Manual verification queue section present ==
38+
== 4. ROADMAP size and status agree with SLICE.md ==
39+
== 5. Change-log slice count equals the tree ==
40+
== 6. No reference to a plan path absent from git ls-files ==
41+
== 6b. No slice depends on a slice that does not exist ==
42+
== 7. No board identifiers in the tree ==
43+
== 8. Commit messages: no attribution trailers, every commit signed off ==
44+
== 10. No reference to the pre-move owner path ==
45+
== 9. Secrets are ignored, as CLAUDE.md claims ==
46+
== 11. Slice lifecycle matches the branch ==
47+
== 12. Every workflow and Dependabot file parses as YAML ==
48+
plan_check: PASS
49+
gate exit 0
50+
```
51+
52+
Sobelow's traversal findings on this slice's file paths are skipped in the source with a reason
53+
each (`# sobelow_skip reason:` above every `@sobelow_skip`, which `test/sobelow_skips_test.exs`
54+
requires): every path is the host's own (the data directory, the key directory, the token store),
55+
never a request's.
56+
57+
## Tests
58+
59+
```
60+
$ mix test --cover
61+
Finished in 106.4 seconds (0.7s async, 105.7s sync)
62+
Result: 524 passed, 18 excluded
63+
| Percentage | Module |
64+
| 80.92% | Total |
65+
```
66+
67+
The slice's own files and the two MCP suites it touches:
68+
69+
```
70+
$ mix test test/trinity/mcp/auth test/trinity/mcp/server_test.exs test/trinity_web/live/mcp_live_test.exs test/trinity/mcp/boundary_test.exs
71+
Finished in 0.9 seconds (0.1s async, 0.8s sync)
72+
Result: 37 passed
73+
```
74+
75+
## Acceptance criteria evidence
76+
77+
Every criterion below is `[auto]`. AC3 and AC6 were removed on 2026-09-22 under the owner's
78+
decision (SLICE.md and NOTES.md, "Amendment"); nothing of Enterprise Managed Authorization is
79+
built, so nothing of it is proven here.
80+
81+
### AC1: RS: unauthenticated → 401 with `resource_metadata`; PRM lists our AS; wrong `aud`/expired → 401; each receipted
82+
83+
```
84+
$ mix test test/trinity/mcp/auth/token_test.exs test/trinity/mcp/auth/resource_server_test.exs --trace
85+
* test AC1: an audience-bound token the issuer signed is a principal with issuer, subject, scope and client (3.2ms)
86+
* test each claim check is its own refusal (4.3ms)
87+
* test AC1: 401 with resource_metadata; the PRM names the AS; wrong audience, expired and the static bearer are 401; each refusal receipted (20.3ms)
88+
* test introspection: an opaque token is asked about at the issuer (RFC 7662), the answer's claims checked as a JWT's are (7.4ms)
89+
* test the configuration refuses an incomplete production profile (5.7ms)
90+
* test the issuer's metadata is refused when it names another issuer (2.3ms)
91+
```
92+
93+
The refusals, each its own named error, are asserted in `token_test.exs` one at a time: wrong
94+
`iss`, missing `aud`, wrong `aud`, expired, no `exp`, `nbf` in the future, `alg` outside the allow
95+
list, a key the JWKS never held, a malformed token, and the personal profile's mark in production;
96+
`Config.new/1` refuses `none` and any `HS*` in the allow list, and refuses a production profile
97+
with no issuer or no resource. Through the endpoint (`resource_server_test.exs`) the same refusals
98+
are `401` with `WWW-Authenticate: Bearer resource_metadata="…/.well-known/oauth-protected-resource/mcp"`,
99+
the PRM at that URL names the fake enterprise AS as the authorization server, 061's static bearer
100+
is refused in this profile, each refusal leaves a decision receipt of outcome `deny`, basis `auth`,
101+
with the reason and the caller's unverified `iss`/`sub` marked as unverified, and no receipt of the
102+
session matches `eyJ`.
103+
104+
The same endpoints on a running application, in the personal profile
105+
(`scripts/dev_mcp_auth_consent.sh`; full transcript in `proof/personal-profile-endpoints.txt`):
106+
107+
```
108+
$ curl -si -X POST http://127.0.0.1:35717/mcp -H 'content-type: application/json' \
109+
-H 'mcp-protocol-version: 2026-07-28' -H 'mcp-method: server/discover' \
110+
-d '{"jsonrpc":"2.0","id":1,"method":"server/discover","params":{}}'
111+
HTTP/1.1 401 Unauthorized
112+
www-authenticate: Bearer resource_metadata="http://127.0.0.1:35717/.well-known/oauth-protected-resource/mcp"
113+
content-type: application/json; charset=utf-8
114+
115+
{"jsonrpc":"2.0","id":null,"error":{"code":-32001,"message":"Unauthorized"}}
116+
```
117+
118+
### AC2: AS: a CIMD-registered client completes code + PKCE with a resource indicator and receives an audience-bound token the RS accepts; DCR only when enabled
119+
120+
```
121+
$ mix test test/trinity/mcp/auth/embedded_test.exs --trace
122+
* test AC2: the code flow with PKCE and a resource indicator issues an audience-bound token the RS accepts; the metadata and JWKS are published; iss rides the redirect (8.1ms)
123+
* test a wrong resource, an unknown scope and a denied consent are refusals; DCR is 404 unless enabled; an unknown client is refused (34.1ms)
124+
* test DCR registers a client when enabled, and the registered client completes the flow (5.0ms)
125+
* test the personal profile refuses to start under an external authority adapter (9.5ms)
126+
* test the production profile holds no key material of its own: no keys, no JWKS, no AS metadata (4.4ms)
127+
* test rotating the signing key: a token the old key signed verifies by kid; new tokens use the new key (10.1ms)
128+
```
129+
130+
The AC2 test drives the real endpoints over HTTP: the RFC 8414 metadata (`S256` only, CIMD
131+
supported, no `registration_endpoint` while DCR is off), the JWKS, the PRM, a `401` with no token,
132+
then `GET /oauth/authorize` with `code_challenge`/`S256`/`resource`/`state`, the owner's consent
133+
form posted with its CSRF token, the redirect carrying `code`, `state` and RFC 9207 `iss`, the
134+
token endpoint with the verifier and the resource, and the resulting token accepted by the resource
135+
server at `/mcp` (200). The code is single use, a wrong verifier is `invalid_grant`, a wrong
136+
`resource` is an `invalid_target` redirect, an unknown scope `invalid_scope`, a denied consent
137+
`access_denied`, an unreachable client document a refusal, and `POST /oauth/register` is `404`
138+
until `dcr: true`. The issued token carries `"profile": "personal"`, `aud` = this server and `iss`
139+
= this server, and the production profile refuses that claim.
140+
141+
Manual view for the owner: `proof/personal-profile-consent.png` (the consent page as it renders,
142+
naming the client, the resource, the scopes asked and what a personal token is not good for).
143+
144+
### AC4: Scope mapping: `trinity:recall` cannot call an `:artifact` tool; `trinity:tools:artifact` can, subject to the gate
145+
146+
```
147+
$ mix test test/trinity/mcp/auth/resource_server_test.exs --trace
148+
* test AC4 and the receipts: read scope refused on an artifact tool, artifact scope reaches the gate, receipts name the principal, no token material (30.7ms)
149+
```
150+
151+
A token scoped `trinity:tools:read` calling the `memory` tool (`:artifact`) is answered
152+
`insufficient scope: this tool needs trinity:tools:artifact` and leaves a decision receipt of
153+
outcome `deny`, basis `scope`, reason `needs trinity:tools:artifact`, with the principal; the gate
154+
is never asked. The same call under `trinity:tools:artifact` reaches the gate and is held for the
155+
owner (`input_required`), which is the point: a scope is not an allow rule. A read tool under an
156+
allow rule runs, and both its decision and its query receipt carry
157+
`principal = %{iss, sub, scope, client_id, profile}`. No receipt and no message of the MCP session
158+
matches `eyJ`.
159+
160+
### AC5: Key rotation: old tokens verify until expiry via JWKS `kid`; new tokens use the new key
161+
162+
```
163+
$ mix test test/trinity/mcp/auth/token_test.exs --trace
164+
* test AC5: after the issuer rotates its key, old tokens verify by kid until expiry and new tokens use the new key; a key no longer published fails (3.9ms)
165+
```
166+
167+
Against the external issuer (the fake enterprise AS): after a rotation the new `kid` is unknown to
168+
the cache, one JWKS fetch follows (asserted by counting the fake's fetches), both tokens then
169+
verify, and a key withdrawn from the JWKS makes its token `{:unknown_kid, …}`. For the personal
170+
profile's own keys the same property is driven through the endpoints (`embedded_test.exs`,
171+
"rotating the signing key"): after `AuthHost.rotate_key!/0` the JWKS publishes both kids, a token
172+
signed before the rotation is still accepted at `/mcp`, and a token issued after it carries the new
173+
`kid`.
174+
175+
### AC7: `Trinity.MCP.Auth.*` has no dependency on `Trinity.Sessions`/`Trinity.Tools` (boundary check)
176+
177+
The compiler holds it. Planting the line in `test/support/mcp/planted_auth_reference.ex.txt` inside
178+
`lib/trinity/mcp/auth/scopes.ex` and compiling:
179+
180+
```
181+
$ printf '\n def planted, do: Trinity.Sessions.history("x")\n' >> …/scopes.ex # inside the module
182+
$ mix compile --force --warnings-as-errors
183+
warning: forbidden reference to Trinity.Sessions
184+
(references from Trinity.MCP.Auth to Trinity.Sessions are not allowed)
185+
lib/trinity/mcp/auth/scopes.ex:33
186+
compile exit 1
187+
```
188+
189+
That refusal only appears since this slice made the package a **top-level** boundary: a
190+
sub-boundary inherits its ancestors' deps unless it says otherwise, and `Trinity.MCP` depends on
191+
`Trinity`, so the package's `deps: []` compiled clean with the same planted line before the fix.
192+
`Trinity.MCP` now names `Trinity.MCP.Auth` as a dependency, which is the only way in.
193+
194+
The census and the no-token-material rule:
195+
196+
```
197+
$ mix test test/trinity/mcp/auth/boundary_test.exs --trace
198+
* test the boundary is top level, lists no dependency, and exports the package (2.8ms)
199+
* test the population is the package's files, and no file of it names a module of the tree in code (3.1ms)
200+
* test the one reader of the Authorization header under lib/ is the boundary; the server side never names a token (14.0ms)
201+
* test a principal's receipt form carries issuer, subject, scope, client and profile, and nothing else (0.00ms)
202+
* test the planted line the proof compiles is a real call from the package into the tree (0.1ms)
203+
```
204+
205+
The population is `git ls-files lib/trinity/mcp/auth.ex lib/trinity/mcp/auth` (thirteen files,
206+
listed in the test); the census reads each file with its comments and docs stripped and refuses any
207+
`Trinity.*` reference outside the package. Demonstrated red with the same planted line:
208+
209+
```
210+
$ mix test test/trinity/mcp/auth/boundary_test.exs
211+
1) test the population is the package's files, and no file of it names a module of the tree in code
212+
lib/trinity/mcp/auth/scopes.ex reaches the tree: ["Trinity.Sessions.history"]
213+
Result: 3/4 passed
214+
```
215+
216+
The header census derives its population from `git ls-files lib/*.ex lib/**/*.ex lib/**/*.heex`
217+
(over a hundred files, asserted) and holds that `lib/trinity/mcp/auth.ex` is the only reader of the
218+
`Authorization` header, and that no file of `lib/trinity/mcp/server*` names the header, a token or
219+
`Auth.bearer`.
220+
221+
### AC8: Client role: against a test AS the client obtains an audience-bound token the RS accepts; wrong `iss` rejected; the 060 driver performs no flow
222+
223+
```
224+
$ mix test test/trinity/mcp/auth/client_role_test.exs --trace
225+
* test AC8: 401 to challenge, PKCE against the AS, the token stored and presented, the RS accepts it (9.0ms)
226+
* test a callback from another issuer is refused; an unknown state is refused; DCR once when allowed and offered; no identity, no flow (7.0ms)
227+
* test the driver performs no flow: the census over its files (5.7ms)
228+
```
229+
230+
060's driver connects to Trinity's own `/mcp` in the production profile, is refused `401`, and
231+
records the challenge (`auth_challenge` in its info). The host begins the flow: the authorization
232+
URL names the fake enterprise AS, `response_type=code`, the configured `client_id`, `S256` with a
233+
43-character challenge, the resource and a state; the pending request on disk is mode `0600`. The
234+
AS consents, the callback is fetched as a browser would fetch it, and afterwards the token file is
235+
mode `0600`, the pending file is gone, `Client.Auth.bearer/1` returns the token, and the resource
236+
server admits it as a principal with the expected issuer, subject, scope and client. The driver
237+
then reconnects and reaches `ready` at 2026-07-28. Neither the client's info, nor the receipts, nor
238+
the MCP session's messages match `eyJ`. A callback carrying another `iss` is
239+
`{:wrong_issuer, …}`, an unknown `state` is refused, an AS error is surfaced as such, a missing
240+
client identity refuses to begin the flow, and DCR registers once and is then remembered per
241+
issuer. The census over `git ls-files lib/trinity/mcp/client.ex lib/trinity/mcp/client` holds that
242+
no file of the driver names a verifier, a challenge, an authorization or token endpoint, the
243+
client-role functions or the store.
244+
245+
The page (`/mcp`), which is all of the UI this slice added:
246+
247+
```
248+
$ mix test test/trinity_web/live/mcp_live_test.exs --trace
249+
* test a server that answered 401 with resource metadata shows the challenge; authorize sends the owner to the AS (162.1ms)
250+
```
251+
252+
## Manual verification for the reviewer
253+
254+
Nothing in the acceptance criteria requires a person: AC6, the slice's only `[manual]` criterion,
255+
was removed with AC3. Two artefacts are in `proof/` for the owner's eye rather than as criteria:
256+
257+
- `proof/personal-profile-consent.png`: the consent page in the personal profile.
258+
- `proof/personal-profile-endpoints.txt`: the PRM, the RFC 8414 metadata, the JWKS, the `401` with
259+
its challenge and the `404` from the registration endpoint, from a running application.
260+
261+
To see either again: `scripts/dev_mcp_auth_consent.sh` prints `PORT=` and the `URL=` a client would
262+
open (its database is `trinity_screenshots.db`, never the suite's). Kill it by the pid
263+
`pgrep -af beam.smp` prints.
264+
265+
## Deviations from SLICE.md
266+
267+
See NOTES.md, "Deviations from SLICE.md and the G1 plan": eight, the first being the amendment that
268+
removed Enterprise Managed Authorization and its admin UI from the slice.
269+
270+
## Versions touched
271+
272+
`VERSIONS.md` updated: yes, one row, `jose ~> 1.11` (1.11.12, MIT), added by the G1 commit and
273+
verified by the gate's `versions.verify` and `versions.gen --check` steps. No other dependency
274+
changed; `joken` was considered and not taken (NOTES, "Read before code").
275+
276+
## Git
277+
278+
```
279+
$ git log --oneline main..HEAD
280+
```
281+
282+
(The branch's commits, in order, are listed by that command; the closing commit's sha is appended
283+
below when the slice closes, as the house rule requires.)

0 commit comments

Comments
 (0)