发表机构
ETH Zürich; University of Copenhagen（苏黎世联邦理工学院; 哥本哈根大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出EnfFlash，一种高效执行一阶时间需求的算法与工具，通过编译需求为命令式程序，显著降低延迟，并在社交网络GDPR合规中实现低开销。
AI 中文摘要
运行时执行器观察系统的行为并对其施加控制，以确保系统始终遵守其需求。许多自然需求不仅对系统当前行为制定限制，还对其未来行为施加义务；例如，智能体安全可能要求在运行期间收集的个人数据在某个截止日期前被擦除。在日益增长的合规环境中，现实世界的系统可能受到数百个此类需求的约束。然而，现有的支持复杂策略的执行机制对于生产软件来说往往过于缓慢；因此，开发者可能求助于非时间性的访问控制机制和临时插桩，但这些机制在需求复杂性增加时扩展性不佳。为了解决这个问题，我们引入了一种高效的算法和工具来执行复杂的时间需求，并展示了其性能。具体来说，我们识别了度量一阶时间逻辑（MFOTL）的一个片段，该片段可以以低运行时复杂度进行执行，同时支持丰富的一系列实际相关需求，包括义务。然后，我们为该片段设计了一种执行算法，并将其实现于EnfFlash中，这是一种新颖的工具，在标准基准测试中，其执行需求的延迟比之前最先进的执行器EnfGuard低至44倍，在针对LLM智能体的安全策略上低至三个数量级。这一性能是通过将需求编译为命令式程序并高效解释这些程序来实现的。我们既独立地在现有基准测试上评估EnfFlash，也将其集成到Web应用程序中作为执行后端进行评估。我们证明，它可以执行一个包含400行MFOTL公式、指定社交网络上GDPR的需求，同时为每次页面视图增加不到15毫秒的延迟，这足以满足大多数交互式和实时应用程序的需求。
英文摘要
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.
