发表机构
University of Otago（奥塔哥大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出将访问控制决策函数编码为固定缓冲区，用EverParse验证器一次性证明执行代码忠实于策略，覆盖所有请求，并部署于seL4微内核。
AI 中文摘要
商业安全网关在从网络到策略决策的代码路径中反复出现实现漏洞：手写的执行逻辑偏离了策略作者的意图，以及网络边界上的临时请求解析器引入了自身的内存安全缺陷。在这两种情况下，缺陷都存在于部署的执行代码中，而非策略本身。现有方法要么不验证执行运行时，要么仅通过差分测试将形式模型连接到手写引擎。我们的贡献是一个类结果：一个仅向前、无回溯的EverParse验证器是受限有限状态类的已验证识别器，而具有固定偏移字段和受限析取的访问控制决策函数属于该类，因此一个经过机器检查的证明可转移到该类中的每个策略，而无需为每个策略重新建立。具体而言，我们将受限策略语言的决策函数编码为固定大小的字节缓冲区，并使用SMT求解器一次性验证执行代码——覆盖所有字节值——证明验证器接受当且仅当决策函数接受，适用于每个策略、请求和会话。在固定端点集上编辑规则内容无需新证明；添加端点则重新运行工具链；扩展语言需要新证明。我们确立的是策略的忠实执行，而非策略本身的安全性。经过验证的网关是平台无关的，仅需EverParse/Z3和C编译器，其正确性由我们假定。我们演示了在seL4微内核上的部署，确保每个请求都通过网关，且未经验证的组件无法破坏已验证的执行链。
英文摘要
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.
Comments12 pages, 2 figures
