Document Open Access Logo

Bounded-Memory Runtime Enforcement of Timed Properties

Authors Saumya Shankar , Srinivas Pinisetty , Thierry Jéron

PDF
Thumbnail PDF

File

LIPIcs.TIME.2023.6.pdf
  • Filesize: 0.96 MB
  • 22 pages

Document Identifiers

Author Details

Saumya Shankar
  • Indian Institute of Technology Bhubaneswar, India
Srinivas Pinisetty
  • Indian Institute of Technology Bhubaneswar, India
Thierry Jéron
  • Univ Rennes, Inria, IRISA, France

Funding

This work has been partially supported by The Ministry of Human Resource Development, Government of India (SPARC P#701), IIT Bhubaneswar Seed Grant (SP093).

Cite AsGet BibTex

Saumya Shankar, Srinivas Pinisetty, and Thierry Jéron. Bounded-Memory Runtime Enforcement of Timed Properties. In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 6:1-6:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.TIME.2023.6

Abstract

Runtime Enforcement (RE) is a monitoring technique aimed at correcting possibly incorrect executions w.r.t. a set of formal requirements (properties) of a system. In this paper, we consider enforcement monitoring of real-time properties. Thus, executions are modelled as timed words and specifications as timed automata. Moreover, we consider that the enforcer has the ability to delay events by storing or buffering them into its internal memory (and releasing them when the property is finally satisfied) and suppressing events when no delaying is appropriate. Practically, in an implementation, the internal memory of the enforcer is finite. In this paper, we propose a new RE paradigm for timed properties, where the memory of the enforcer is bounded/finite, to address practical applications with memory constraints and timed specifications. Bounding the memory presents a number of difficulties, e.g., how to accommodate a timed event into the memory when the memory is full, s.t., regardless of the course of action we choose to handle this situation, the behaviour of the bounded enforcer should not significantly differ from that of the unbounded enforcer. The problem of how to optimally discard events when the buffer is full is significantly more difficult in a timed environment where the progress of time affects the satisfaction or violation of a property. We define the bounded-memory RE problem for timed properties and develop a framework for regular timed properties specified as timed automata. The proposed framework is implemented in Python, and its performance is evaluated. From experiments, we discovered that the enforcer has a reasonable execution time overhead.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Automata over infinite objects
  • Software and its engineering → Software verification and validation
Keywords
  • Formal methods
  • Runtime enforcement
  • Bounded-memory
  • Timed automata

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Rajeev Alur and David L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183-235, 1994. URL: https://doi.org/10.1016/0304-3975(94)90010-8.
  2. Roderick Bloem, Bettina Könighofer, Robert Könighofer, and Chao Wang. Shield synthesis: Runtime enforcement for reactive systems. In Christel Baier and Cesare Tinelli, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 533-548, Berlin, Heidelberg, 2015. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-662-46681-0_51.
  3. Christian Colombo, Gordon J. Pace, and Gerardo Schneider. Dynamic event-based runtime monitoring of real-time and contextual properties. In Darren Cofer and Alessandro Fantechi, editors, Formal Methods for Industrial Critical Systems, pages 135-149, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. Google Scholar
  4. Christian Colombo, Gordon J. Pace, and Gerardo Schneider. Larva - safer monitoring of real-time java programs (tool paper). In 2009 Seventh IEEE International Conference on Software Engineering and Formal Methods, pages 33-37, 2009. URL: https://doi.org/10.1109/SEFM.2009.13.
  5. Egor Dolzhenko, Jay Ligatti, and Srikar Reddy. Modeling runtime enforcement with mandatory results automata. Int. J. Inf. Sec., 14(1):47-60, February 2015. URL: https://doi.org/10.1007/s10207-014-0239-8.
  6. Yliès Falcone, Jean-Claude Fernandez, and Laurent Mounier. What can you verify and enforce at runtime? Int. J. Softw. Tools Technol. Transf., 14(3):349-382, 2012. URL: https://doi.org/10.1007/s10009-011-0196-8.
  7. Yliès Falcone, Thierry Jéron, Hervé Marchand, and Srinivas Pinisetty. Runtime enforcement of regular timed properties by suppressing and delaying events. Systems & Control Letters, 123:2-41, 2016. URL: https://doi.org/10.1016/j.scico.2016.02.008.
  8. Yliès Falcone, Laurent Mounier, Jean-Claude Fernandez, and Jean-Luc Richier. Runtime enforcement monitors: composition, synthesis, and enforcement abilities. Formal Methods Syst. Des., 38(3):223-262, 2011. URL: https://doi.org/10.1007/s10703-011-0114-4.
  9. P. W. L. Fong. Access control by tracking shallow execution history. In IEEE Symposium on Security and Privacy, 2004. Proceedings. 2004, pages 43-55, 2004. URL: https://doi.org/10.1109/SECPRI.2004.1301314.
  10. Jay Ligatti, Lujo Bauer, and David Walker. Edit automata: enforcement mechanisms for run-time security policies. Int. J. Inf. Sec., 4(1-2):2-16, 2005. URL: https://doi.org/10.1007/s10207-004-0046-8.
  11. Jay Ligatti, Lujo Bauer, and David Walker. Run-time enforcement of nonsafety policies. ACM Trans. Inf. Syst. Secur., 12(3), January 2009. URL: https://doi.org/10.1145/1455526.1455532.
  12. Oded Maler, Dejan Nickovic, and Amir Pnueli. From mitl to timed automata. In Proceedings of the 4th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS'06, pages 274-289, Berlin, Heidelberg, 2006. Springer-Verlag. URL: https://doi.org/10.1007/11867340_20.
  13. Dejan Nickovic and Oded Maler. Amt: A property-based monitoring tool for analog systems. In Jean-François Raskin and P. S. Thiagarajan, editors, Formal Modeling and Analysis of Timed Systems, pages 304-319, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. Google Scholar
  14. Srinivas Pinisetty, Yliès Falcone, Thierry Jéron, and Hervé Marchand. Tipex: A tool chain for timed property enforcement during execution. In Ezio Bartocci and Rupak Majumdar, editors, Runtime Verification, pages 306-320, Cham, 2015. Springer International Publishing. Google Scholar
  15. Srinivas Pinisetty, Yliès Falcone, Thierry Jéron, Hervé Marchand, Antoine Rollet, and Omer Nguena-Timo. Runtime enforcement of timed properties revisited. Formal Methods in System Design, 45(3):381-422, 2014. URL: https://doi.org/10.1007/s10703-014-0215-y.
  16. Srinivas Pinisetty, Partha S. Roop, Steven Smyth, Nathan Allen, Stavros Tripakis, and Reinhard von Hanxleden. Runtime enforcement of cyber-physical systems. ACM Trans. Embed. Comput. Syst., 16(5s):178:1-178:25, 2017. URL: https://doi.org/10.1145/3126500.
  17. Matthieu Renard, Yliès Falcone, Antoine Rollet, Srinivas Pinisetty, Thierry Jéron, and Hervé Marchand. Enforcement of (timed) properties with uncontrollable events. In Theoretical Aspects of Computing - ICTAC 2015 - 12th International Colloquium Cali, Colombia, October 29-31, 2015, Proceedings, pages 542-560, 2015. URL: https://doi.org/10.1007/978-3-319-25150-9_31.
  18. Matthieu Renard, Antoine Rollet, and Yliès Falcone. Runtime enforcement of timed properties using games. Formal Aspects of Computing, 32(2):315-360, 2020. URL: https://link.springer.com/article/10.1007/s00165-020-00515-2.
  19. G. Roc su. On safety properties and their monitoring. Scientific Annals of Computer Science, 22(2):327-365, 2012. URL: https://doi.org/10.7561/SACS.2012.2.327.
  20. U. Sammapun, Insup Lee, and O. Sokolsky. Rt-mac: runtime monitoring and checking of quantitative and probabilistic properties. In 11th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA'05), pages 147-153, August 2005. URL: https://doi.org/10.1109/RTCSA.2005.84.
  21. Fred B. Schneider. Enforceable security policies. ACM Trans. Inf. Syst. Secur., 3(1):30-50, February 2000. URL: https://doi.org/10.1145/353323.353382.
  22. Saumya Shankar and Srinivas Pinisetty. Serial compositional runtime enforcement of safety timed properties. In Proceedings of the 16th Innovations in Software Engineering Conference, ISEC '23, New York, NY, USA, 2023. Association for Computing Machinery. URL: https://doi.org/10.1145/3578527.3578529.
  23. Saumya Shankar, Antoine Rollet, Srinivas Pinisetty, and Yliès Falcone. Bounded-memory runtime enforcement. In Owolabi Legunsen and Grigore Rosu, editors, Model Checking Software, pages 114-133, Cham, 2022. Springer International Publishing. Google Scholar
  24. Chamseddine Talhi, Nadia Tawbi, and Mourad Debbabi. Execution monitoring enforcement under memory-limitation constraints. Information and Computation, 206(2):158-184, 2008. Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis (FCS-ARSPA ’06). URL: https://doi.org/10.1016/j.ic.2007.07.009.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact