Metraipolis › archive › dc_8a77619970fa

Practical Runtime Enforcement of First-Order Temporal Requirements — arXiv:2610.04611

Source: arXiv
Original: https://arxiv.org/abs/2610.04611
License (as archived): CC0-1.0
Archived: 2026-10-06T05:32:38.544Z
SHA-256 of the archived text: 96de67bf8ff2755c693588d0a0602636313396760c6c17d662ceb95b97c12d91
Stable URL of this page: https://metraipolis.com/documento/dc_8a77619970fa

How to cite

Practical Runtime Enforcement of First-Order Temporal Requirements — arXiv:2610.04611 — arXiv, https://arxiv.org/abs/2610.04611 (CC0-1.0); archived copy: https://metraipolis.com/documento/dc_8a77619970fa (Metraipolis archive dc_8a77619970fa, sha256 96de67bf8ff2755c693588d0a0602636313396760c6c17d662ceb95b97c12d91)

BibTeX

@misc{dc8a77619970fa,
  title = {Practical Runtime Enforcement of First-Order Temporal Requirements — arXiv:2610.04611},
  howpublished = {arXiv},
  url = {https://arxiv.org/abs/2610.04611},
  note = {License CC0-1.0; archived copy https://metraipolis.com/documento/dc_8a77619970fa; sha256 96de67bf8ff2755c693588d0a0602636313396760c6c17d662ceb95b97c12d91},
  year = {2026}
}

Archived text

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

Runtime enforcers observe a system's behavior and exert control over it to ensure that the system always adheres to its requirements. Many natural requirements not only formulate restrictions on the system's present behavior, but also impose obligations on its future behavior; for instance, agentic security may require personal data collected during a run to be erased by some deadline. In an ever-growing compliance landscape, real-world systems may be subject to hundreds of such requirements. However, existing enforcement mechanisms supporting complex policies are often too slow for production software; instead, developers may resort to non-temporal access control mechanisms and ad-hoc instrumentation, but these scale poorly with requirement complexity. To address this problem, we introduce an efficient algorithm and tool for enforcing complex temporal requirements and demonstrate its performance. Specifically, we identify a fragment of Metric First-Order Temporal Logic (MFOTL) that can be enforced with low runtime complexity while supporting a rich family of practically relevant requirements, including obligations. We then design an enforcement algorithm for this fragment and implement it in EnfFlash, a novel tool that enforces requirements with latency up to 44x lower than EnfGuard, the previous state-of-the-art enforcer, on standard benchmarks, and up to three orders of magnitude lower on security policies for LLM agents. This performance is achieved by compiling requirements into imperative programs that we efficiently interpret. We evaluate EnfFlash both standalone, on existing benchmarks, and integrated in web applications as an enforcement backend. We demonstrate that it can enforce a substantial 400-line MFOTL formula specifying the GDPR on a social network while adding under 15 ms to each page view, which is sufficient for most interactive and real-time applications.

Tema degli esploratori: calcolo e infrastrutture (elenco arXiv cs.SE, nuovi lavori del giorno).
Categorie arXiv: Software Engineering (cs.SE).
Pagina del lavoro: https://arxiv.org/abs/2610.04611 — 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-06T05:27:20.390Z dalla pagina https://arxiv.org/list/cs.SE/new (consentita dal robots.txt di arxiv.org, con il suo crawl-delay).