Document Open Access Logo

On Runtime Enforcement via Suppressions

Authors Luca Aceto, Ian Cassar, Adrian Francalanza, Anna Ingólfsdóttir

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2018.34.pdf
  • Filesize: 0.55 MB
  • 17 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Software and its engineering → Software verification
  • Software and its engineering → Dynamic analysis
Keywords
  • Enforceability
  • Suppression Enforcement
  • Monitor Synthesis
  • Logic

Metrics

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

Abstract

Runtime enforcement is a dynamic analysis technique that uses monitors to enforce the behaviour specified by some correctness property on an executing system. The enforceability of a logic captures the extent to which the properties expressible via the logic can be enforced at runtime. We study the enforceability of Hennessy-Milner Logic with Recursion (muHML) with respect to suppression enforcement. We develop an operational framework for enforcement which we then use to formalise when a monitor enforces a muHML property. We also show that the safety syntactic fragment of the logic, sHML, is enforceable by providing an automated synthesis function that generates correct suppression monitors from sHML formulas.

Cite As Get BibTex

Luca Aceto, Ian Cassar, Adrian Francalanza, and Anna Ingólfsdóttir. On Runtime Enforcement via Suppressions. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 34:1-34:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.CONCUR.2018.34

Author Details

Luca Aceto
  • Gran Sasso Science Institute, L'Aquila, Italy
  • and, Reykjavik University, Reykjavik, Iceland
Ian Cassar
  • Reykjavik University, Reykjavik Iceland
  • and, University of Malta, Msida, Malta
Adrian Francalanza
  • University of Malta, Msida, Malta
Anna Ingólfsdóttir
  • Reykjavik University, Reykjavik, Iceland

References

  1. Luca Aceto, Antonis Achilleos, Adrian Francalanza, and Anna Ingólfsdóttir. A framework for parameterized monitorability. In Foundations of Software Science and Computation Structures, pages 203-220, Cham, 2018. Springer International Publishing. Google Scholar
  2. Luca Aceto, Antonis Achilleos, Adrian Francalanza, and Anna Ingólfsdóttir. Monitoring for silent actions. In Satya Lokam and R. Ramanujam, editors, FSTTCS 2017: Foundations of Software Technology and Theoretical Computer Science, volume 93 of LIPIcs, pages 7:1-7:14, Dagstuhl, Germany, 2018. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. Google Scholar
  3. Luca Aceto, Anna Ingólfsdóttir, Kim Guldstrand Larsen, and Jiri Srba. Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, New York, NY, USA, 2007. Google Scholar
  4. Rajeev Alur and Pavol Černý. Streaming transducers for algorithmic verification of single-pass list-processing programs. In Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 599-610. ACM, 2011. Google Scholar
  5. Henrik Reif Andersen. Partial model checking. In Proceedings of Tenth Annual IEEE Symposium on Logic in Computer Science, pages 398-407. IEEE, 1995. Google Scholar
  6. Cyrille Artho, Howard Barringer, Allen Goldberg, Klaus Havelund, Sarfraz Khurshid, Michael R. Lowry, Corina S. Pasareanu, Grigore Rosu, Koushik Sen, Willem Visser, and Richard Washington. Combining test case generation and runtime verification. Theoretical Computer Science, 336(2-3):209-234, 2005. Google Scholar
  7. Duncan Paul Attard, Ian Cassar, Adrian Francalanza, Luca Aceto, and Anna Ingolfsdottir. A Runtime Monitoring Tool for Actor-Based Systems., chapter 3, pages 49-74. River Publishers, 2017. Google Scholar
  8. Duncan Paul Attard and Adrian Francalanza. A monitoring tool for a branching-time logic. In Runtime Verification, pages 473-481, Cham, 2016. Springer International Publishing. Google Scholar
  9. Jean Berstel and Luc Boasson. Transductions and context-free languages. Ed. Teubner, pages 1-278, 1979. Google Scholar
  10. Nataliia Bielova. A theory of constructive and predictable runtime enforcement mechanisms. PhD thesis, University of Trento, 2011. Google Scholar
  11. Nataliia Bielova and Fabio Massacci. Predictability of enforcement. In International Symposium on Engineering Secure Software and Systems, pages 73-86. Springer, 2011. Google Scholar
  12. Laura Bocchi, Tzu-Chun Chen, Romain Demangeon, Kohei Honda, and Nobuko Yoshida. Monitoring networks through multiparty session types. Theoretical Computer Science, 669:33-58, 2017. Google Scholar
  13. Ian Cassar and Adrian Francalanza. On implementing a monitor-oriented programming framework for actor systems. In International Conference on Integrated Formal Methods, pages 176-192. Springer, 2016. Google Scholar
  14. Ilaria Castellani, Mariangiola Dezani-Ciancaglini, and Jorge A. Pérez. Self-adaptation and secure information flow in multiparty communications. Formal Aspects of Computing, 28(4):669-696, July 2016. Google Scholar
  15. Edward Chang, Zohar Manna, and Amir Pnueli. The safety-progress classification. In Logic and Algebra of Specification, pages 143-202. Springer, 1993. Google Scholar
  16. Clare Cini and Adrian Francalanza. An LTL proof system for runtime verification. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 581-595. Springer, 2015. Google Scholar
  17. Edmund M Clarke and E Allen Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In 25 Years of Model Checking, pages 196-215. Springer, 2008. Google Scholar
  18. Ankush Desai, Tommaso Dreossi, and Sanjit A. Seshia. Combining model checking and runtime verification for safe robotics. In Runtime Verfication (RV), LNCS, pages 172-189, Cham, 2017. Springer International Publishing. Google Scholar
  19. Yliès Falcone. You should better enforce than verify. In Runtime Verification, pages 89-105. Springer Berlin Heidelberg, 2010. Google Scholar
  20. Yliès Falcone, Jean-Claude Fernandez, and Laurent Mounier. What can you verify and enforce at runtime? International Journal on Software Tools for Technology Transfer, 14(3):349, jun 2012. Google Scholar
  21. Yliès Falcone, Laurent Mounier, Jean-Claude Fernandez, and Jean-Luc Richier. Runtime enforcement monitors: composition, synthesis, and enforcement abilities. Formal Methods in System Design, 38(3):223-262, jun 2011. Google Scholar
  22. Adrian Francalanza. A Theory of Monitors. In International Conference on Foundations of Software Science and Computation Structures, pages 145-161. Springer, 2016. Google Scholar
  23. Adrian Francalanza. Consistently-Detecting Monitors. In 28th International Conference on Concurrency Theory (CONCUR 2017), volume 85 of Leibniz International Proceedings in Informatics (LIPIcs), pages 8:1-8:19, Dagstuhl, Germany, 2017. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. Google Scholar
  24. Adrian Francalanza, Luca Aceto, Antonis Achilleos, Duncan Paul Attard, Ian Cassar, Dario Della Monica, and Anna Ingólfsdóttir. A foundation for runtime monitoring. In Runtime Verification, pages 8-29, Cham, 2017. Springer International Publishing. Google Scholar
  25. Adrian Francalanza, Luca Aceto, and Anna Ingólfsdóttir. Monitorability for the Hennessy-Milner logic with recursion. Formal Methods in System Design, 51(1):87-116, 2017. Google Scholar
  26. Adrian Francalanza and Aldrin Seychell. Synthesising correct concurrent runtime monitors. Formal Methods in System Design, 46(3):226-261, 2015. Google Scholar
  27. Limin Jia, Hannah Gommerstadt, and Frank Pfenning. Monitors and blame assignment for higher-order session types. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 582-594, New York, NY, USA, 2016. ACM. Google Scholar
  28. Katarína Kejstová, Petr Ročkai, and Jiří Barnat. From Model Checking to Runtime Verification and Back. In RV. Springer, 2017. Google Scholar
  29. Bettina Könighofer, Mohammed Alshiekh, Roderick Bloem, Laura Humphrey, Robert Könighofer, Ufuk Topcu, and Chao Wang. Shield synthesis. Formal Methods in System Design, 51(2):332-361, Nov 2017. Google Scholar
  30. Dexter C. Kozen. Results on the propositional μ-calculus. Theoretical Computer Science, 27:333-354, 1983. Google Scholar
  31. Frédéric Lang and Radu Mateescu. Partial model checking using networks of labelled transition systems and boolean equation systems. In Cormac Flanagan and Barbara König, editors, TACAS, pages 141-156, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg. Google Scholar
  32. Kim G Larsen. Proof systems for satisfiability in Hennessy-Milner logic with recursion. Theoretical Computer Science, 72(2):265-288, 1990. Google Scholar
  33. Jay Ligatti, Lujo Bauer, and David Walker. Edit automata: enforcement mechanisms for run-time security policies. International Journal of Information Security, 4(1):2-16, Feb 2005. Google Scholar
  34. Jay Ligatti and Srikar Reddy. A theory of runtime enforcement, with results. In CESORICS, pages 87-100, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg. Google Scholar
  35. Zohar Manna and Amir Pnueli. A hierarchy of temporal properties. In Cynthia Dwork, editor, Proceedings of the Ninth Annual ACM Symposium on Principles of Distributed Computing, pages 377-410. ACM, 1990. URL: http://dx.doi.org/10.1145/93385.93442.
  36. Fabio Martinelli and Ilaria Matteucci. Partial model checking, process algebra operators and satisfiability procedures for (automatically) enforcing security properties. In Foundations of Computer Security, pages 133-144. Citeseer, 2005. Google Scholar
  37. Fabio Martinelli and Ilaria Matteucci. Through modeling to synthesis of security automata. Electronic Notes in Theoretical Computer Science, 179:31-46, 2006. Google Scholar
  38. Fabio Martinelli and Ilaria Matteucci. An approach for the specification, verification and synthesis of secure systems. Electronic Notes in Theoretical Computer Science, 168:29-43, 2007. Google Scholar
  39. Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, I. Information and computation, 100(1):1-40, 1992. Google Scholar
  40. Amir Pnueli and Aleksandr Zaks. PSL model checking and run-time verification via testers. In Jayadev Misra, Tobias Nipkow, and Emil Sekerinski, editors, International Symposium on Formal Methods, pages 573-586. Springer Berlin Heidelberg, 2006. Google Scholar
  41. Alexander Moshe Rabinovich. A complete axiomatisation for trace congruence of finite state behaviors. In Proceedings of the 9th International Conference on Mathematical Foundations of Programming Semantics, pages 530-543, London, UK, UK, 1994. Springer-Verlag. Google Scholar
  42. Jacques Sakarovitch. Elements of Automata Theory. Cambridge University Press, New York, NY, USA, 2009. Google Scholar
  43. Davide Sangiorgi. Introduction to Bisimulation and Coinduction. Cambridge University Press, New York, NY, USA, 2011. Google Scholar
  44. Fred B Schneider. Enforceable security policies. ACM Transactions on Information and System Security (TISSEC), 3(1):30-50, 2000. 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact