System enforces complex future data rules with low delay
Practical Runtime Enforcement of First-Order Temporal Requirements
Software Engineering
Summary
Systems often need to follow rules that not only restrict what they do now but also require certain things to happen later, like deleting personal data on time. The authors present a new efficient method and tool called EnfFlash that watches and controls software to make sure it meets these complex timing rules without slowing it down much. EnfFlash works by turning these rules into simple programs that run quickly. Tested on benchmarks and real web apps, it enforces even detailed rules like GDPR with very little added delay.
What this means in practice
- •For software developers: Add efficient runtime checks for complex temporal privacy and security rules to interactive applications without noticeable slowdowns.
- •For web application engineers: Integrate runtime enforcement backends that ensure compliance with data protection regulations like GDPR in social networks and other online platforms.
Authors
François Hublet, David Basin, Srđan Krstić
Abstract
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.