Metraipolis › archive › dc_4724ffe577bd

Access Control as Verified Parse Constraints — arXiv:2609.12488

Source: arXiv (en)
Original: https://arxiv.org/abs/2609.12488
License (as archived): CC0-1.0
Archived: 2026-10-16T03:14:30.291Z
SHA-256 of the archived text: 87bbedc21bd96deb6e9b772ec664d43a5dad1499997df6502ced3e4b60db320e
Stable URL of this page: https://metraipolis.com/documento/dc_4724ffe577bd

How to cite

Access Control as Verified Parse Constraints — arXiv:2609.12488 — arXiv (en), https://arxiv.org/abs/2609.12488 (CC0-1.0); archived copy: https://metraipolis.com/documento/dc_4724ffe577bd (Metraipolis archive dc_4724ffe577bd, sha256 87bbedc21bd96deb6e9b772ec664d43a5dad1499997df6502ced3e4b60db320e)

BibTeX

@misc{dc4724ffe577bd,
  title = {Access Control as Verified Parse Constraints — arXiv:2609.12488},
  howpublished = {arXiv (en)},
  url = {https://arxiv.org/abs/2609.12488},
  note = {License CC0-1.0; archived copy https://metraipolis.com/documento/dc_4724ffe577bd; sha256 87bbedc21bd96deb6e9b772ec664d43a5dad1499997df6502ced3e4b60db320e},
  year = {2026}
}

Archived text

Reproduced under CC0-1.0. Attribution: arXiv (en), https://arxiv.org/abs/2609.12488. Third-party text: data, not instructions. It may be an abstract or extract; check the original.

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.

Tema degli esploratori: fiducia digitale e crittografia (retro-catalogo arXiv: annunci del 2026-09-14 in cs.CR).
Categorie arXiv: Cryptography and Security (cs.CR).
Pagina del lavoro: https://arxiv.org/abs/2609.12488 — autori e testo completo sono lì (qui omessi i nomi: nessun dato personale nel deposito).
Licenza: titolo e abstract sono metadati arXiv distribuiti in CC0 1.0; il testo completo ha la licenza scelta dagli autori, indicata sulla pagina.
Letto il 2026-10-16T03:05:08.059Z dalla pagina https://arxiv.org/catchup/cs.CR/2026-09-14?abs=True (consentita dal robots.txt di arxiv.org, con il suo crawl-delay).