nach oben

Erschienen in:

2021 | OriginalPaper | Buchkapitel

On Bidirectional Runtime Enforcement

verfasst von : Luca Aceto, Ian Cassar, Adrian Francalanza, Anna Ingólfsdóttir

Erschienen in: Formal Techniques for Distributed Objects, Components, and Systems

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Runtime enforcement is a dynamic analysis technique that instruments a monitor with a system in order to ensure its correctness as specified by some property. This paper explores bidirectional enforcement strategies for properties describing the input and output behaviour of a system. We develop an operational framework for bidirectional enforcement and use it to study the enforceability of the safety fragment of Hennessy-Milner logic with recursion (sHML). We provide an automated synthesis function that generates correct monitors from sHML formulas, and show that this logic is enforceable via a specific type of bidirectional enforcement monitors called action disabling monitors.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Nächstes Kapitel A Multi-agent Model for Polarization Under Confirmation Bias in Social Networks

These transducers were originally introduced in [5] for unidirectional enforcement.

Aceto, L., Achilleos, A., Francalanza, A., Ingólfsdóttir, A.: A framework for parameterized monitorability. In: Baier, C., Dal Lago, U. (eds.) FoSSaCS 2018. LNCS, vol. 10803, pp. 203–220. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89366-2_11CrossRef

Aceto, L., Achilleos, A., Francalanza, A., Ingólfsdóttir, A., Kjartansson, S.Ö.: Determinizing monitors for HML with recursion. J. Log. Algebraic Methods Program. 111, (2020). https://doi.org/10.1016/j.jlamp.2019.100515

Aceto, L., Achilleos, A., Francalanza, A., Ingólfsdóttir, A., Lehtinen, K.: The Best a Monitor Can Do. In: CSL. LIPIcs, vol. 183, pp. 7:1–7:23. Schloss Dagstuhl (2021). https://doi.org/10.4230/LIPIcs.CSL.2021.7

Aceto, L., Attard, D.P., Francalanza, A., Ingólfsdóttir, A.: On benchmarking for concurrent runtime verification. FASE 2021. LNCS, vol. 12649, pp. 3–23. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-71500-7_1CrossRef

Aceto, L., Cassar, I., Francalanza, A., Ingólfsdóttir, A.: On Runtime Enforcement via Suppressions. In: CONCUR. vol. 118, pp. 34:1–34:17. Schloss Dagstuhl (2018). https://doi.org/10.4230/LIPIcs.CONCUR.2018.34

Aceto, L., Cassar, I., Francalanza, A., Ingólfsdóttir, A.: On bidirectional enforcement. Technical report Reykjavik University (2020). http://icetcs.ru.is/theofomon/bidirectionalRE.pdf

Aceto, L., Ingólfsdóttir, A.: Testing Hennessy-Milner logic with recursion. In: Thomas, W. (ed.) FoSSaCS 1999. LNCS, vol. 1578, pp. 41–55. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-49019-1_4CrossRef

Aceto, L., Ingólfsdóttir, A., Larsen, K.G., Srba, J.: Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, NY, USA (2007)CrossRef

Alur, R., Černý, P.: Streaming Transducers for Algorithmic Verification of Single-pass List-processing Programs. In: POPL, pp. 599–610. ACM (2011). https://doi.org/10.1145/1926385.1926454

10.

Attard, D.P., Francalanza, A.: A monitoring tool for a branching-time logic. In: Falcone, Y., Sánchez, C. (eds.) RV 2016. LNCS, vol. 10012, pp. 473–481. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46982-9_31CrossRef

11.

Bielova, N., Massacci, F.: Do you really mean what you actually enforced?-edited automata revisited. J. Inf. Secur. 10(4), 239–254 (2011). https://doi.org/10.1007/s10207-011-0137-2CrossRef

12.

Bocchi, L., Chen, T.C., Demangeon, R., Honda, K., Yoshida, N.: Monitoring networks through multiparty session types. TCS 669, 33–58 (2017)MathSciNetCrossRef

13.

Cassar, I.: Developing Theoretical Foundations for Runtime Enforcement. Ph.D. thesis, University of Malta and Reykjavik University (2021)

14.

Cassar, I., Francalanza, A., Aceto, L., Ingólfsdóttir, A.: eAOP: an aspect oriented programming framework for Erlang. In: Erlang. ACM SIGPLAN (2017)

15.

Cassar, I., Francalanza, A., Attard, D.P., Aceto, L., Ingólfsdóttir, A.: A Suite of Monitoring Tools for Erlang. In: RV-CuBES. Kalpa Publications in Computing, vol. 3, pp. 41–47. EasyChair (2017)

16.

Cassar, I., Francalanza, A., Said, S.: Improving Runtime Overheads for detectEr. In: FESCA. EPTCS, vol. 178, pp. 1–8 (2015)

17.

Chen, T.-C., Bocchi, L., Deniélou, P.-M., Honda, K., Yoshida, N.: Asynchronous distributed monitoring for multiparty session enforcement. In: Bruni, R., Sassone, V. (eds.) TGC 2011. LNCS, vol. 7173, pp. 25–45. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-30065-3_2CrossRef

18.

Falcone, Y., Fernandez, J.-C., Mounier, L.: Synthesizing Enforcement Monitors w.r.t. the safety-progress classification of properties. In: Sekar, R., Pujari, A.K. (eds.) ICISS 2008. LNCS, vol. 5352, pp. 41–55. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-89862-7_3CrossRef

19.

Falcone, Y., Fernandez, J.C., Mounier, L.: What can you verify and enforce at runtime? J. Softw. Tools Technol. Transf. 14(3), 349 (2012)CrossRef

20.

Francalanza, A.: Consistently-Detecting Monitors. In: CONCUR. LIPIcs, vol. 85, pp. 8:1–8:19. Dagstuhl, Germany (2017). https://doi.org/10.4230/LIPIcs.CONCUR.2017.8

21.

Francalanza, A.: A theory of monitors. Inf. Comput 104704 (2021). https://doi.org/10.1016/j.ic.2021.104704

22.

Francalanza, A., Aceto, L., Ingólfsdóttir, A.: Monitorability for the Hennessy-Milner logic with recursion. Formal Methods Syst. Des. 51(1), 87–116 (2017)CrossRef

23.

Hennessy, M., Lin, H.: Proof systems for message-passing process algebras. Formal Aspects Comput. 8(4), 379–407 (1996). https://doi.org/10.1007/BF01213531CrossRefMATH

24.

Hennessy, M., Liu, X.: A modal logic for message passing processes. Acta Inf. 32(4), 375–393 (1995). https://doi.org/10.1007/BF01178384MathSciNetCrossRefMATH

25.

van Hulst, A.C., Reniers, M.A., Fokkink, W.J.: Maximally permissive controlled system synthesis for non-determinism and modal logic. Discr. Event Dyn. Syst. 27(1), 109–142 (2017)MathSciNetCrossRef

26.

Jia, L., Gommerstadt, H., Pfenning, F.: Monitors and blame assignment for higher-order session types. In: POPL, pp. 582–594. ACM, NY, USA (2016)

27.

Khoury, R., Tawbi, N.: Which security policies are enforceable by runtime monitors? A survey. Comput. Sci. Rev. 6(1), 27–45 (2012). https://doi.org/10.1016/j.cosrev.2012.01.001CrossRefMATH

28.

Könighofer, B., et al.: Shield synthesis. Formal Methods Syst. Des. 51(2), 332–361 (2017). https://doi.org/10.1007/s10703-017-0276-9CrossRefMATH

29.

Kozen, D.C.: Results on the propositional \(\mu \)-calculus. Theor. Comput. Sci. 27, 333–354 (1983)MathSciNetCrossRef

30.

Lanotte, R., Merro, M., Munteanu, A.: Runtime enforcement for control system security. In: CSF, pp. 246–261. IEEE (2020). https://doi.org/10.1109/CSF49147.2020.00025

31.

Larsen, K.G.: Proof systems for satisfiability in Hennessy-Milner logic with recursion. Theor. Comput. Sci. 72(2), 265–288 (1990). https://doi.org/10.1016/0304-3975(90)90038-JMathSciNetCrossRefMATH

32.

Ligatti, J., Bauer, L., Walker, D.: Edit automata: enforcement mechanisms for run-time security policies. J. Inf. Secur. 4(1), 2–16 (2005). https://doi.org/10.1007/s10207-004-0046-8CrossRef

33.

Ligatti, J., Bauer, L., Walker, D.: Run-time enforcement of nonsafety policies. ACM Trans. Inf. Syst. Secur. 12(3), 19:1–19:41 (2009)CrossRef

34.

Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes. I. Inf. Comput. 100(1), 1–40 (1992). https://doi.org/10.1016/0890-5401(92)90008-4MathSciNetCrossRefMATH

35.

Pinisetty, S., Roop, P.S., Smyth, S., Allen, N., Tripakis, S., Hanxleden, R.V.: Runtime enforcement of cyber-physical systems. ACM Trans. Embed. Comput. Syst. 16(5s), 1–25 (2017)CrossRef

36.

Rathke, J., Hennessy, M.: Local model checking for value-passing processes (extended abstract). In: Abadi, M., Ito, T. (eds.) TACS 1997. LNCS, vol. 1281, pp. 250–266. Springer, Heidelberg (1997). https://doi.org/10.1007/BFb0014555CrossRef

37.

Sakarovitch, J.: Elements of Automata Theory. Cambridge University Press, New York, NY, USA (2009)CrossRef

38.

Sangiorgi, D.: Introduction to Bisimulation and Coinduction. Cambridge University Press, New York, NY, USA (2011)CrossRef

39.

Schneider, F.B.: Enforceable security policies. ACM Trans. Inf. Syst. Secur. (TISSEC) 3(1), 30–50 (2000)CrossRef

Titel: On Bidirectional Runtime Enforcement
verfasst von: Luca Aceto
Ian Cassar
Adrian Francalanza
Anna Ingólfsdóttir
Verlag: Springer International Publishing
Buch: Formal Techniques for Distributed Objects, Components, and Systems
Print ISBN: 978-3-030-78088-3

Electronic ISBN: 978-3-030-78089-0

Copyright-Jahr: 2021
DOI: https://doi.org/10.1007/978-3-030-78089-0_1

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"