一阶时间要求的实际运行时执行

运行时执行器观察系统的行为并对其进行控制，以确保系统始终遵守其要求。许多自然要求不仅对系统当前的行为制定限制，而且对其未来的行为施加义务；例如，Agentic安全可能要求在某个截止日期之前删除运行期间收集的个人数据。在不断发展的合规环境中，现实世界的系统可能会受到数百种此类要求的影响。然而，支持复杂策略的现有执行机制对于生产软件来说通常太慢；相反，开发人员可能会求助于非临时访问控制机制和临时工具，但这些机制随着需求的复杂性而扩展性很差。为了解决这个问题，我们引入了一种有效的算法和工具来执行复杂的时间要求并展示其性能。具体来说，我们确定了度量一阶时态逻辑（MFOTL）的一个片段，它可以以较低的运行时复杂性执行，同时支持丰富的实际相关需求（包括义务）。然后，我们为该片段设计了一种执行算法，并在 EnfFlash 中实现，这是一种新颖的工具，在标准基准测试中，执行要求的延迟相较之前最先进的执行器EnfGuard最高降低44倍，而LLM智能体的安全策略上最高低三个数量级。这种性能是通过将需求编译成我们有效解释的命令式程序来实现的。我们根据现有基准评估独立的 EnfFlash，以及作为执行后端集成到 Web 应用程序中的 EnfFlash。我们证明，它可以在社交网络上强制执行一个 400 行的 MFOTL 公式，指定 GDPR，同时为每个页面视图添加不到 15 毫秒的时间，这对于大多数交互式和实时应用程序来说已经足够了。