Matthieu Renard
ABSTRACT
We leverage Büchi games for the runtime enforcement of regular properties with uncontrollable events. Runtime enforcement consists in modifying the execution of a running system to have it satisfy a given regular property, modelled by an automaton. We revisit runtime enforcement with uncontrollable events and propose a framework where we model the runtime enforcement problem as a Büchi game and synthesise sound, compliant, and optimal enforcement mechanisms as strategies.We present algorithms and a tool implementing enforcement mechanisms.We reduce the complexity of the computations performed by enforcement mechanisms at runtime by pre-computing the decisions of enforcement mechanisms ahead of time.
- David Basin, Vincent Jugé, Felix Klaedtke, and Eugen Zălinescu. 2013. Enforceable Security Policies Revisited. ACM Trans. Inf. Syst. Secur. 16, 1, Article 3 (June 2013), 26 pages. Google Scholar
Digital Library
- David Basin, Felix Klaedtke, and Eugen Zalinescu. 2011. Algorithms for Monitoring Real-Time Properties. In Proceedings of the 2nd International Conference on Runtime Verification (RV 2011) (Lecture Notes in Computer Science), Sarfraz Khurshid and Koushik Sen (Eds.), Vol. 7186. Springer-Verlag, 260–275. Google ScholarDigital Library
- Roderick Bloem, Bettina Könighofer, Robert Könighofer, and Chao Wang. 2015.Google Scholar
- Shield Synthesis: - Runtime Enforcement for Reactive Systems. In Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings. 533–548. Google ScholarDigital Library
- Peter Bulychev, Thomas Chatain, Alexandre David, and Kim G. Larsen. 2009.Google Scholar
- Efficient on-the-fly Algorithm for Checking Alternating Timed Simulation. Springer Berlin Heidelberg, Berlin, Heidelberg, 73–87.Google Scholar
- Krishnendu Chatterjee and Monika Henzinger. 2012. An O(N2) Time Algorithm for Alternating BÜChi Games. In Proceedings of the Twenty-third Annual ACMSIAM Symposium on Discrete Algorithms (SODA ’12). Society for Industrial and Applied Mathematics, Philadelphia, PA, USA, 1386–1399. Google ScholarDigital Library
- Egor Dolzhenko, Jay Ligatti, and Srikar Reddy. 2015. Modeling Runtime Enforcement with Mandatory Results Automata. International Journal of Information Security 14, 1 (Feb. 2015), 47–60. Google ScholarDigital Library
- Yliès Falcone. 2010. You Should Better Enforce Than Verify. In Runtime Verification - First International Conference, RV 2010, St. Julians, Malta, November 1-4, 2010. Proceedings. 89–105. Google ScholarDigital Library
- Yliès Falcone, Jean-Claude Fernandez, and Laurent Mounier. 2012.Google Scholar
- What can you verify and enforce at runtime? International Journal on Software Tools for Technology Transfer 14, 3 (2012), 349–382.Google Scholar
- Yliès Falcone, Thierry Jéron, Hervé Marchand, and Srinivas Pinisetty. 2016.Google Scholar
- Runtime enforcement of regular timed properties by suppressing and delaying events. Systems & Control Letters 123 (2016), 2–41.Google Scholar
- Yliès Falcone, Laurent Mounier, Jean-Claude Fernandez, and Jean-Luc Richier. 2011. Runtime enforcement monitors: composition, synthesis, and enforcement abilities. Formal Methods in System Design 38, 3 (2011), 223–262. Google ScholarDigital Library
- Jay Ligatti, Lujo Bauer, and David Walker. 2009.Google Scholar
- Run-Time Enforcement of Nonsafety Policies. ACM Trans. Inf. Syst. Secur. 12, 3, Article 19 (Jan. 2009), 41 pages. Google ScholarDigital Library
- Srinivas Pinisetty, Yliès Falcone, Thierry Jéron, Hervé Marchand, Antoine Rollet, and Omer Nguena-Timo. 2014. Runtime enforcement of timed properties revisited. Formal Methods in System Design 45, 3 (2014), 381–422. Google ScholarDigital Library
- Matthieu Renard, Yliès Falcone, Antoine Rollet, Thierry Jéron, and Hervé Marchand. 2017.Google Scholar
- Optimal Enforcement of (Timed) Properties with Uncontrollable Events. Mathematical Structures in Computer Science (MSCS) (2017), 1–46.Google Scholar
- Matthieu Renard, Yliès Falcone, Antoine Rollet, Srinivas Pinisetty, Thierry Jéron, and Hervé Marchand. 2015. Enforcement of (Timed) Properties with Uncontrollable Events. In Theoretical Aspects of Computing - ICTAC 2015 (Lecture Notes in Computer Science), Vol. 9399. Springer International Publishing, 542–560. Google ScholarDigital Library
- Fred B. Schneider. 2000.Google Scholar
- Enforceable Security Policies. ACM Trans. Inf. Syst. Secur. 3, 1 (Feb. 2000), 30–50. Google ScholarDigital Library
Index Terms
- Runtime enforcement using Büchi games
Recommendations
Runtime enforcement of timed properties using games
AbstractThis paper deals with runtime enforcement of timed properties with uncontrollable events. Runtime enforcement consists in defining and using an enforcement mechanism that modifies the executions of a running system to ensure their correctness with ...
Predictive runtime enforcement
Runtime enforcement (RE) is a technique to ensure that the (untrustworthy) output of a black-box system satisfies some desired properties. In RE, the output of the running system, modeled as a sequence of events, is fed into an enforcer. The enforcer ...
Runtime enforcement of timed properties revisited
Runtime enforcement is a powerful technique to ensure that a running system satisfies some desired properties. Using an enforcement monitor, an (untrustworthy) input execution (in the form of a sequence of events) is modified into an output sequence ...
Comments