Document Open Access Logo

Centralized vs Decentralized Monitors for Hyperproperties

Authors Luca Aceto , Antonis Achilleos , Elli Anastasiadi , Adrian Francalanza , Daniele Gorla , Jana Wagemaker

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2024.4.pdf
  • Filesize: 0.84 MB
  • 19 pages

Document Identifiers

Author Details

Luca Aceto
  • Dept. of Computer Science, Reykjavik University, Iceland
  • Gran Sasso Science Institute, L'Aquila, Italy
Antonis Achilleos
  • Dept. of Computer Science, Reykjavik University, Iceland
Elli Anastasiadi
  • Uppsala University, Sweden
Adrian Francalanza
  • University of Malta, Malta
Daniele Gorla
  • Dept. of Computer Science, "Sapienza" University of Rome, Italy
Jana Wagemaker
  • Dept. of Computer Science, Reykjavik University, Iceland

Funding

This work has been supported by the project "Mode(l)s of Verification and Monitorability" (MoVeMent) (grant No 217987) of the Icelandic Research Fund.
  • Anastasiadi, Elli: Elli Anastasiadi’s research has been supported by grant VR 2020-04430 of the Swedish Research Council.

Cite AsGet BibTex

Luca Aceto, Antonis Achilleos, Elli Anastasiadi, Adrian Francalanza, Daniele Gorla, and Jana Wagemaker. Centralized vs Decentralized Monitors for Hyperproperties. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 4:1-4:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.CONCUR.2024.4

Abstract

This paper focuses on the runtime verification of hyperproperties expressed in Hyper-recHML, an expressive yet simple logic for describing properties of sets of traces. To this end, we consider a simple language of monitors that observe sets of system executions and report verdicts w.r.t. a given Hyper-recHML formula. We first employ a unique omniscient monitor that centrally observes all system traces. Since centralised monitors are not ideal for distributed settings, we also provide a language for decentralized monitors, where each trace has a dedicated monitor; these monitors yield a unique verdict by communicating their observations to one another. For both the centralized and the decentralized settings, we provide a synthesis procedure that, given a formula, yields a monitor that is correct (i.e., sound and violation complete). A key step in proving the correctness of the synthesis for decentralized monitors is a result showing that, for each formula, the synthesized centralized monitor and its corresponding decentralized one are weakly bisimilar for a suitable notion of weak bisimulation.

Subject Classification

ACM Subject Classification
  • Theory of computation → Operational semantics
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Logic and verification
Keywords
  • Runtime Verification
  • hyperlogics
  • decentralization

Metrics

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

Related Versions

References

  1. Luca Aceto, Antonis Achilleos, Elli Anastasiadi, and Adrian Francalanza. Monitoring hyperproperties with circuits. In Mohammad Reza Mousavi and Anna Philippou, editors, Formal Techniques for Distributed Objects, Components, and Systems - 42nd IFIP WG 6.1 International Conference, FORTE 2022, volume 13273 of LNCS, pages 1-10. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-08679-3_1.
  2. Luca Aceto, Antonis Achilleos, Elli Anastasiadi, Adrian Francalanza, Daniele Gorla, and Jana Wagemaker. Centralized vs decentralized monitors for hyperproperties. CoRR, abs/2405.12882, 2024. URL: https://doi.org/10.48550/arXiv.2405.12882.
  3. Luca Aceto, Antonis Achilleos, Duncan Paul Attard, Léo Exibard, Adrian Francalanza, and Anna Ingólfsdóttir. A monitoring tool for linear-time μhml. In COORDINATION, volume 13271 of LNCS, pages 200-219. Springer, 2022. Google Scholar
  4. Luca Aceto, Antonis Achilleos, Duncan Paul Attard, Léo Exibard, Adrian Francalanza, and Anna Ingólfsdóttir. A monitoring tool for linear-time μ. Sci. Comput. Program., 232:103031, 2024. URL: https://doi.org/10.1016/j.scico.2023.103031.
  5. Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen. Adventures in monitorability: from branching to linear time and back again. Proc. ACM Program. Lang. POPL, 3(52):1-29, 2019. URL: https://doi.org/10.1145/3290365.
  6. Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen. Testing equivalence vs. runtime monitoring. In Models, Languages, and Tools for Concurrent and Distributed Programming, volume 11665 of LNCS, pages 28-44. Springer, 2019. Google Scholar
  7. Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen. An operational guide to monitorability with applications to regular properties. Softw. Syst. Model., 20(2):335-361, 2021. Google Scholar
  8. Luca Aceto, Duncan Paul Attard, Adrian Francalanza, and Anna Ingólfsdóttir. Runtime Instrumentation for Reactive Components. In ECOOP, volume 313 of LIPIcs, pages 16:1-16:33. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. Google Scholar
  9. Luca Aceto, Ian Cassar, Adrian Francalanza, and Anna Ingólfsdóttir. On first-order runtime enforcement of branching-time properties. Acta Informatica, 60(4):385-451, 2023. Google Scholar
  10. Shreya Agrawal and Borzoo Bonakdarpour. Runtime Verification of k-Safety Hyperproperties in HyperLTL. In IEEE 29th Computer Security Foundations Symposium, pages 239-252. IEEE Computer Society, 2016. Google Scholar
  11. Duncan Paul Attard, Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen. Better late than never or: Verifying asynchronous components at runtime. In FORTE, volume 12719 of LNCS, pages 207-225. Springer, 2021. Google Scholar
  12. Ezio Bartocci, Yliès Falcone, Adrian Francalanza, and Giles Reger. Introduction to runtime verification. In Ezio Bartocci and Yliès Falcone, editors, Lectures on Runtime Verification - Introductory and Advanced Topics, volume 10457 of LNCS, pages 1-33. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-75632-5_1.
  13. Raven Beutner and Bernd Finkbeiner. Software verification of hyperproperties beyond k-safety. In Sharon Shoham and Yakir Vizel, editors, Computer Aided Verification - 34th International Conference, CAV 2022, volume 13371 of LNCS, pages 341-362. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-13185-1_17.
  14. Raven Beutner, Bernd Finkbeiner, Hadar Frenkel, and Niklas Metzger. Second-order hyperproperties. In CAV (2), volume 13965 of LNCS, pages 309-332. Springer, 2023. Google Scholar
  15. Raven Beutner, Bernd Finkbeiner, Hadar Frenkel, and Niklas Metzger. Monitoring second-order hyperproperties. In Mehdi Dastani, Jaime Simão Sichman, Natasha Alechina, and Virginia Dignum, editors, Proceedings of the 23rd International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2024, pages 180-188. ACM, 2024. URL: https://dl.acm.org/doi/10.5555/3635637.3662865.
  16. Laura Bocchi, Tzu-Chun Chen, Romain Demangeon, Kohei Honda, and Nobuko Yoshida. Monitoring networks through multiparty session types. Theor. Comput. Sci., 669:33-58, 2017. Google Scholar
  17. Laura Bocchi, Kohei Honda, Emilio Tuosto, and Nobuko Yoshida. A theory of design-by-contract for distributed multiparty interactions. In Paul Gastin and François Laroussinie, editors, CONCUR 2010 - Concurrency Theory, pages 162-176, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg. Google Scholar
  18. Borzoo Bonakdarpour and Bernd Finkbeiner. Runtime verification for HyperLTL. In Yliès Falcone and César Sánchez, editors, Runtime Verification - 16th International Conference, RV 2016, Madrid, Spain, September 23-30, 2016, Proceedings, volume 10012 of LNCS, pages 41-45. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-46982-9_4.
  19. Borzoo Bonakdarpour and Bernd Finkbeiner. The complexity of monitoring hyperproperties. In 31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford, United Kingdom, July 9-12, 2018, pages 162-174. IEEE Computer Society, 2018. URL: https://doi.org/10.1109/CSF.2018.00019.
  20. Borzoo Bonakdarpour, Pierre Fraigniaud, Sergio Rajsbaum, David A. Rosenblueth, and Corentin Travers. Decentralized asynchronous crash-resilient runtime verification. J. ACM, 69(5):34:1-34:31, 2022. URL: https://doi.org/10.1145/3550483.
  21. Borzoo Bonakdarpour, Pierre Fraigniaud, Sergio Rajsbaum, and Corentin Travers. Challenges in fault-tolerant distributed runtime verification. In Tiziana Margaria and Bernhard Steffen, editors, Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications - 7th International Symposium, ISoLA 2016,, volume 9953 of LNCS, pages 363-370, 2016. URL: https://doi.org/10.1007/978-3-319-47169-3_27.
  22. Borzoo Bonakdarpour, César Sánchez, and Gerardo Schneider. Monitoring hyperproperties by combining static analysis and runtime verification. In Tiziana Margaria and Bernhard Steffen, editors, Leveraging Applications of Formal Methods, Verification and Validation. Verification - 8th International Symposium, ISoLA 2018, volume 11245 of LNCS, pages 8-27. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-03421-4_2.
  23. Noel Brett, Umair Siddique, and Borzoo Bonakdarpour. Rewriting-based runtime verification for alternation-free hyperltl. In Axel Legay and Tiziana Margaria, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 77-93, Berlin, Heidelberg, 2017. Springer Berlin Heidelberg. Google Scholar
  24. Ian Cassar, Adrian Francalanza, Claudio Antares Mezzina, and Emilio Tuosto. Reliability and fault-tolerance by choreographic design. In Adrian Francalanza and Gordon J. Pace, editors, Proceedings Second International Workshop on Pre- and Post-Deployment Verification Techniques, PrePost@iFM 2017, Torino, Italy, 19 September 2017, volume 254 of EPTCS, pages 69-80, 2017. URL: https://doi.org/10.4204/EPTCS.254.6.
  25. Marek Chalupa and Thomas A. Henzinger. Monitoring hyperproperties with prefix transducers. In RV, volume 14245 of LNCS, pages 168-190. Springer, 2023. Google Scholar
  26. Michael R. Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, and César Sánchez. Temporal logics for hyperproperties. In Martín Abadi and Steve Kremer, editors, Principles of Security and Trust - Third International Conference, POST 2014, volume 8414 of LNCS, pages 265-284. Springer, 2014. URL: https://doi.org/10.1007/978-3-642-54792-8_15.
  27. Michael R. Clarkson and Fred B. Schneider. Hyperproperties. J. Comput. Secur., 18(6):1157-1210, 2010. URL: https://doi.org/10.3233/JCS-2009-0393.
  28. E. Allen Emerson and Joseph Y. Halpern. "Sometimes" and "Not Never" revisited: on branching versus linear time temporal logic. J. ACM, 33(1):151-178, 1986. URL: https://doi.org/10.1145/4904.4999.
  29. Bernd Finkbeiner, Christopher Hahn, Marvin Stenger, and Leander Tentrup. RVHyper: A runtime verification tool for temporal hyperproperties. In TACAS (2), volume 10806 of LNCS, pages 194-200. Springer, 2018. Google Scholar
  30. Bernd Finkbeiner, Christopher Hahn, Marvin Stenger, and Leander Tentrup. Monitoring hyperproperties. Formal Methods Syst. Des., 54(3):336-363, 2019. URL: https://doi.org/10.1007/s10703-019-00334-z.
  31. Pierre Fraigniaud, Sergio Rajsbaum, and Corentin Travers. A lower bound on the number of opinions needed for fault-tolerant decentralized run-time monitoring. J. Appl. Comput. Topol., 4(1):141-179, 2020. URL: https://doi.org/10.1007/s41468-019-00047-6.
  32. Adrian Francalanza. Consistently-detecting monitors. In CONCUR, volume 85 of LIPIcs, pages 8:1-8:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. Google Scholar
  33. Adrian Francalanza. A Theory of Monitors. Inf. Comput., 281:104704, 2021. URL: https://doi.org/10.1016/j.ic.2021.104704.
  34. Adrian Francalanza, Luca Aceto, and Anna Ingólfsdóttir. Monitorability for the Hennessy-Milner logic with recursion. Formal Methods Syst. Des., 51(1):87-116, 2017. URL: https://doi.org/10.1007/S10703-017-0273-Z.
  35. Adrian Francalanza, Andrew Gauci, and Gordon J. Pace. Distributed system contract monitoring. J. Log. Algebraic Methods Program., 82(5-7):186-215, 2013. Google Scholar
  36. Jens Oliver Gutsfeld, Markus Müller-Olm, and Christoph Ohrem. Automata and fixpoints for asynchronous hyperproperties. Proc. ACM Program. Lang., 5(POPL), January 2021. URL: https://doi.org/10.1145/3434319.
  37. Christopher Hahn, Marvin Stenger, and Leander Tentrup. Constraint-based monitoring of hyperproperties. In Tomáš Vojnar and Lijun Zhang, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 115-131, Cham, 2019. Springer International Publishing. Google Scholar
  38. Jun Inoue and Yoriyuki Yamagata. Operational semantics of process monitors. In RV, volume 10548 of LNCS, pages 403-409. Springer, 2017. Google Scholar
  39. Limin Jia, Hannah Gommerstadt, and Frank Pfenning. Monitors and blame assignment for higher-order session types. In POPL, pages 582-594. ACM, 2016. Google Scholar
  40. Dexter Kozen. Results on the propositional μ-calculus. Theoretical Computer Science, 27(3):333-354, 1983. URL: https://doi.org/10.1016/0304-3975(82)90125-6.
  41. Orna Kupferman, Moshe Y. Vardi, and Pierre Wolper. An automata-theoretic approach to branching-time model checking. J. ACM, 47(2):312-360, 2000. URL: https://doi.org/10.1145/333979.333987.
  42. Ruggero Lanotte, Massimo Merro, and Andrei Munteanu. A process calculus approach to detection and mitigation of PLC malware. Theor. Comput. Sci., 890:125-146, 2021. Google Scholar
  43. Ruggero Lanotte, Massimo Merro, and Andrei Munteanu. Industrial control systems security via runtime enforcement. ACM Trans. Priv. Secur., 26(1):4:1-4:41, 2023. Google Scholar
  44. Kim G. Larsen. Proof systems for satisfiability in Hennessy-Milner logic with recursion. Theoretical Computer Science, 72(2):265-288, 1990. URL: https://doi.org/10.1016/0304-3975(90)90038-J.
  45. Claudio Antares Mezzina and Jorge A. Pérez. Causally consistent reversible choreographies: A monitors-as-memories approach. In Proceedings of the 19th International Symposium on Principles and Practice of Declarative Programming, PPDP '17, pages 127-138, New York, NY, USA, 2017. Association for Computing Machinery. URL: https://doi.org/10.1145/3131851.3131864.
  46. Iain Phillips. Refusal testing. Theoretical Computer Science, 50:241-284, 1987. URL: https://doi.org/10.1016/0304-3975(87)90117-4.
  47. Amir Pnueli. The temporal logic of programs. In FOCS'77, 18th IEEE Annual Symposium on Foundations of Computer Science, Proceedings, pages 46-57. IEEE, 1977. URL: https://doi.org/10.1109/SFCS.1977.32.
  48. Amir Pnueli and Aleksandr Zaks. PSL model checking and run-time verification via testers. In FM, volume 4085 of LNCS, pages 573-586. Springer, 2006. Google Scholar
  49. George M. Reed and A. W. Roscoe. The timed failures-stability model for CSP. heoretical Computer Science, 211(1-2):85-127, 1999. URL: https://doi.org/10.1016/S0304-3975(98)00214-X.
  50. A. W. Roscoe. The Theory and Practice of Concurrency. Prentice Hall PTR, USA, 1997. Google Scholar
  51. Moshe Y. Vardi. A temporal fixpoint calculus. In Jeanne Ferrante and Peter Mager, editors, Conference Record of the Fifteenth Annual ACM Symposium on Principles of Programming Languages, pages 250-259. ACM Press, 1988. URL: https://doi.org/10.1145/73560.73582.
  52. Pierre Wolper. Temporal logic can be more expressive. Inf. Control., 56(1/2):72-99, 1983. URL: https://doi.org/10.1016/S0019-9958(83)80051-5.
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact