Source-linked AI summary
When Does Authorization End? Effect Closure at Provider Boundaries
Igor Santos-Grueiro
TL;DR
Previously authorized work may still cause application-rejected effects after revocation completion, clean state, or operation success. EFFECTBOUND uses evidence-supported finite contracts to decide whether an interface can establish effect closure while required work completes, returning a strategy, impossibility certificate, or no verdict when evidence is insufficient. Across four systems, it finds missing controls, hidden active work, and premature frontiers; a Kafka gate closes the studied write path without blocking unrelated requests.
Problem
Provider completion or clean visible state can leave authorized work able to reach application-rejected effects, so the paper asks when a provider boundary can truthfully report authorization closure.
Method
EFFECTBOUND constructs an evidence-supported finite contract, models authorization paths to the effect frontier with hidden state, and decides realizability using finite control.
Results
Across GitHub, Kubernetes, NATS, and Kafka, closure fails through missing controls, hidden active work, or premature model boundaries; Effect Fence closes the studied Kafka path without blocking unrelated work.
Takeaways & Limitations
Authorization ends only when no new authorization can issue and no existing authorization can reach a rejected effect; provider-local completion alone is insufficient.
Takeaways & Limitations
Results are conditional on evidence-supported paths and continuations represented in each finite contract, and the analysis does not discover provider paths.
Abstract
from arXiv · showhide
Revocation completion, clean state, or operation success can leave authorized work able to cause an effect the application rejects while the provider stays within its contract. We call the absence of all such paths policy-relative effect closure, or effect closure for short. Thus, a grant is closed when its existing authorizations retain no such path, and it cannot issue any new ones. We present EFFECTBOUND, which uses an evidence-supported finite contract to decide whether an interface can truthfully report closure while required work completes. It reduces this to finite control with hidden state and returns a strategy, an impossibility certificate, or no verdict when evidence is insufficient. Machine-checked proofs establish the reduction and checker soundness; the checker derives closure results and validates certificates. Across GitHub, Kubernetes, NATS, and Kafka, closure fails in three ways: an interface lacks a needed control, clean visible state hides active work, or the model stops before the effect frontier---the last point where the effect can be prevented. The GitHub tool cannot bind a merge to the reviewed commit; a controlled run confirms that it may merge a different commit. NATS can report no stored or pending messages while dispatched work can still publish downstream. In Kafka, all fixed-set brokers had applied the revocation, yet an earlier authorized request could still append. We add a gate that blocks new use of revoked authority and delays return until earlier in-flight work completes. In a fixed-set Kafka~4.3.1 test deployment, this closes the studied synchronous, nontransactional write path without blocking unrelated requests. For a grant, authorization ends only when issuance stops and no earlier authorization can reach an effect the application rejects.
1. Introduction
The paper defines authorization ending in terms of policy-relative effect closure and studies whether provider boundaries can truthfully establish it while required work completes. Across four systems, closure fails when controls are missing, active work is hidden, or models stop before the effect frontier.
- Systems evidence: The GitHub MCP tool cannot bind a merge to the reviewed commit, so proceeding without a condition may merge h2 while refusal blocks required work.The native API can reject a changed head, but the tested MCP interface exposes no equivalent check.
- Systems evidence: Kafka authorizer convergence can precede append: an earlier authorized request appended after return, showing that the initial model stopped before the effect frontier.Effect Fence blocks new use of revoked authority and delays return until earlier in-flight work completes.
- Authorization and effect closure: Effect closure requires stopping new authorization issuance and eliminating paths from existing authorizations to application-rejected effects.It is distinct from local completion and quiescence, because safe work may continue.
- Systems evidence: Across GitHub, Kubernetes, NATS, and Kafka, six structural paths expose missing controls, hidden active work, and premature model boundaries.The paths include late-bound names, post-check changes, admitted execution, repeated delivery, callbacks, and distributed in-flight work.
- Analysis and contributions: EFFECTBOUND uses provider evidence to construct a finite contract, then returns a strategy, losing certificate, or UNSUPPORTED verdict for insufficient evidence.Machine-checked proofs establish the reduction and checker soundness; the checker validates 17 published certificates and derives closure results for four NATS contracts.
- Analysis and contributions: The paper identifies policy-relative semantics, frontier adequacy, and boundary realizability as the basis for truthful closure claims.Bind, Re-enter, and Fence respectively bind identity, recheck authority, or wait at the effect boundary.
2. Effect Closure at Provider Boundaries
Effect closure follows authorized work to the effect frontier, distinguishing future-use closure, instance-effect closure, and quiescence. EFFECTBOUND checks whether an evidence-supported boundary can prevent rejected effects while required work completes.
- Effect-closure semantics: Effect closure requires stopping new instances and eliminating every open carrier from an issued authorization to a rejected effect.The effect frontier is the last transition or distributed cut where prevention remains possible.
- Effect-closure semantics: The contract tracks authorization instances through continuations and records effects at their frontier crossing.Effects include policy-relevant targets, versions, payloads, principals, generations, or recipients.
- Boundary adequacy: Boundary adequacy requires representing every path from the proposed boundary to the frontier, including every intervening preventive choice.Evidence must identify the last preventive choice, rule out later choices, and track the effect consistently across model, checker, and trace.
- Boundary controls: Bind, Re-enter, and Fence address different points in the path: identity binding, post-change reauthorization, and restriction or draining of in-flight work.Updating future authorization state or observing provider state alone cannot close already authorized work.
- Closure distinctions: Future-use closure can coexist with an open carrier, while quiescence is stronger than necessary when a carrier can cross the frontier safely.Kafka demonstrates that broker-wide ACL convergence can precede an earlier request’s append.
- Claims and scope: EFFECTBOUND scopes claims to provider, interface, policy, workload, frontier, controls, evidence, and configuration, returning UNSUPPORTED when evidence is insufficient.Its claims cover contractual behavior only and require truthful claims, policy safety, and completion rather than deny-all behavior.
3. Provider-Boundary Realizability
EFFECTBOUND reduces closure at a provider boundary to finite partially observed control over an evidence-grounded contract. Realizability requires safety, truthful claims, settlement, and required completion, with certificates establishing either a winning strategy or impossibility within scope.
- Finite Boundary Model: A finite contract becomes a partially observed DES in which mediator actions are controllable, provider and environment moves are not, and observations are restricted to interface I.The construction preserves hidden state and admitted provider behavior within the contract’s stated scope.
- Assurance Boundary: Exactness is two-sided: omitted hidden behavior can create a false winner, while omitted exposed control can create a false impossibility, so insufficient evidence yields UNSUPPORTED.The contract’s empirical route inventory remains outside Lean’s machine-checked inference.
- Typed Closure Claims: Effect closure is distinct from future-use closure and quiescence: already-issued carriers may remain when every reachable effect is policy-safe.Quiescence implies effect closure, but future-use closure does not imply lineage effect closure.
- Boundary Obligations: Frontier adequacy and boundary power are separate obligations: a model must reach the effect frontier, and the exposed interface must distinguish required from unsafe worlds.An authorization twin can make safety and required completion unrealizable even when the mediator is otherwise unrestricted.
- Deciding Realizability: Realizability holds exactly when the initial information state q0 belongs to the winning region W.The winning region supports policy safety, claim safety, contract settlement, and required completion.
- Certificates: A winning certificate supplies one observation-based strategy that preserves safety, makes only true claims, and completes required work.A losing certificate instead rules out every mediator in the finite contract, while omitted provider routes remain outside the result.
4. EFFECTBOUND
EFFECTBOUND grounds finite contracts in provider evidence, machine-checks their verdicts and certificates, and separates analysis from deployment conformance. Its evaluation covers structurally distinct authorization-to-effect paths and studies Kafka repair behavior in depth.
- Grounding the Contract: EFFECTBOUND constructs an analysis contract from provider behavior, interface controls, policy, workload, authorization links, effect frontier, claims, exclusions, and repair candidates.Provider details such as target resolution, atomicity, retries, and fan-out require documentation, pinned source, controlled execution, or instrumentation.
- Checking Verdicts and Repairs: Evidence supports a finite contract or yields UNSUPPORTED; Lean validates the proposed game and untrusted solver certificates but does not infer provider semantics.The compiler and solver need not be trusted after the finite contract is constructed.
- From Certificates to Execution: The evaluation selects six authorization-to-effect paths for distinct mechanisms, with detailed scope and evidence obligations recorded per contract.The paths include mechanisms such as role-based access control and downstream publish acknowledgment.
- GitHub MCP-to-REST Path: The GitHub MCP path cannot guarantee both safe merging of reviewed head h1 and completion because the exposed interface cannot atomically bind the merge to h1.The controlled MCP run confirms late-bound behavior; the Bind candidate adds sha=h1 as an atomic merge precondition without changing public response or effect semantics.
- GitHub MCP-to-REST Path: The Bind candidate makes the checked GitHub merge safe but makes no closure claim.Native REST traces link the authorized head through the atomic check to the merged head.
5. Evaluation
The evaluation tests whether boundary interventions close authorization-to-effect paths across providers while preserving designated work. Across six paths and a focused Kafka study, matching controls eliminate challenged forbidden effects, while Kafka shows that authorizer convergence alone is insufficient.
- Study A: Study A tests six structurally different authorization-to-effect paths, asking whether matching controls eliminate forbidden effects without blocking designated work.The study covers Bind, Re-enter, and Fence placements across provider mechanisms.
- Study A: A cross-layer audit found tool forms preserved the selected policy-relevant control in 11/20 operations, omitted two, weakened two, and moved five.Native-to-SDK representations retained the control in all 20 cases.
- Study A: NATS redelivery produced two durable effects in 10/10 base schedules, while an idempotency ID bound to authorization, request, and payload committed one effect within the duplicate window.After the configured window expired, both attempts committed.
- Study A: Kubernetes rechecking after admission-state changes produced 0/30 forbidden effects and 30/30 authorized completions.The scope was one principal, RoleBinding, object, and API-server path, excluding regrant and alternate authorization.
- Study A: Across six paths, the matching Bind, Re-enter, or Fence placement eliminated the challenged forbidden path while designated authorized work completed.The result establishes structural coverage and feasibility within each path’s declared scope.
- Study B: Kafka’s Applied-State Fence established FutureUseClosed but a paused previously authorized request still appended, showing that the model stopped before the append frontier.Effect Fence instead blocks revoked use and drains earlier in-flight work to establish lineage closure.
- Study B: At concurrency 32 and 128, the old-instance fence changed throughput by −4.2% and −11.8%, with p99 increases of +10.4 and +36.5 ms.The full variant changed throughput by −18.9% and −15.0%, with p99 changes of +89.1 and +2.3 ms.
- Study B: Effect Fence established lineage closure for the declared Kafka path while unrelated work remained usable under its scoped gate.The claim covers synchronous nontransactional append to the target leader’s local log under the declared fixed controller and broker set.
6. Discussion
The discussion argues that closure claims must reach the application’s effect frontier and remain tied to their scope and configuration. It also limits the claims because modeled-path coverage cannot establish provider-wide completeness.
- Closure claims: A closure response must identify what has closed, including its subject, kind, policy, frontier, scope, and configuration.Provider-local completion does not imply application-level closure.
- Boundary controls: End-to-end mediation must preserve authorization to the effect frontier, recheck after the last policy-relevant change, or restrict and drain admitted work.The required placement depends on how identity, provider state, and admitted execution evolve.
- Repair constraints: EFFECTBOUND repairs may add state, epochs, or leases, but must preserve workload, responses, claims, and the meaning and representation of effects.A changed public claim defines a new contract, while a mediator change defines a new configuration version.
- Limitations: Provider-wide completeness remains unproved because UNSUPPORTED flags missing evidence for represented premises but cannot detect omitted paths.The construct validity of results depends on modeled paths, authorization links, the frontier, and post-return behavior.
7. Related Work
Related work studies authority lifetime, authorization–execution divergence, supplied-interface enforcement, and supervisory control. EFFECTBOUND differs by first asking what must close, whether the model reaches the effect frontier, and whether the interface can realize closure during required work.
- Existing approaches: Prior work covers revocation and ongoing use, check/use divergence, enforcement over supplied interfaces or models, commit-time authorization, and supervisory control.These approaches generally assume a monitored interface, a supplied model, or an exposed commit point.
- EFFECTBOUND: EFFECTBOUND first checks whether the chosen interface reaches the required effect frontier and exposes enough observation and control to report closure without blocking required work.Finite control begins only after these boundary questions are answered.
8. Conclusion
The conclusion separates closure from authorization-state convergence and provider-local completion. It concludes that authorization ends within scope only when no new authorization can issue and no prior authorization can still reach a rejected effect.
- Conclusion: Authorization-state convergence can coexist with admitted work reaching a rejected effect, so closure requires separate analysis of the effect frontier.EFFECTBOUND separates what must close, whether the model reaches that frontier, and whether the interface can establish the claim.
- Conclusion: Across six paths, missing controls, hidden active work, and prematurely ending models expose distinct closure failures.Kafka demonstrates that a correct proof can stop before append.
- Conclusion: Within the declared scope, a lineage ends only when it can issue no new authorization and no existing authorization can still reach a rejected effect.The claim requires named scope and configuration together with controls and tracking that make it true.
Appendix A. Open Science and Artifact Availability
The artifact provides the implementation, schemas, contracts, evidence records, study protocols, results, solver, independent checkers, and reconstruction scripts for EFFECTBOUND.
- The artifact bundles the implementation, schemas, contracts, evidence records, study protocols, results, solver, independent checkers, and reconstruction scripts.Its manifest records the submitted snapshot’s cryptographic checksum.
Appendix B. Ethics Considerations
The study uses public materials, controlled fixtures, disposable clusters, synthetic pull requests, and one managed service, while avoiding production workloads and unsolicited scanning.
- The study uses public documentation and source code, controlled fixtures, disposable Kubernetes, NATS, and Kafka clusters, and synthetic pull requests.GitHub is the only managed service.
- The study uses no production workloads, nonpublic third-party data, or unsolicited scanning.GitHub work included pinned-source inspection, 25 controlled REST replay pairs, and one end-to-end run through the official server.
- The sanitized artifact excludes credentials, private endpoints, correspondence, and identifying metadata.It supports defensive analysis without discovering paths or providing exploits; the analyst supplies the contract, policy, and scope.
Appendix C. Formal Contract Semantics and Soundness
The appendix defines an evidence-grounded finite contract, represents hidden provider-boundary state and live carriers, and formally checks closure claims and certificates.
- C.1. Exact Information States and Decision Segments: The compiler maps observed histories to finite information states that record represented worlds, controls, successors, safety, completion, provenance, carrier, and closure data.Equal states must agree on these derived data.
- C.1. Exact Information States and Decision Segments: Execution segments enumerate outcome endpoints and intermediate prefixes, allowing the checker to mark a decision unsafe when any intermediate prefix violates SafePrefix.The checker consumes the Boolean cell label rather than reconstructing provider histories.
- C.1. Exact Information States and Decision Segments: Post-settlement invariants require represented states to be settled, policy-safe, claim-safe, and closed under the prescribed successor relation.Lean checks membership, inductivity, policy safety, and claim preservation, while successor inventories remain empirical.
- C.2. Configuration History, Provenance, and Live Carriers: The contract requires evidence-linked carriers with declared authorization instances and effects, but physical outcomes and provider-inventory completeness remain empirically grounded.A represented suffix may cross the frontier with an effect outside its authorization scope, as in GitHub’s moved-head world.
- C.2. Configuration History, Provenance, and Live Carriers: Configuration changes preserve issued instances and live carriers, while unsupported creation, ambiguous termination, missing correlation, or unjustified provenance yields UNSUPPORTED.Carrier tuples are inserted on creation and removed only by represented, evidence-supported end events.
- C.3. Closure Predicates and Typed Claims: Closure predicates distinguish future-use, instance-effect, and lineage closure by checking future issuance and frontier-crossing tails from already-issued authority.A carrier is open when a tail crosses the frontier and fails the authorization-and-policy test.
- C.4. Finite Decision, Certificates, and Obstruction: The machine-checked checker establishes certificate soundness and validates 17 published certificates, while the evaluated NATS variants separate satisfying Bind and Tracked Drain from failing base and native-terminal variants.The separate Python check reports 2 winning and 15 losing verdicts.
- C.5. Deployment-to-Contract Soundness: Deployment soundness follows when a repair preserves the external contract, the mediator follows its winning strategy, and deployed traces refine the repaired finite contract.Under those assumptions, every prefix is safe and visible closure claims satisfy the contract.
Appendix D. Evidence, Scope, and Validation
The validation combines a Kafka throughput study with contract coverage and abstention audits, while explicitly limiting representativeness and applicability claims.
- The 644-line Kafka prototype processed 1,310,720 records in 160 error-free trials on a three-broker fixture.Kafka remained unmodified during the experiment.
- At c = (32, 128), Stock and full fixed-set throughput medians were (10.328, 10.319) and (8.340, 8.281) thousand records/s.The reported p99 medians and throughput ranges quantify the performance comparison.
- The 12 contracts comprise six UNREALIZABLE path contracts with repairs, two REALIZABLE controls, and four UNSUPPORTED cases.Seven of eight abstention-audit strata yielded UNSUPPORTED, without estimating applicability or prevalence.
- In a preregistered 20-operation audit, SDKs retained all native primitives, while tools preserved 11, omitted two, misplaced five, and weakened two.The selection procedure was deterministic but neither independent nor representative.
- Kafka traces link request identity, authorization epoch, broker boot, deletion, return, and local append, but cover only the studied scope.The appendix reports separate intermediate variants, startup and host conditions, recovery timings, and old-instance-fence ranges.