Top

Hint

Swipe to navigate through the chapters of this book

Published in:

Read chapter Read first chapter

2021 | OriginalPaper | Chapter

Runtime Enforcement of Hyperproperties

Authors : Norine Coenen, Bernd Finkbeiner, Christopher Hahn, Jana Hofmann, Yannick Schillo

Published in: Automated Technology for Verification and Analysis

Publisher: Springer International Publishing

Abstract

An enforcement mechanism monitors a reactive system for undesired behavior at runtime and corrects the system’s output in case it violates the given specification. In this paper, we study the enforcement problem for hyperproperties, i.e., properties that relate multiple computation traces to each other. We elaborate the notion of sound and transparent enforcement mechanisms for hyperproperties in two trace input models: 1) the parallel trace input model, where the number of traces is known a-priori and all traces are produced and processed in parallel and 2) the sequential trace input model, where traces are processed sequentially and no a-priori bound on the number of traces is known. For both models, we study enforcement algorithms for specifications given as formulas in universally quantified HyperLTL, a temporal logic for hyperproperties. For the parallel model, we describe an enforcement mechanism based on parity games. For the sequential model, we show that enforcement is in general undecidable and present algorithms for reasonable simplifications of the problem (partial guarantees or the restriction to safety properties). Furthermore, we report on experimental results of our prototype implementation for the parallel model.

To get access to this content you need the following product:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

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

über 69.000 Bücher
über 500 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 90 Tage mit der neuen Mini-Lizenz testen!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 50.000 Bücher
über 380 Zeitschriften

aus folgenden Fachgebieten:

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

Jetzt 90 Tage mit der neuen Mini-Lizenz testen!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 58.000 Bücher
über 300 Zeitschriften

aus folgenden Fachgebieten:

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

Jetzt 90 Tage mit der neuen Mini-Lizenz testen!

inform now

previous chapter Verification by Gambling on Program Slices

next chapter Compositional Synthesis of Modular Systems

REHyper is available at https://github.com/reactive-systems/REHyper.

Agrawal, S., Bonakdarpour, B.: Runtime verification of k-safety hyperproperties in HyperLTL. In: CSF 2016 (2016)

Beeri, C.: On the membership problem for functional and multivalued dependencies in relational databases. ACM Trans. Database Syst. 5(3), 241–259 (1980) CrossRef

Bloem, R., Könighofer, B., Könighofer, R., Wang, C.: Shield synthesis: runtime enforcement for reactive systems. CoRR abs/1501.02573 (2015)

Bonakdarpour, B., Finkbeiner, B.: The complexity of monitoring hyperproperties. In: CSF 2018 (2018)

Bozzelli, L., Maubert, B., Pinchinat, S.: Unifying hyper and epistemic temporal logics. In: Pitts, A. (ed.) FoSSaCS 2015. LNCS, vol. 9034, pp. 167–182. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46678-0_11 CrossRefMATH

Clarkson, M.R., Schneider, F.B.: Hyperproperties. In: CSF 2008 (2008)

Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., Sánchez, C.: Temporal logics for hyperproperties. In: Abadi, M., Kremer, S. (eds.) POST 2014. LNCS, vol. 8414, pp. 265–284. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54792-8_15 CrossRef

Coenen, N., Finkbeiner, B., Hahn, C., Hofmann, J.: The hierarchy of hyperlogics. In: LICS 2019 (2019)

Coenen, N., Finkbeiner, B., Sánchez, C., Tentrup, L.: Verifying hyperliveness. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 121–139. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-25540-4_7 CrossRef

10.

Devriese, D., Piessens, F.: Noninterference through secure multi-execution. In: S&P 2010 (2010)

11.

Ehlers, R., Finkbeiner, B.: Monitoring realizability. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 427–441. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-29860-8_34 CrossRef

12.

Erlingsson, U., Schneider, F.B.: SASI enforcement of security policies: a retrospective. In: NSPW 1999 (1999)

13.

Esparza, Javier, Křetínský, Jan, Raskin, Jean-François., Sickert, Salomon: From LTL and limit-deterministic Büchi automata to deterministic parity automata. In: Legay, Axel, Margaria, Tiziana (eds.) TACAS 2017. LNCS, vol. 10205, pp. 426–442. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54577-5_25 CrossRefMATH

14.

Falcone, Y.: You should better enforce than verify. In: Barringer, H., et al. (eds.) RV 2010. LNCS, vol. 6418, pp. 89–105. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16612-9_9 CrossRef

15.

Falcone, Y., Fernandez, J., Mounier, L.: What can you verify and enforce at runtime? Int. J. Softw. Tools Technol. Transf. 14(3), 349–382 (2012). https://doi.org/10.1007/s10009-011-0196-8 CrossRef

16.

Falcone, Y., Mounier, L., Fernandez, J.C., Richier, J.L.: Runtime enforcement monitors: composition, synthesis, and enforcement abilities. Form. Methods Syst. Des. 38, 223–262 (2011). https://doi.org/10.1007/s10703-011-0114-4 CrossRefMATH

17.

Falcone, Y., Pinisetty, S.: On the runtime enforcement of timed properties. In: Finkbeiner, B., Mariani, L. (eds.) RV 2019. LNCS, vol. 11757, pp. 48–69. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-32079-9_4 CrossRef

18.

Finkbeiner, B., Hahn, C., Lukert, P., Stenger, M., Tentrup, L.: Synthesizing reactive systems from hyperproperties. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 289–306. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-96145-3_16 CrossRef

19.

Finkbeiner, B., Hahn, C., Stenger, M., Tentrup, L.: Monitoring hyperproperties. Form. Methods Syst. Des. 54(3), 336–363 (2019). https://doi.org/10.1007/s10703-019-00334-z CrossRefMATH

20.

Finkbeiner, B., Hahn, C., Stenger, M., Tentrup, L.: \(\text{ RVHyper }\): a runtime verification tool for temporal hyperproperties. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 194–200. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89963-3_11 CrossRef

21.

Finkbeiner, B., Hahn, C., Torfah, H.: Model checking quantitative hyperproperties. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 144–163. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-96145-3_8 CrossRef

22.

Finkbeiner, B., Rabe, M.N., Sánchez, C.: Algorithms for model checking HyperLTL and HyperCTL \(^*\). In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 30–48. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_3 CrossRef

23.

Friedmann, O., Lange, M.: The PGSolver Collection of Parity Game Solvers Version 3 (2010)

24.

Hahn, C., Stenger, M., Tentrup, L.: Constraint-based monitoring of hyperproperties. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11428, pp. 115–131. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17465-1_7 CrossRef

25.

Kupferman, O., Vardi, M.Y.: Model checking of safety properties. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 172–183. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48683-6_17 CrossRef

26.

Lamport, L.: A new solution of Dijkstra’s concurrent programming problem. Commun. ACM 17(8), 453–455 (1974) MathSciNetCrossRef

27.

Li, X., et al.: Digital health: tracking physiomes and activity using wearable biosensors reveals useful health-related information. PLoS Biol. 15, e2001402 (2017) CrossRef

28.

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

29.

Luo, Q., Roundefinedu, G.: EnforceMOP: a runtime property enforcement system for multithreaded programs. In: ISSTA 2013 (2013)

30.

McLean, J.: Proving noninterference and functional correctness using traces. J. Comput. Secur. 1(1), 37–58 (1992) CrossRef

31.

Meyer, P.J., Sickert, S., Luttenberger, M.: Strix: explicit reactive synthesis strikes back! In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 578–586. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-96145-3_31 CrossRef

32.

Ngo, M., Massacci, F., Milushev, D., Piessens, F.: Runtime enforcement of security policies on black box reactive programs. In: POPL 2015 (2015)

33.

Norman, G., Shmatikov, V.: Analysis of probabilistic contract signing. J. Comput. Secur. 14(6), 561–589 (2006)

34.

Parys, P.: Parity games: Zielonka’s algorithm in quasi-polynomial time. In: MFCS 2019 (2019)

35.

Pnueli, A.: The temporal logic of programs. In: SFCS 1977 (1977)

36.

Renard, M., Falcone, Y., Rollet, A., Jéron, T., Marchand, H.: Optimal enforcement of (timed) properties with uncontrollable events. In: MSCS 2019 (2019)

37.

Roscoe, A.W.: CSP and determinism in security modelling. In: S&P 1995 (1995)

38.

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

39.

Stucki, S., Sánchez, C., Schneider, G., Bonakdarpour, B.: Gray-box monitoring of hyperproperties. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 406–424. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-30942-8_25 CrossRef

40.

Wu, M., Zeng, H., Wang, C.: Synthesizing runtime enforcer of safety properties under burst error. In: Rayadurgam, S., Tkachuk, O. (eds.) NFM 2016. LNCS, vol. 9690, pp. 65–81. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40648-0_6 CrossRef

41.

Zdancewic, S., Myers, A.C.: Observational determinism for concurrent program security. In: CSFW-16 (2003)

Title: Runtime Enforcement of Hyperproperties
Authors: Norine Coenen
Bernd Finkbeiner
Christopher Hahn
Jana Hofmann
Yannick Schillo
Publisher: Springer International Publishing
Book: Automated Technology for Verification and Analysis
Print ISBN: 978-3-030-88884-8

Electronic ISBN: 978-3-030-88885-5

Copyright Year: 2021
DOI: https://doi.org/10.1007/978-3-030-88885-5_19

Springer Professional

Hint

Swipe to navigate through the chapters of this book

Abstract

Please log in to get access to this content

To get access to this content you need the following product:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner