Document Open Access Logo

On the Monitorability of Session Types, in Theory and Practice

Authors Christian Bartolo Burlò , Adrian Francalanza , Alceste Scalas

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2021.20.pdf
  • Filesize: 1.25 MB
  • 30 pages

Document Identifiers

Author Details

Christian Bartolo Burlò
  • Gran Sasso Science Institute, L'Aquila, Italy
Adrian Francalanza
  • Department of Computer Science, University of Malta, Msida, Malta
Alceste Scalas
  • DTU Compute, Technical University of Denmark, Kongens Lyngby, Denmark

Funding

This work has been partly supported by: the project MoVeMnt (No: 217987-051) under the Icelandic Research Fund; the BehAPI project funded by the EU H2020 RISE under the Marie Skłodowska-Curie action (No: 778233); the EU Horizon 2020 project 830929 CyberSec4Europe; the Danish Industriens Fonds Cyberprogram 2020-0489 Security-by-Design in Digital Denmark.

Cite As Get BibTex

Christian Bartolo Burlò, Adrian Francalanza, and Alceste Scalas. On the Monitorability of Session Types, in Theory and Practice. In 35th European Conference on Object-Oriented Programming (ECOOP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 194, pp. 20:1-20:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.ECOOP.2021.20

Abstract

Software components are expected to communicate according to predetermined protocols and APIs. Numerous methods have been proposed to check the correctness of communicating systems against such protocols/APIs. Session types are one such method, used both for static type-checking as well as for run-time monitoring. This work takes a fresh look at the run-time verification of communicating systems using session types, in theory and in practice. On the theoretical side, we develop a formal model of session-monitored processes. We then use this model to formulate and prove new results on the monitorability of session types, defined in terms of soundness (i.e., whether monitors only flag ill-typed processes) and completeness (i.e., whether all ill-typed processes can be flagged by a monitor). On the practical side, we show that our monitoring theory is indeed realisable: we instantiate our formal model as a Scala toolkit (called STMonitor) for the automatic generation of session monitors. These executable monitors can be used as proxies to instrument communication across black-box processes written in any programming language. Finally, we evaluate the viability of our approach through a series of benchmarks.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Development frameworks and environments
  • Software and its engineering → Software verification and validation
  • Theory of computation → Concurrency
Keywords
  • Session types
  • monitorability
  • monitor correctness
  • Scala

Metrics

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

Related Versions

Supplementary Materials

References

  1. Luca Aceto, Antonis Achilleos, Adrian Francalanza, and Anna Ingólfsdóttir. Monitoring for silent actions. In FSTTCS, volume 93 of LIPIcs, pages 7:1-7:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. Google Scholar
  2. Luca Aceto, Antonis Achilleos, Adrian Francalanza, and Anna Ingólfsdóttir. A framework for parameterized monitorability. In FoSSaCS, volume 10803 of Lecture Notes in Computer Science, pages 203-220. Springer, 2018. Google Scholar
  3. 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., 3(POPL):52:1-52:29, 2019. URL: https://doi.org/10.1145/3290365.
  4. Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen. An operational guide to monitorability. In SEFM, volume 11724 of Lecture Notes in Computer Science, pages 433-453. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-30446-1_23.
  5. Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen. The best a monitor can do. In CSL, volume 183 of LIPIcs, pages 7:1-7:23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. Google Scholar
  6. 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. URL: https://doi.org/10.1007/s10270-020-00860-z.
  7. Luca Aceto, Duncan Paul Attard, Adrian Francalanza, and Anna Ingólfsdóttir. A choreographed outline instrumentation algorithm for asynchronous components. CoRR, abs/2104.09433, 2021. URL: https://arxiv.org/abs/2104.09433.
  8. Luca Aceto, Duncan Paul Attard, Adrian Francalanza, and Anna Ingólfsdóttir. On benchmarking for concurrent runtime verification. In FASE, volume 12649 of Lecture Notes in Computer Science, pages 3-23. Springer, 2021. Google Scholar
  9. Luca Aceto, Ian Cassar, Adrian Francalanza, and Anna Ingólfsdóttir. On runtime enforcement via suppressions. In CONCUR, volume 118 of LIPIcs, pages 34:1-34:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2018.34.
  10. Amal Ahmed, Robert Bruce Findler, Jeremy G. Siek, and Philip Wadler. Blame for all. In POPL, pages 201-214. ACM, 2011. URL: https://doi.org/10.1145/1926385.1926409.
  11. Davide Ancona, Viviana Bono, Mario Bravetti, Joana Campos, Giuseppe Castagna, Pierre-Malo Deniélou, Simon J. Gay, Nils Gesbert, Elena Giachino, Raymond Hu, Einar Broch Johnsen, Francisco Martins, Viviana Mascardi, Fabrizio Montesi, Rumyana Neykova, Nicholas Ng, Luca Padovani, Vasco T. Vasconcelos, and Nobuko Yoshida. Behavioral types in programming languages. Found. Trends Program. Lang., 3(2-3):95-230, 2016. URL: https://doi.org/10.1561/2500000031.
  12. Duncan Paul Attard and Adrian Francalanza. Trace partitioning and local monitoring for asynchronous components. In SEFM, volume 10469 of Lecture Notes in Computer Science, pages 219-235. Springer, 2017. Google Scholar
  13. Ezio Bartocci, Yliès Falcone, Adrian Francalanza, and Giles Reger. Introduction to runtime verification. In Lectures on Runtime Verification, volume 10457 of Lecture Notes in Computer Science, pages 1-33. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-75632-5_1.
  14. David A. Basin, Thibault Dardinier, Lukas Heimes, Srdan Krstic, Martin Raszyk, Joshua Schneider, and Dmitriy Traytel. A formally verified, optimized monitor for metric first-order dynamic logic. In IJCAR (1), volume 12166 of Lecture Notes in Computer Science, pages 432-453. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51074-9_25.
  15. Andreas Bauer and Yliès Falcone. Decentralised LTL monitoring. Formal Methods Syst. Des., 48(1-2):46-93, 2016. Google Scholar
  16. Jeremy Blackburn, Ivory Hernandez, Jay Ligatti, and Michael Nachtigal. Completely subtyping iso-recursive types. Technical Report CSE-071012, University of South Florida, 2012. Google Scholar
  17. 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. URL: https://doi.org/10.1016/j.tcs.2017.02.009.
  18. Alan Brown, Jerry Fishenden, and Mark Thompson. API Economy, Ecosystems and Engagement Models, pages 225-236. Palgrave Macmillan UK, London, 2014. URL: https://doi.org/10.1057/9781137443649_13.
  19. Christian Batrolo Burlò, Adrian Francalanza, and Alceste Scalas. On the monitorability of session types, in theory and practice (extended version), 2021. URL: http://arxiv.org/abs/2105.06291.
  20. Francesco Cesarini and Simon Thompson. ERLANG Programming. O’Reilly Media, Inc., 1st edition, 2009. Google Scholar
  21. Tzu-Chun Chen, Laura Bocchi, Pierre-Malo Deniélou, Kohei Honda, and Nobuko Yoshida. Asynchronous distributed monitoring for multiparty session enforcement. In TGC, volume 7173 of Lecture Notes in Computer Science, pages 25-45. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-30065-3_2.
  22. Tzu-Chun Chen, Mariangiola Dezani-Ciancaglini, Alceste Scalas, and Nobuko Yoshida. On the preciseness of subtyping in session types. Log. Methods Comput. Sci., 13(2), 2017. URL: https://doi.org/10.23638/LMCS-13(2:12)2017.
  23. Arthur Azevedo de Amorim, Maxime Dénès, Nick Giannarakis, Catalin Hritcu, Benjamin C. Pierce, Antal Spector-Zabusky, and Andrew Tolmach. Micro-policies: Formally verified, tag-based security monitors. In IEEE Symposium on Security and Privacy, pages 813-830. IEEE Computer Society, 2015. URL: https://doi.org/10.1109/SP.2015.55.
  24. Romain Demangeon, Kohei Honda, Raymond Hu, Rumyana Neykova, and Nobuko Yoshida. Practical interruptible conversations: distributed dynamic verification with multiparty session types and python. Formal Methods Syst. Des., 46(3):197-225, 2015. URL: https://doi.org/10.1007/s10703-014-0218-8.
  25. Bernd Finkbeiner, Christopher Hahn, Marvin Stenger, and Leander Tentrup. Monitoring hyperproperties. Formal Methods Syst. Des., 54(3):336-363, 2019. Google Scholar
  26. Adrian Francalanza. A theory of monitors - (extended abstract). In FoSSaCS, volume 9634 of Lecture Notes in Computer Science, pages 145-161. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49630-5_9.
  27. Adrian Francalanza. Consistently-detecting monitors. In CONCUR, volume 85 of LIPIcs, pages 8:1-8:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2017.8.
  28. Adrian Francalanza. A Theory of Monitors. Information and Computation, page 104704, 2021. URL: https://doi.org/10.1016/j.ic.2021.104704.
  29. 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 RV, volume 10548 of Lecture Notes in Computer Science, pages 8-29. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-67531-2_2.
  30. 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.
  31. Adrian Francalanza and Jasmine Xuereb. On implementing symbolic controllability. In COORDINATION, volume 12134 of Lecture Notes in Computer Science, pages 350-369. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-50029-0_22.
  32. Silvia Ghilezan, Svetlana Jaksic, Jovanka Pantovic, Alceste Scalas, and Nobuko Yoshida. Precise subtyping for synchronous multiparty sessions. J. Log. Algebraic Methods Program., 104:127-173, 2019. URL: https://doi.org/10.1016/j.jlamp.2018.12.002.
  33. Silvia Ghilezan, Jovanka Pantovic, Ivan Prokic, Alceste Scalas, and Nobuko Yoshida. Precise subtyping for asynchronous multiparty sessions. Proc. ACM Program. Lang., 5(POPL):1-28, 2021. URL: https://doi.org/10.1145/3434297.
  34. Hannah Gommerstadt, Limin Jia, and Frank Pfenning. Session-typed concurrent contracts. In ESOP, volume 10801 of Lecture Notes in Computer Science, pages 771-798. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-89884-1_27.
  35. Ruben Hamers and Sung-Shik Jongmans. Discourje: Runtime verification of communication protocols in clojure. In TACAS (1), volume 12078 of Lecture Notes in Computer Science, pages 266-284. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-45190-5_15.
  36. Kohei Honda. Types for dyadic interaction. In CONCUR, volume 715 of Lecture Notes in Computer Science, pages 509-523. Springer, 1993. URL: https://doi.org/10.1007/3-540-57208-2_35.
  37. Kohei Honda, Vasco Thudichum Vasconcelos, and Makoto Kubo. Language primitives and type discipline for structured communication-based programming. In ESOP, volume 1381 of Lecture Notes in Computer Science, pages 122-138. Springer, 1998. URL: https://doi.org/10.1007/BFb0053567.
  38. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. In POPL, pages 273-284. ACM, 2008. URL: https://doi.org/10.1145/1328438.1328472.
  39. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. J. ACM, 63(1):9:1-9:67, 2016. URL: https://doi.org/10.1145/2827695.
  40. Raymond Hu, Rumyana Neykova, Nobuko Yoshida, Romain Demangeon, and Kohei Honda. Practical interruptible conversations - distributed dynamic verification with session types and python. In RV, volume 8174 of Lecture Notes in Computer Science, pages 130-148. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-40787-1_8.
  41. Atsushi Igarashi, Peter Thiemann, Vasco T. Vasconcelos, and Philip Wadler. Gradual session types. Proc. ACM Program. Lang., 1(ICFP):38:1-38:28, 2017. URL: https://doi.org/10.1145/3110282.
  42. Limin Jia, Hannah Gommerstadt, and Frank Pfenning. Monitors and blame assignment for higher-order session types. In POPL, pages 582-594. ACM, 2016. URL: https://doi.org/10.1145/2837614.2837662.
  43. 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.
  44. Jay Ligatti, Jeremy Blackburn, and Michael Nachtigal. On subtyping-relation completeness, with an application to iso-recursive types. ACM Trans. Program. Lang. Syst., 39(1):4:1-4:36, 2017. URL: https://doi.org/10.1145/2994596.
  45. Kim Guldstrand Larsen Luca Aceto, Anna Ingólfsdóttir and Jiri Srba. Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, 2007. Google Scholar
  46. Hernán C. Melgratti and Luca Padovani. Chaperone contracts for higher-order sessions. Proc. ACM Program. Lang., 1(ICFP):35:1-35:29, 2017. URL: https://doi.org/10.1145/3110279.
  47. Network Working Group. RFC 5321: Simple Mail Transfer Protocol. https://tools.ietf.org/html/rfc5321, 2008.
  48. Rumyana Neykova, Raymond Hu, Nobuko Yoshida, and Fahd Abdeljallal. A session type provider: compile-time API generation of distributed protocols with refinements in f#. In CC, pages 128-138. ACM, 2018. URL: https://doi.org/10.1145/3178372.3179495.
  49. Rumyana Neykova and Nobuko Yoshida. Let it recover: multiparty protocol-induced recovery. In CC, pages 98-108. ACM, 2017. URL: https://doi.org/10.1145/3033019.
  50. Rumyana Neykova, Nobuko Yoshida, and Raymond Hu. SPY: local verification of global protocols. In RV, volume 8174 of Lecture Notes in Computer Science, pages 358-363. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-40787-1_25.
  51. Doron A. Peled. Specification and verification using message sequence charts. Electron. Notes Theor. Comput. Sci., 65(7):51-64, 2002. URL: https://doi.org/10.1016/S1571-0661(04)80484-5.
  52. Iain Phillips. Refusal testing. Theor. Comput. Sci., 50:241-284, 1987. Google Scholar
  53. Benjamin C. Pierce. Types and Programming Languages. The MIT Press, 1st edition, 2002. Google Scholar
  54. Alceste Scalas, Ornela Dardha, Raymond Hu, and Nobuko Yoshida. A linear decomposition of multiparty sessions for safe distributed programming. In ECOOP, volume 74 of LIPIcs, pages 24:1-24:31. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2017.24.
  55. Alceste Scalas, Ornela Dardha, Raymond Hu, and Nobuko Yoshida. A linear decomposition of multiparty sessions for safe distributed programming (artifact). Dagstuhl Artifacts Ser., 3(2):03:1-03:2, 2017. URL: https://doi.org/10.4230/DARTS.3.2.3.
  56. Alceste Scalas and Nobuko Yoshida. Lightweight session programming in scala. In ECOOP, volume 56 of LIPIcs, pages 21:1-21:28. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2016.21.
  57. Fred B. Schneider. Enforceable security policies. ACM Trans. Inf. Syst. Secur., 3(1):30-50, 2000. URL: https://doi.org/10.1145/353323.353382.
  58. Scribble homepage, 2020. URL: http://www.scribble.org.
  59. SecuritySpace. Mail (MX) server survey, 2021. URL: http://www.securityspace.com/s_survey/data/man.202103/mxsurvey.html.
  60. Paula Severi and Mariangiola Dezani-Ciancaglini. Observational equivalence for multiparty sessions. Fundam. Informaticae, 170(1-3):267-305, 2019. URL: https://doi.org/10.3233/FI-2019-1863.
  61. Sharon Shoham, Eran Yahav, Stephen Fink, and Marco Pistoia. Static specification mining using automata-based abstractions. In ISSTA, pages 174-184. ACM, 2007. URL: https://doi.org/10.1145/1273463.1273487.
  62. Fu Song and Tayssir Touili. Model-checking software library API usage rules. In IFM, volume 7940 of Lecture Notes in Computer Science, pages 192-207. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-38613-8_14.
  63. Lucas Waye, Stephen Chong, and Christos Dimoulas. Whip: higher-order contracts for modern services. Proc. ACM Program. Lang., 1(ICFP):36:1-36:28, 2017. Google Scholar
  64. Nobuko Yoshida, Raymond Hu, Rumyana Neykova, and Nicholas Ng. The Scribble protocol language. In TGC, volume 8358 of Lecture Notes in Computer Science, pages 22-41. Springer, 2013. URL: https://doi.org/10.1007/978-3-319-05119-2_3.
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 About DROPS Imprint Privacy Contact