← All papers
First page of When Does Authorization End? Effect Closure at Provider Boundaries

When Does Authorization End? Effect Closure at Provider Boundaries

Igor Santos-Grueiro

cs.CR Sep 2, 2026 · v1 cs.DC
Lean 4 machine-checks the reduction from closure to finite games, certificate soundness, contract-to-game translations, and Kafka Effect Fence invariants.
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.

Revocation completion, clean visible state, or operation success at provider boundaries can still leave previously authorized work able to cause effects the application rejects. The paper asks when an interface can truthfully report that authorization has ended, a property it calls policy-relative effect closure.

EffectBound builds an evidence-supported finite contract of the provider path from grant to authorization instance, continuation, effect frontier, and effect. It reduces boundary realizability to control of a partially observed discrete-event system, which yields a winning strategy, an impossibility certificate, or abstention when evidence is insufficient. Lean 4 machine-checks the reduction, certificate soundness, the contract-to-game translations, and the closure derivations. Three repair placements (Bind, Re-enter, Fence) are evaluated on GitHub MCP, Kubernetes, NATS, and Kafka.

Six paths fail closure through missing controls, hidden active work, or models that stop before the effect frontier. All repairs reduce forbidden effects to zero while required work still completes. Lean validates all 17 translated game certificates (2 winning, 15 losing), and Kafka's Effect Fence closes the studied synchronous write path without blocking unrelated requests.

PathBaseRepairRepairedComplete
GitHub MCP-to-REST25/25Bind SHA0/2525/25
NATS redelivery10/10Bind ID0/1010/10
Kubernetes RBAC30/30Re-enter0/3030/30
NATS purge30/30Tracked Drain0/3030/30
Kafka produce10/10Effect Fence0/1010/10
Forbidden effects before and after repair