diff --git a/specs/ceremony-common.md b/specs/ceremony-common.md index 9bfe63e7..445bdc57 100644 --- a/specs/ceremony-common.md +++ b/specs/ceremony-common.md @@ -192,17 +192,20 @@ Attestation Count: The number of entries in the closed attestation list a each authoritative field appears exactly once at the JSON location fixed by its Platform Profile. - ASM-PROV-07: - For profiles relying on platform-side decoded-form uniqueness (X), at the - exact token endpoint and method fixed by that profile, the - Identity Platform accepts token redemption only under the profile's media - type and rejects a form body containing more than one decoded occurrence of - any profile-listed field. Necessity: launch circuits deliberately avoid - proving the complete form grammar; without this parser property a prover - could witness one `code` or `code_verifier` while the platform consumes - another. GitHub instead enforces the complete canonical request in its - Platform Verifier under REQ-PLAT-61 and does not depend on this assumption. - Evidence: recurring integration probes against each dependent profile's - production endpoint. + For a Platform Profile that reads a decoded form field from a token request + it does not hold whole, at the exact token endpoint and method fixed by that + profile, the Identity Platform accepts token redemption only under the + profile's media type and rejects a form body containing more than one + decoded occurrence of any profile-listed field. Necessity: a circuit that + extracts a field without proving the complete form grammar needs this + parser property; without it a prover could witness one `code` or + `code_verifier` while the platform consumes another. No launch profile + depends on this assumption: X and GitHub each hold the complete revealed + token body in the Platform Verifier under REQ-PLAT-63 and REQ-PLAT-61. A + future Platform Profile that reads a decoded form it does not hold whole + cites this assumption and joins the probes of REQ-COMMON-32. Evidence: + recurring integration probes against each citing profile's production + endpoint. - ASM-NOTARY-01: The configured notary key is unforgeable, signs only transcripts it observed, and stamps their creation time from a clock within ordinary skew @@ -233,13 +236,15 @@ on it. Evidence produced by a ceremony discharges only for the Authorized Transaction Data committed in its Authorization Digest. Depends on ASM-PROV-02, ASM-PROV-05, ASM-PROV-06, - ASM-PROV-07, ASM-NOTARY-01, ASM-PROOF-01, ASM-CHAIN-01. Evidence: + ASM-PROV-07 for a profile that cites it, ASM-NOTARY-01, ASM-PROOF-01, + ASM-CHAIN-01. Evidence: conformance tests (supporting, not proving) plus the collision resistance of SHA-256 and keccak256. - SP-CLIENT-01: The Canonical Runtime rejects evidence issued to an OAuth client other than the one fixed by its immutable ceremony profile. Depends on ASM-PROV-05, - ASM-PROV-07 where applicable, ASM-NOTARY-01, ASM-PROOF-01, and ASM-BROWSER-01. + ASM-PROV-07 for a profile that cites it, ASM-NOTARY-01, ASM-PROOF-01, and + ASM-BROWSER-01. Evidence: checked invariant in the Canonical Runtime, plus conformance tests (supporting). - SP-DELIVERY-01: @@ -250,8 +255,9 @@ on it. conformance tests (supporting). - SP-EXCHANGE-01: An attested token exchange redeems the authorization code produced by this - ceremony and no other. Depends on ASM-PROV-02, ASM-PROV-03, ASM-PROV-07, - ASM-NOTARY-01, ASM-PROOF-01, ASM-BROWSER-01. Evidence: conformance tests + ceremony and no other. Depends on ASM-PROV-02, ASM-PROV-03, ASM-PROV-07 + for a profile that cites it, ASM-NOTARY-01, ASM-PROOF-01, ASM-BROWSER-01. + Evidence: conformance tests (supporting, not proving). - SP-FRESH-01: Evidence older than its authenticated ceiling is rejected. Depends on @@ -652,6 +658,27 @@ attestation to verify carries no value at all. emits for the expected unencoded value. The Canonical Runtime MUST NOT compare that range directly with the unencoded value or apply a second, permissive decoder. +- REQ-COMMON-07A (upholds SP-EXCHANGE-01, SP-CLIENT-01): + The Platform Verifier MUST accept a complete revealed form body only as the + profile's listed fields in the listed order, each the literal name, `=` and + a nonempty value in the serializer's output alphabet, with `&` between + pairs and nothing after the last. The output alphabet is the bytes the + serializer passes through, `A`-`Z`, `a`-`z`, `0`-`9`, `*`, `-`, `.` and + `_`, the `+` it writes for a space, and `%` followed by two uppercase + hexadecimal digits spelling a byte that is neither passed through nor the + space. The Platform Verifier MUST NOT decode a value. The Platform Verifier + MUST NOT require that a value's escapes decode to UTF-8 or to any character + set: a value it reads is held to a charset inside the pass-through set, and + what any other value decodes to is not judged. Necessity: every byte has + one spelling under the serializer, so a body every token of which is + canonical is the serialization of what it decodes to, and a value in the + alphabet cannot become another field. REQ-COMMON-07 and this rule judge + different things by design: REQ-COMMON-07 governs what the Implementation + sends, from UTF-8 input it alone holds; this rule governs the bytes the + Platform Verifier judges. A value whose escapes decode to bytes that are + not UTF-8 is canonical and passes the Platform Verifier, though the + Implementation never emits one; a decoding check would be the second + decoder REQ-COMMON-07 forbids. - REQ-COMMON-08: The Implementation MUST emit each field listed in the platform profile exactly once, in the listed order. The Implementation MUST emit no other @@ -832,7 +859,8 @@ the value, and its closing quote. JSON unsigned integers and booleans use the typed local matches of REQ-COMMON-19D. A form-field check asserts a field boundary, the exact ASCII name and `=`, the value, and the next `&` or body end. Because authenticated response fields satisfy ASM-PROV-06, and form uniqueness -is either enforced by the Platform Verifier or assumed under ASM-PROV-07, +is enforced by the Platform Verifier over the revealed body under REQ-PLAT-61 +and REQ-PLAT-63, or assumed under ASM-PROV-07 by a profile that cites it, these local checks provide the required field meaning without the impractical proving cost of a complete JSON or form parser. Hidden ranges stay behind the pinned attestation format's range commitments; the circuit links transcripts @@ -1043,7 +1071,8 @@ which the following identity-header rules could apply. name, `=`, the charset-constrained value, and then `&` or the authenticated body end. The circuit does not scan the rest of the body for duplicates; a profile relying on the platform for that property cites ASM-PROV-07. - GitHub instead checks its fully revealed body under REQ-PLAT-61. + X and GitHub instead check their fully revealed bodies under REQ-PLAT-63 + and REQ-PLAT-61. - REQ-COMMON-19A (upholds SP-EXCHANGE-01): The Platform Verifier extracting a field from revealed attestation bytes MUST reject a transcript in which the field's full delimiter matches at @@ -1128,9 +1157,9 @@ constant. from one, as a public proof input. Disclosure alone does not enforce decoded form semantics. GitHub pairs full -request disclosure with REQ-PLAT-61's canonical, complete five-field check; -a hidden suffix or a second form field is rejected by its Platform Verifier. -X retains ASM-PROV-07 as its decoded-form soundness dependency. +request disclosure with REQ-PLAT-61's canonical, complete five-field check, +and X with REQ-PLAT-63's; a hidden suffix or a second form field is rejected +by the Platform Verifier. Neither depends on ASM-PROV-07. REQ-COMMON-22A prevents adding request credentials to the circuit's public inputs. It does not forbid revealing an intentionally public application @@ -1267,8 +1296,12 @@ the constructions that role implements. Two ceremonies over identical Authorized Transaction Data yield distinct digests, and a digest carrying a foreign `platformCeremonyVersion` is rejected. -- TEST-COMMON-05 (exercises REQ-COMMON-07, REQ-COMMON-08, REQ-COMMON-10): - The §6 serializer vector reproduces byte for byte. +- TEST-COMMON-05 (exercises REQ-COMMON-07, REQ-COMMON-07A, REQ-COMMON-08, REQ-COMMON-10): + The §6 serializer vector reproduces byte for byte. Under the canonical form + grammar a lowercase escape, an escape of a passed-through byte or of the + space, a truncated escape, a raw space or a raw delimiter in a value fails; + a value whose escapes decode to bytes that are not UTF-8 passes, and no + serializer input produces it. - TEST-COMMON-06 (exercises REQ-COMMON-09, REQ-COMMON-11): A request carrying an appended caller parameter is rejected, and a redirected notarized request is abandoned. diff --git a/specs/platform-ceremonies.md b/specs/platform-ceremonies.md index 4941f2d8..c3055899 100644 --- a/specs/platform-ceremonies.md +++ b/specs/platform-ceremonies.md @@ -433,6 +433,11 @@ sessions. | 4 | `redirect_uri` | immutable redirect URI | | 5 | `code_verifier` | PKCE verifier per common §7 | +The whole request is revealed. The table fixes field order for canonical +serialization under common §6, not to protect a hidden suffix; REQ-PLAT-63 +holds the complete body to the canonical form grammar of common +REQ-COMMON-07A. + - REQ-PLAT-29 (upholds SP-EXCHANGE-01): The Implementation MUST reveal the token request's `code` range. The Canonical Runtime MUST require that revealed serialized value to equal the @@ -445,6 +450,29 @@ sessions. identity session sends it inside a header. Necessity: the range is opened to link two attestations, so it needs a bound and a charset; the circuit verifies no other property of the token response. +- REQ-PLAT-63 (upholds SP-EXCHANGE-01, SP-BIND-01, SP-CLIENT-01): + The Prover and Platform Verifier MUST require the complete request body to + satisfy the canonical form grammar of common REQ-COMMON-07A for exactly the + five fields in the table, in that order. + The Prover and Platform Verifier MUST reject malformed encoding, noncanonical + spelling, an extra or duplicate field, or bytes outside that complete body. + The Prover and Platform Verifier MUST enforce common REQ-COMMON-16B's + charset for `client_id` and common §7's canonical unpadded base64url + encoding of exactly 32 bytes for `code_verifier`. `code` and + `redirect_uri` are nonempty values with no further constraint: the Platform + Verifier reads neither and judges only their bytes under REQ-COMMON-07A, + and the Canonical Runtime compares them with the values it serialized under + REQ-PLAT-29 and REQ-PLAT-29C. The `grant_type` value is the exact ASCII + bytes `authorization_code`, which REQ-PLAT-56 compares. No `refresh_token`, + device-flow field, or other grant field is admitted; the pinned endpoint + receives only this authorization-code request. Acceptance does not depend + on X rejecting malformed or duplicate forms. The Canonical Runtime's + comparisons of `code`, `grant_type` and `redirect_uri` under REQ-PLAT-29 + and REQ-PLAT-29C are separate local checks; the Platform Verifier's + digest-to-verifier comparison remains common REQ-COMMON-15A. Necessity: + revealing a range does not reject a form delimiter inside it, and the + circuit does not scan for duplicates under common REQ-COMMON-19C; holding + the whole body removes the platform's parser from the soundness argument. The request is one revealed range: the request line, every header and the body. The rows below name what the Platform Verifier reads out of it, not @@ -483,8 +511,8 @@ range indistinguishable from a `refresh_token` value. Those reveals and the in-circuit `code_verifier` opening of REQ-COMMON-15 reduce the hidden request surface, but revealing a range does not reject a form -delimiter inside it. The X profile therefore retains ASM-PROV-07 as a soundness -dependency. +delimiter inside it. REQ-PLAT-63 therefore holds the complete body to the exact +five-field form; X, like GitHub, does not depend on ASM-PROV-07. - REQ-PLAT-29A (upholds SP-CLIENT-01): The Implementation MUST reveal the `client_id` range of the token request in @@ -506,7 +534,8 @@ dependency. reads; the Platform Verifier compares the revealed `grant_type` itself under REQ-PLAT-56. Revealing them narrows the body a prover can compose without being observed; it does - not by itself exclude a duplicate field, which remains ASM-PROV-07. The + not by itself exclude a duplicate field, which REQ-PLAT-63 rejects over the + complete body. The Platform Verifier enforces the disclosure: an attestation hiding either range does not match the profile layout of common REQ-COMMON-17A and REQ-COMMON-18A and fails verification. @@ -756,20 +785,17 @@ forbidden by REQ-PLAT-56A. - REQ-PLAT-61 (upholds SP-EXCHANGE-01, SP-BIND-01, SP-CLIENT-01): The Prover and Platform Verifier MUST require the complete request body to - be the common §6 canonical form serialization of exactly the five fields in - the table, in that order, each occurring once with a nonempty value. + satisfy the canonical form grammar of common REQ-COMMON-07A for exactly the + five fields in the table, in that order. The Prover and Platform Verifier MUST reject malformed encoding, noncanonical spelling, an extra or duplicate field, or bytes outside that complete body. The Prover and Platform Verifier MUST enforce common REQ-COMMON-16B's - charset for `client_id`, common §7's canonical unpadded base64url encoding - of exactly 32 bytes for `code_verifier`, and printable ASCII without - whitespace for `client_secret`. The decoded `code` and `redirect_uri` are - nonempty UTF-8 strings with no additional charset restriction. - Verification: decode each value once, apply its field constraints, serialize - the ordered tuple with the common serializer, and compare the complete body - byte for byte. Field names are the exact literal names in the table. Encoded - value bytes are never reparsed as another form. A credential containing a form - delimiter is safe only as the serializer's encoded value, not as another field. + charset for `client_id` and common §7's canonical unpadded base64url + encoding of exactly 32 bytes for `code_verifier`. `code`, `redirect_uri` + and `client_secret` are nonempty values with no further constraint: the + Platform Verifier reads none of them and judges only their bytes under + REQ-COMMON-07A, and the Prover compares `code` and `redirect_uri` with the + values it serialized under REQ-PLAT-46 and REQ-PLAT-48A. No `grant_type`, `refresh_token`, device-flow field, or other extension is admitted; the pinned endpoint receives only this authorization-code request. Acceptance does not depend on GitHub rejecting malformed or duplicate forms. @@ -1139,7 +1165,7 @@ Platform Verifier, Notary Service, Consumer. - TEST-PLAT-09B (exercises REQ-PLAT-30A, REQ-PLAT-32A): An X transcript that reveals plaintext `access_token` bytes in either session, or omits the bearer hash commitment, is rejected. -- TEST-PLAT-09C (exercises REQ-PLAT-29C, REQ-PLAT-56, REQ-PLAT-56A, REQ-PLAT-56B, REQ-PLAT-56C): +- TEST-PLAT-09C (exercises REQ-PLAT-29C, REQ-PLAT-56, REQ-PLAT-56A, REQ-PLAT-56B, REQ-PLAT-56C, REQ-PLAT-63): The Platform Verifier rejects an X attestation that hides the `grant_type` or `redirect_uri` range, and the Canonical Runtime rejects a revealed value differing from the canonical form serialization of its deployment profile. @@ -1158,7 +1184,19 @@ Platform Verifier, Notary Service, Consumer. count that is not the body's length, is not decimal digits, or carries a leading zero, and accepts the count wherever it sits in the head; and it rejects a head carrying a bare line feed, a bare carriage return, an - obsolete line fold, or a line with no colon. + obsolete line fold, or a line with no colon. The canonical five-field body + passes; missing, empty, additional, duplicate, reordered, malformed, or + noncanonical fields fail even if X were to accept them. Encoded duplicate + names cannot evade the exact name/serialization check. A value with encoded + delimiters remains one value and passes; raw delimiters creating more + fields fail. Refresh or device-grant fields fail. Invalid + client-identifier bytes and a noncanonical or wrong-length PKCE verifier + fail. Canonical form escaping in `code` and `redirect_uri` passes the form + check; a mismatch with the consumed code or the deployment profile's + redirect still fails under REQ-PLAT-29 and REQ-PLAT-29C. A `code` or + `redirect_uri` whose canonical escapes decode to bytes that are not UTF-8 + passes the form check, which the Implementation never emits, and fails + those comparisons. - TEST-PLAT-10 (exercises REQ-PLAT-30, REQ-PLAT-31, REQ-PLAT-32, REQ-PLAT-36, REQ-PLAT-51, REQ-PLAT-52): An opened bearer range that is empty, over 4096 bytes, or outside printable ASCII fails to prove; a revealed identity response missing `id` or the @@ -1180,10 +1218,13 @@ Platform Verifier, Notary Service, Consumer. exact name/serialization check. A credential with encoded delimiters remains one value and passes; raw delimiters creating more fields fail. Refresh or device-grant fields fail. All accepted lengths cover the complete body. - Invalid client-identifier bytes, a noncanonical or wrong-length PKCE verifier, - and invalid UTF-8 in `code` or `redirect_uri` fail. Canonical form escaping in - those two strings passes the form check; a mismatch with the captured code - or frozen redirect still fails the Prover's local comparisons. + Invalid client-identifier bytes and a noncanonical or wrong-length PKCE + verifier fail. Canonical form escaping in `code` and `redirect_uri` passes + the form check; a mismatch with the captured code or frozen redirect still + fails the Prover's local comparisons. A `client_secret` whose canonical + escapes decode to bytes that are not UTF-8 passes: the Platform Verifier + judges its bytes and decodes nothing. The same in `code` or `redirect_uri` + passes the form check and fails the Prover's local comparisons. - TEST-PLAT-13 (exercises REQ-PLAT-37, REQ-PLAT-38, REQ-PLAT-62): Prover sends the frozen client/credential/redirect and ceremony code/verifier through its token Proxy session, using the same selected notary as identity. @@ -1249,11 +1290,13 @@ Platform Verifier, Notary Service, Consumer. before any token request starts, as is a redirect whose `state` matches no live local ceremony or a ceremony already consumed. - TEST-PLAT-19 (exercises REQ-COMMON-32; supports ASM-PROV-07): - Recurring integration probes send each profile-listed X token - request field twice, in both orders and using both literal and percent-encoded - equivalent field names, and send the otherwise valid request under alternate - media types. The production endpoint rejects every probe and issues no - bearer. + For each production Platform Profile that cites ASM-PROV-07, recurring + integration probes send each profile-listed token request field twice, in + both orders and using both literal and percent-encoded equivalent field + names, and send the otherwise valid request under alternate media types. + The production endpoint rejects every probe and issues no bearer. No launch + profile cites ASM-PROV-07: X and GitHub hold the complete token body under + REQ-PLAT-63 and REQ-PLAT-61, so the launch probe set is empty. - TEST-PLAT-21 (exercises REQ-PLAT-38, REQ-PLAT-49, REQ-PLAT-55): A same-session bearer opening opens the token attestation commitment; a missing, mismatched, or other-session opening fails. The opening remains @@ -1301,11 +1344,11 @@ platform behavior rather than a proven property. The Implementation claiming conformance MUST run a recurring check that each platform still rejects a mismatched `code_verifier`. -X still relies on ASM-PROV-07 for decoded-form uniqueness and uses -TEST-PLAT-19's recurring probes. GitHub instead rejects noncanonical or extra -fields over its fully revealed request under REQ-PLAT-61; it no longer relies -on GitHub rejecting duplicate fields. Both still assume the platform honors -the canonical request, PKCE, and one-use authorization-code semantics. +X and GitHub each reject noncanonical, extra or duplicate fields over the +fully revealed token request, under REQ-PLAT-63 and REQ-PLAT-61; neither +depends on ASM-PROV-07, and TEST-PLAT-19 has no launch profile to probe for +it. Both still assume the platform honors the canonical request, PKCE, and +one-use authorization-code semantics. The Prover can withhold work or supply malformed evidence. Local request and commitment checks detect structural substitution, not a well-formed forged