Skip to main navigation Skip to search Skip to main content

Scaling Up Proactive Enforcement

François Hublet*, Leonardo Lima*, David Basin*, Srđan Krstić*, Dmitriy Traytel*

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

1 Citation (Scopus)
8 Downloads (Pure)

Abstract

Runtime enforcers receive events from a system and output commands ensuring the system’s policy compliance. Proactive enforcers extend traditional (reactive) enforcers by emitting commands at any time, rather only as a response to system actions. However, proactive enforcers have so far lacked support for many useful policy features. This, along with the existing tools’ poor performance, hinders their adoption. We present a performance-optimized, proactive enforcement algorithm for a rich policy language: metric first-order temporal logic with function applications, aggregations, and let bindings. We have implemented this algorithm in EnfGuard, the first proactive enforcer tool that supports the above constructs. We evaluated our tool using a novel set of six benchmarks containing both real-world and synthetic policies and logs, demonstrating that it enforces realistic policies out-of-the-box and achieves the necessary performance to be used in real-time systems.

Original languageEnglish
Title of host publicationComputer Aided Verification - 37th International Conference, CAV 2025, Proceedings
EditorsRuzica Piskac, Zvonimir Rakamaric
PublisherSpringer
Publication date2025
Pages370-392
ISBN (Print)9783031986819
DOIs
Publication statusPublished - 2025
Event37th International Conference on Computer Aided Verification, CAV 2025 - Zagreb, Croatia
Duration: 23 Jul 202525 Jul 2025

Conference

Conference37th International Conference on Computer Aided Verification, CAV 2025
Country/TerritoryCroatia
CityZagreb
Period23/07/202525/07/2025
SeriesLecture Notes in Computer Science
Volume15933 LNCS
ISSN0302-9743

Bibliographical note

Publisher Copyright:
© The Author(s) 2025.

Cite this