Access control enforcement verified using a single proof for all policies
Access Control as Verified Parse Constraints
Cryptography and Security
Summary
Security systems that control who can do what often have bugs in the code that enforces rules, even if the rules themselves are correct. The authors show a way to verify once and for all that the enforcement code matches the policy rules for a large class of policies. This means that editing the rules does not require verifying the code again, as long as the structure stays the same. Their approach uses a special validator and mathematical tools to prove correctness, and it was demonstrated on a secure operating system kernel.
What this means in practice
- •For network security engineers: Ensure that network access control gateways enforce policies exactly as intended without re-verifying code for each policy edit.
- •For operating system developers: Integrate verified access control enforcement within microkernel environments to guarantee request filtering correctness across all policies.
Authors
Saranachon Iammongkol, Zhiyi Huang, David Eyers
Abstract
Commercial security gateways repeatedly ship implementation bugs in the code path between the network and the policy decision: hand-written enforcement logic that diverges from the policy author's intent, and ad-hoc request parsers at the network boundary that introduce memory-safety flaws of their own. In both cases the bug is in the deployed enforcement code, not in the policy. Existing approaches either leave the enforcement runtime unverified or connect a formal model to a hand-written engine only by differential testing. Our contribution is a class result: a forward-only, backtrack-free EverParse validator is a verified recognizer for a bounded, finite-state class, and access-control decision functions with fixed-offset fields and bounded disjunction belong to it, so one machine-checked proof transfers to every policy in the class rather than being re-established per policy. Concretely, we encode a bounded policy language's decision function into a fixed-size byte buffer and verify the enforcement code once---covering all byte values---with an SMT solver, proving the validator accepts if and only if the decision function accepts, for every policy, request, and session. Editing rule content over a fixed endpoint set then needs no new proof; adding endpoints reruns the toolchain; extending the language needs new proofs. We establish faithful enforcement of a policy, not that a policy is itself secure. The verified gate is platform-independent, requiring only EverParse/Z3 and a C compiler, whose correctness we assume. We demonstrate a deployment on the seL4 microkernel, which ensures every request passes through the gate and that unverified components cannot corrupt the verified enforcement chain.