mirror of
https://github.com/block/buzz.git
synced 2026-10-28 04:51:40 +00:00
17d455a9bf
Two defects found by running a bounded state model of the composed core + LIFECYCLE machine in two encodings -- one holding every guard the documents state plus the guards a careful implementer would infer, one holding only the guards actually written. Both were invisible to four line-by-line readers because reading supplies the missing rule unconsciously. Defect 1: administrative expiry was escapable by rotation. LIFECYCLE said an expired binding "remains durable and occupies both sides of the core partial bijection", so it stays in the relation -- and core Rotate replaces one exact "active" binding with "a fresh binding version" while no document said the replacement inherits binding_not_after. Reading the expired binding as active let rotation authority alone clear a bound only expiry authority had set; reading it as inactive removed it from TargetEligible, letting ProvisionBinding double-bind the identity or bind the administratively terminated key to a different identity, violating FI-INV-01 -- the invariant LIFECYCLE was leaning on. FI-LC-ADMIN-EXPIRY did not detect either: core Rotate is authorized and version-checked, so the escape satisfied the oracle's own wording. Defect 2: nothing in the six files said what binding_not_after is a bound *on*. Two reviewers resolved it in opposite directions -- one grant-scoped, one identity-scoped -- and the readings differ by 25,200 reachable states. The identity-scoped reading also makes RetirePair followed by ordinary enrollment an escape, which under the grant-scoped reading is a legitimately new grant. Repairs: - Core Rotate states that it continues one grant onto a new key and preserves every profile-defined administrative bound as an opaque field core neither interprets nor clears. - LIFECYCLE declares the bound grant-scoped, names the transitions that establish a new grant carrying no prior bound, and points identity-scoped deadlines at the capability projection in authoritative local-policy state, which already carries the revocation-bound machinery such a deadline needs. Encoding one here instead would put an authorization-relevant deadline in a store with no revocation bound. - LIFECYCLE defines a binding with a reached bound as active for every core relation and eligibility test, closing the TargetEligible horn. - Binding-creating transitions must declare continuation or establishment; the two cases partition that set with no remainder, so a future profile cannot add a creator whose bound semantics are undefined. - FI-LC-ADMIN-EXPIRY gains the rotation-must-not-clear arm and the negative arm that retire-then-enroll yields an unbounded binding and is conformant, so the oracle no longer admits the violation it exists to catch. Verification of the shipped bytes, not the intent: re-encoding the model from this text gives 0 grant-scoped escapes (17,184 before) and 0 FI-INV-01/FI-INV-03 regressions over 282,528 states across all three enrollment policies. Each clause was mutated separately and each goes red only for its own clause -- dropping the Rotate carry restores 21,216 escapes, and dropping the active definition admits both FI-INV-01 violations. A clause that cannot be made to fail is not a guard. Co-authored-by: Tyler Longwell <tlongwell@squareup.com> Signed-off-by: Tyler Longwell <tlongwell@squareup.com>