Bounded-Memory Runtime Enforcement

Saumya Shankar (1) , Antoine Rollet (2) , Srinivas Pinisetty (1) , Yliès Falcone (3)

1 Indian Institute of technology Bhubaneswar
2 LaBRI - Laboratoire Bordelais de Recherche en Informatique
3 CORSE - Compiler Optimization and Run-time Systems

Runtime Enforcement (RE) is a monitoring technique to ensure that a system obeys a set of formal requirements (properties). RE employs an enforcer (a safety wrapper for the system) which modifies the (untrustworthy) output by performing actions such as delaying (by storing/buffering) and suppressing events, when needed. In this paper, to handle practical applications with memory constraints, we propose a new RE paradigm where the memory of the enforcer is bounded/finite. Besides the property to be enforced, the user specifies a bound on the enforcer memory. Bounding the memory poses various challenges such as how to handle the situation when the memory is full, how to optimally discard events from the buffer to accommodate new events and let the enforcer continue operating. We define the bounded-memory RE problem and develop a framework for any regular property. The proposed framework is implemented and its performance evaluated via some examples from application scenarios indicates that the enforcer has reasonable execution time overhead.

Domaines: Réseaux et télécommunications [cs.NI]

Saumya Shankar, Antoine Rollet, Srinivas Pinisetty, Yliès Falcone. Bounded-Memory Runtime Enforcement. SPIN 2022 - 28th International Symposium on Model Checking of Software, May 2022, Chicago, United States. pp.114-133, ⟨10.1007/978-3-031-15077-7_7⟩. ⟨hal-03758964⟩