Document Open Access Logo

Decentralized Runtime Enforcement of Message Sequences in Message-Based Systems

Authors Mahboubeh Samadi, Fatemeh Ghassemi, Ramtin Khosravi

PDF
Thumbnail PDF

File

LIPIcs.OPODIS.2020.21.pdf
  • Filesize: 0.72 MB
  • 18 pages

Document Identifiers

Author Details

Mahboubeh Samadi
  • University of Tehran, Iran
Fatemeh Ghassemi
  • University of Tehran, Iran
Ramtin Khosravi
  • University of Tehran, Iran

Cite AsGet BibTex

Mahboubeh Samadi, Fatemeh Ghassemi, and Ramtin Khosravi. Decentralized Runtime Enforcement of Message Sequences in Message-Based Systems. In 24th International Conference on Principles of Distributed Systems (OPODIS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 184, pp. 21:1-21:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.OPODIS.2020.21

Abstract

In the new generation of message-based systems such as network-based smart systems, distributed components collaborate via asynchronous message passing. In some cases, particular ordering among the messages may lead to violation of the desired properties such as data confidentiality. Due to the absence of a global clock and usage of off-the-shelf components, there is no control over the order of messages at design time. To make such systems safe, we propose a choreography-based runtime enforcement algorithm that given an automata-based specification of unwanted message sequences, prevents certain messages to be sent, and assures that the unwanted sequences are not formed. Our algorithm is fully decentralized in the sense that each component is equipped with a monitor, as opposed to having a centralized monitor. As there is no global clock in message-based systems, the order of messages cannot be determined exactly. In this way, the monitors behave conservatively in the sense that they prevent a message from being sent, even when the sequence may not be formed. We aim to minimize conservative prevention in our algorithm when the message sequence has not been formed. The efficiency and scalability of our algorithm are evaluated in terms of the communication overhead and the blocking duration through simulation.

Subject Classification

ACM Subject Classification
  • Computing methodologies → Distributed computing methodologies
Keywords
  • Asynchronous Message Passing
  • Choreography-Based
  • Runtime Enforcement
  • Runtime Prevention
  • Message Ordering

Metrics

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

References

  1. Gul. Agha. ACTORS - a model of concurrent computation in distributed systems. MIT Press series in artificial intelligence, 1990. Google Scholar
  2. Akka. https://akka.io. Accessed: 2020-09-09.
  3. Bavid Basin, Felix Klaedtke, and Eugen Zălinescu. Runtime verification of temporal properties over out-of-order data streams. In Proc. CAV. Springer, 2017. Google Scholar
  4. Andreas Bauer and Yliès Falcone. Decentralized LTL monitoring. In Proc. FM. Springer, 2012. Google Scholar
  5. Simon Bliudze and Joseph Sifakis. The algebra of connectors—structuring interaction in bip. Journal of TC. IEEE, 57(10):1-16, 2008. Google Scholar
  6. Roderick Bloem, Bettina Könighofer, Robert Könighofer, and Chao Wang. Shield synthesis: runtime enforcement for reactive systems. In Proc. TACAS. Springer, 2015. Google Scholar
  7. Hadil Charafeddine, Khalil El-Harake, Yliès Falcone, and Mohamad Jaber. Runtime enforcement for component-based systems. In Proc. SAC. ACM, 2015. Google Scholar
  8. Franco Cicirelli, Libero Nigro, and Paolo Sciammarella. Model continuity in cyber-physical systems:a control-centered methodology based on agents. Journal of Simul Model Pract Theory. Elsevier, 83:93-107, 2018. Google Scholar
  9. Christian Colombo and Yliès Falcone. Organising LTL monitors over distributed systems with a global clock. Journal of FMSD. Springer, 42(1):109-158, 2016. Google Scholar
  10. Egor Dolzhenko, Jay Ligatti, and Srikar Reddy. Modeling runtime enforcement with mandatory results automata. JIS. Springer, 14(2):47-60, 2015. Google Scholar
  11. Yliès Falcone and Mohamad Jaber. Fully automated runtime enforcement of component-based systemswith formal and sound recovery. Journal of STTT. Springer, 19(3):341-365, 2017. Google Scholar
  12. Yliès Falcone, Thierry Jéron, Hervé Marchand, and Srinivas Pinisetty. Runtime enforcement of regular timed properties by suppressing and delaying events. Journal of SCP. Elsevier, 123(1):2-41, 2016. Google Scholar
  13. Yliès Falcone, Leonardo Mariani, Antoine Rollet, and Saikat Saha. Runtime failure prevention and reaction. In Lectures on Runtime Verification. Springer, 2018. Google Scholar
  14. Yliès Falcone, Robert Shostak, and Marshall Pease. The byzantine generals problem. Journal of TOPLAS. ACM, 4(3):382-401, 1982. Google Scholar
  15. Richard Gay, Heiko Mantel, and Barbara Sprick. Serveice automata. In Proc. FAST. Springer, 2011. Google Scholar
  16. Sylvain Hall, Raphaël Khoury, Quentin Betti, Antoine El-Hokayem, and Yliès Falcone. Decentralized enforcement of document lifecycle constraints. JIS. ACM, 74(2), 2018. Google Scholar
  17. Brinch Hansen. The Origin of Concurrent Programming. Springer-Verlag, 2002. Google Scholar
  18. C.A.R. Hoare. Communicating sequential processes. Prentice-Hall International series in computer science, 1985. Google Scholar
  19. Ilya Kolchinsky and Assaf Schuster. Efficient adaptive detection of complex event patterns. In Proc. VLDB. ACM, 2018. Google Scholar
  20. Ajay D Kshemkalyani and Mukesh Singhal. Distributed Computing: Principles, Algorithms, and Systems. Cambridge University Press, 2011. Google Scholar
  21. Leslie Lamport. Time, clocks, and the ordering of events in a distributed system. JCM. ACM, 21(7):558-565, 1978. Google Scholar
  22. Jay Ligatti, Lujo Bauer, and David Walker. Edit automata: Enforcement mechanisms for run-time security policies. JIS. Springer, 4(1):2-16, 2005. Google Scholar
  23. Jay Ligatti and Srikar Reddy. A theory of runtime enforcement, with results. In Proc. ESORICS. Springer, 2010. Google Scholar
  24. Carmen. T Lopez, Stefan Marr, Elisa Gonzalez, and Hanspeter Mössenböck. A Study of Concurrency Bugs and Advanced Development Support for Actor-based Programs, Programming with Actors. Programming with Actors, 2018. Google Scholar
  25. Friedemann Mattern. Virtual Time and Global States of Distributed Systems, Parallel and Distributed Algorithms. North-Holland Press, 1988. Google Scholar
  26. Barton. P Miller and J. D Choi. Breakpoints and halting in distributed programs. In Proc. ICDCS. IEEE, 1988. Google Scholar
  27. Menna Mostafa and borzoo Bonakdarpour. Decentralized runtime verification of ltl specifications in distributed systems. In Proc. IPDPS. IEEE, 2015. Google Scholar
  28. Saravana.M Palanisamy, Muhammad.A Tariq Frank Dürr, and Kurt Rothermel. Preserving privacy and quality of service in complex event processing through event reordering. In Proc. DEBS. ACM, 2018. Google Scholar
  29. Srinivas Pinisetty, Viorel Preoteasa, Stavros Tripakis, Thierry Jéron, Yliès Falcone, and Hervé Marchand. Predictive runtime enforcement. Journal of FMSD. Springer, 51(3):154-199, 2017. Google Scholar
  30. Yingmei Qi, Lei Cao, Medhabi Ray, and Elke A. Rundensteiner. Complex event analytics: online aggregation of stream sequence patterns. In Proc. SIGMOD. ACM, 2014. Google Scholar
  31. Panos Rondogiannis, Georgios Pavlides, and A. Levy. Distributed algorithm for communication deadlock detection. Journal of IST. Elsevier, 33(7):483-488, 1991. Google Scholar
  32. Mahboubeh Samadi, Fatemeh Ghassemi, and Ramtin Khosravi. Choreography-based runtime verification of message sequences in distributed message-based systems. available in http://rebeca-lang.org/assets/papers/archive/rv.pdf. Google Scholar
  33. Fred. B Schneider. Enforceable security policies. Journal of TISSEC. ACM, 3(1):30-50, 2000. Google Scholar
  34. César Sánchez, Gerardo Schneider, Wolfgang Ahrendt, and et al. A survey of challenges for runtime verification from advanced application domains (beyond software). Journal of FMSD. Springer, 54(3):273-335, 2018. Google Scholar
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