Policy that participates

Abstract

The natural place to put authorization in a multi-agent system is the kernel, and it is the wrong place. This paper describes Arbiter, which keeps Cedar policy evaluation, delegation verification, budgets and approval gates outside our convergence foundation and registers them as Suggestors — so that policy participates in the loop rather than becoming the loop. The architectural argument is easy: an engine that is also a policy engine has put the component that changes weekly inside the component that must not change. The mathematical argument is the contribution. We show that the confluence result our substrate depends on requires policy to be monotone in the context: a rule that permits an action in a smaller context and denies it in a larger one makes the order in which Suggestors ran observable in the final state, and the unique normal form is lost. We give the two-line counterexample, state the obligation as a property of the policy corpus rather than of the engine, and describe the linter that rejects violating rules. We then connect the assurance ladder to the preceding paper on symbolic search: a runtime decision is ordinary policy provenance, a solver-backed no-violation result is searched evidence, and only a checked artifact would be verification — three tiers, and the discipline is in never promoting one to the next.