发表机构
International University of La Rioja（罗伊哈国际大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
该研究提出 EFFECTBOUND 工具判断授权闭合，分析 GitHub、Kubernetes 等系统的闭合失败问题，添加门机制解决 Kafka 相关问题，明确授权终止的条件。
AI 中文摘要
撤销完成、状态清理或操作成功后，授权的工作仍可能产生应用拒绝的效果，而提供者仍在其合同范围内。我们将不存在所有此类路径的情况称为策略相关效果闭合，简称效果闭合。因此，当授权的现有授权保留的路径不存在此类情况，且无法签发任何新授权时，该授权即为闭合。我们提出 EFFECTBOUND，它利用经证据支持的有限合同，在所需工作完成时判断接口是否能如实报告闭合情况。该方法将此问题归约为带隐藏状态的有限控制，当证据不足时返回策略、不可能证明或无裁决。机器验证的证明确立了该归约和检查器的正确性；检查器推导闭合结果并验证证明。在 GitHub、Kubernetes、NATS 和 Kafka 中，闭合以三种方式失败：接口缺少所需控制、干净的可见状态隐藏了活跃工作，或模型在效果前沿（可阻止效果的最后一点）之前停止。GitHub 工具无法将合并绑定到已审查的提交；受控运行确认它可能合并不同的提交。NATS 可报告无存储或待处理消息，但已分派的工作仍可向下游发布。在 Kafka 中，所有固定集代理均已应用撤销，但较早的授权请求仍可追加。我们添加了一个门，阻止对已撤销权限的新使用，并延迟返回，直到较早的在途工作完成。在固定集 Kafka 4.3.1 测试部署中，该门闭合了研究的同步非事务写路径，且未阻塞无关请求。对于授权，授权终止仅当签发停止且无较早授权能产生应用拒绝的效果时。
英文摘要
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.
Comments13 pages body - 18 total
