Serial Compositional Runtime Enforcement of Safety Timed Properties
Article No.: 5, Pages 1 - 11
Abstract
Runtime enforcement is a mechanism that compels a (black-box) system to obey some expected properties. For that, it employs an enforcement monitor /enforcer which modifies an (untrusted) sequence of events into a sequence that complies with the property. In reality, we may have many critical (timed) properties to enforce. Furthermore, an ideal deployed system allows for system customization to meet the needs of the end-users. Thus, it is highly needed to build not a monolithic enforcer for all the properties, instead, there must be individual enforcers for each property and these individual enforcers should be composed accordingly.
We investigate and provide a framework for composing enforcers of (timed) safety properties, formalized as timed automata, demonstrating that enforcement under this approach is not serially compositional in general. However, we identify and establish syntactic criteria on the automata, such that enforcers are serially compositional for any given set of safety timed automata satisfying these conditions. We show some examples of safety timed automata that satisfy those syntactic constraints, and via a prototype implementation, we evaluate the performance of our framework.
References
[1]
Rajeev Alur and David L. Dill. 1994. A theory of timed automata. Theoretical Computer Science 126, 2 (1994), 183–235. https://doi.org/10.1016/0304-3975(94)90010-8
[2]
E.M. Clarke, D.E. Long, and K.L. McMillan. 1989. Compositional model checking. In [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science. 353–362. https://doi.org/10.1109/LICS.1989.39190
[3]
Egor Dolzhenko, Jay Ligatti, and Srikar Reddy. 2015. Modeling Runtime Enforcement with Mandatory Results Automata. Int. J. Inf. Secur. 14, 1 (Feb. 2015), 47–60. https://doi.org/10.1007/s10207-014-0239-8
[4]
Yliès Falcone, Thierry Jéron, Hervé Marchand, and Srinivas Pinisetty. 2016. Runtime enforcement of regular timed properties by suppressing and delaying events. Systems & Control Letters 123 (2016), 2–41. https://doi.org/10.1016/j.scico.2016.02.008
[5]
Yliès Falcone, Laurent Mounier, Jean-Claude Fernandez, and Jean-Luc Richier. 2011. Runtime enforcement monitors: composition, synthesis, and enforcement abilities. Formal Methods Syst. Des. 38, 3 (2011), 223–262. https://doi.org/10.1007/s10703-011-0114-4
[6]
Kichun Jo, Junsoo Kim, Dongchul Kim, Chulhoon Jang, and Myoungho Sunwoo. 2014. Development of Autonomous Car—Part I: Distributed System Architecture and Development Process. IEEE Transactions on Industrial Electronics 61, 12 (Dec 2014), 7131–7140. https://doi.org/10.1109/TIE.2014.2321342
[7]
Kichun Jo, Junsoo Kim, Dongchul Kim, Chulhoon Jang, and Myoungho Sunwoo. 2015. Development of Autonomous Car—Part II: A Case Study on the Implementation of an Autonomous Driving System Based on Distributed Architecture. IEEE Transactions on Industrial Electronics 62, 8 (Aug 2015), 5119–5132. https://doi.org/10.1109/TIE.2015.2410258
[8]
Joshua Levy, Hassen Saïdi, and Tomás E. Uribe. 2002. Combining Monitors for Runtime System Verification. Electronic Notes in Theoretical Computer Science 70, 4 (2002), 112–127. https://doi.org/10.1016/S1571-0661(04)80580-2 RV’02, Runtime Verification 2002 (FLoC Satellite Event).
[9]
Jay Ligatti, Lujo Bauer, and David Walker. 2005. Edit automata: enforcement mechanisms for run-time security policies. Int. J. Inf. Sec. 4, 1-2 (2005), 2–16. https://doi.org/10.1007/s10207-004-0046-8
[10]
Jay Ligatti, Lujo Bauer, and David Walker. 2009. Run-Time Enforcement of Nonsafety Policies. ACM Trans. Inf. Syst. Secur. 12, 3, Article 19 (Jan. 2009), 41 pages. https://doi.org/10.1145/1455526.1455532
[11]
Hammond Pearce, Srinivas Pinisetty, Partha S. Roop, Matthew M. Y. Kuo, and Abhisek Ukil. 2020. Smart I/O Modules for Mitigating Cyber-Physical Attacks on Industrial Control Systems. IEEE Transactions on Industrial Informatics 16, 7 (July 2020), 4659–4669. https://doi.org/10.1109/TII.2019.2945520
[12]
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. https://doi.org/10.1007/s10703-014-0215-y
[13]
Srinivas Pinisetty, Yliès Falcone, Thierry Jéron, and Hervé Marchand. 2015. TiPEX: A Tool Chain for Timed Property Enforcement During eXecution. Vol. 9333. 306–320. https://doi.org/10.1007/978-3-319-23820-3_22
[14]
Srinivas Pinisetty, Ankit Pradhan, Partha Roop, and Stavros Tripakis. 2022. Compositional runtime enforcement revisited. Formal Methods in System Design (10 2022). https://doi.org/10.1007/s10703-022-00401-y
[15]
Srinivas Pinisetty, Partha S. Roop, Steven Smyth, Nathan Allen, Stavros Tripakis, and Reinhard Von Hanxleden. 2017. Runtime Enforcement of Cyber-Physical Systems. ACM Trans. Embed. Comput. Syst. 16, 5s, Article 178 (sep 2017), 25 pages. https://doi.org/10.1145/3126500
[16]
Srinivas Pinisetty, Partha S Roop, Steven Smyth, Stavros Tripakis, and Reinhard von Hanxleden. 2017. Runtime enforcement of reactive systems using synchronous enforcers. In Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software(Santa Barbara, CA, USA) (SPIN 2017). Association for Computing Machinery, New York, NY, USA, 80–89. https://doi.org/10.1145/3092282.3092291
[17]
Srinivas Pinisetty and Stavros Tripakis. 2016. Compositional Runtime Enforcement. In NASA Formal Methods, Sanjai Rayadurgam and Oksana Tkachuk (Eds.). Springer International Publishing, Cham, 82–99. https://doi.org/10.1007/978-3-319-40648-0_7
[18]
Viorel Preoteasa and Stavros Tripakis. 2016. Towards Compositional Feedback in Non-Deterministic and Non-Input-Receptive Systems. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’16, New York, NY, USA, July 5-8, 2016, Martin Grohe, Eric Koskinen, and Natarajan Shankar (Eds.). ACM, 768–777. https://doi.org/10.1145/2933575.2934503
[19]
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 - 12th International Colloquium Cali, Colombia, October 29-31, 2015, Proceedings. 542–560. https://doi.org/10.1007/978-3-319-25150-9_31
[20]
Matthieu Renard, Antoine Rollet, and Yliès Falcone. 2020. Runtime enforcement of timed properties using games. Formal Aspects of Computing 32, 2 (2020), 315–360. https://link.springer.com/article/10.1007/s00165-020-00515-2
[21]
Fred B. Schneider. 2000. Enforceable Security Policies. ACM Trans. Inf. Syst. Secur. 3, 1 (Feb. 2000), 30–50. https://doi.org/10.1145/353323.353382
[22]
Saumya Shankar and Srinivas Pinisetty. 2022. Serial Compositional Runtime Enforcement of Safety Timed Properties repository. https://github.com/saumyashankarsinha/Serial_Compositional_RE_of_Safety_Timed_Properties
Index Terms
- Serial Compositional Runtime Enforcement of Safety Timed Properties
Recommendations
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 ...
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 ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
February 2023
193 pages
ISBN:9798400700644
DOI:10.1145/3578527
Copyright © 2023 ACM.
Publication rights licensed to ACM. ACM acknowledges that this contribution was authored or co-authored by an employee, contractor or affiliate of a national government. As such, the Government retains a nonexclusive, royalty-free right to publish or reproduce this article, or to allow others to do so, for Government purposes only.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 23 February 2023
Check for updates
Author Tags
Qualifiers
- Research-article
- Research
- Refereed limited
Funding Sources
- IIT Bhubaneswar
Conference
ISEC 2023
ISEC 2023: 16th Innovations in Software Engineering Conference
February 23 - 25, 2023
Allahabad, India
Acceptance Rates
Overall Acceptance Rate 76 of 315 submissions, 24%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 50Total Downloads
- Downloads (Last 12 months)17
- Downloads (Last 6 weeks)1
Reflects downloads up to 18 Jan 2025
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign inFull Access
View options
View or Download as a PDF file.
PDFeReader
View online with eReader.
eReaderHTML Format
View this article in HTML Format.
HTML Format