Top

Hint

Swipe to navigate through the chapters of this book

Published in:

Read chapter Read first chapter

2017 | Supplement | Chapter

Monitoring Hyperproperties

Authors : Bernd Finkbeiner, Christopher Hahn, Marvin Stenger, Leander Tentrup

Published in: Runtime Verification

Publisher: Springer International Publishing

Abstract

We investigate the runtime verification problem of hyperproperties, such as non-interference and observational determinism, given as formulas of the temporal logic \(\text {HyperLTL}\). \(\text {HyperLTL}\) extends linear-time temporal logic (LTL) with trace quantifiers and trace variables. We show that deciding whether a \(\text {HyperLTL}\) formula is monitorable is PSPACE-complete. For monitorable specifications, we present an efficient monitoring approach. As hyperproperties relate multiple computation traces with each other, it is necessary to store previously seen traces, and to relate new traces to the traces seen so far. If done naively, this causes the monitor to become slower and slower, before it inevitably runs out of memory. In this paper, we present techniques that reduce the set of traces that new traces must be compared against to a minimal subset. Additionally, we exploit properties of specifications such as reflexivity, symmetry, and transitivity, to reduce the number of comparisons. We show that this leads to much more scalable monitoring with, in particular, significantly lower memory consumption.

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 Combining Model Checking and Runtime Verification for Safe Robotics

next chapter TeLEx: Passive STL Learning Using Only Positive Examples

Agrawal, S., Bonakdarpour, B.: Runtime verification of k-safety hyperproperties in HyperLTL. In: Proceedings of CSF, pp. 239–252. IEEE Computer Society (2016)

Askarov, A., Sabelfeld, A.: Tight enforcement of information-release policies for dynamic languages. In: Proceedings of CSF, pp. 43–59. IEEE Computer Society (2009)

Austin, T.H., Flanagan, C.: Permissive dynamic information flow analysis. In: Proceedings of PLAS, p. 3. ACM (2010)

Bauer, A.: Monitorability of omega-regular languages. CoRR abs/1006.3638 (2010)

Bichhawat, A., Rajani, V., Garg, D., Hammer, C.: Information flow control in WebKit’s JavaScript bytecode. In: Abadi, M., Kremer, S. (eds.) POST 2014. LNCS, vol. 8414, pp. 159–178. Springer, Heidelberg (2014). doi: 10.1007/978-3-642-54792-8_9 CrossRef

Bonakdarpour, B., Finkbeiner, B.: Runtime verification for HyperLTL. In: Falcone, Y., Sánchez, C. (eds.) RV 2016. LNCS, vol. 10012, pp. 41–45. Springer, Cham (2016). doi: 10.1007/978-3-319-46982-9_4 CrossRef

Brett, N., Siddique, U., Bonakdarpour, B.: Rewriting-based runtime verification for alternation-free HyperLTL. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 77–93. Springer, Heidelberg (2017). doi: 10.1007/978-3-662-54580-5_5 CrossRef

Chudnov, A., Kuan, G., Naumann, D.A.: Information flow monitoring as abstract interpretation for relational logic. In: Proceedings of CSF, pp. 48–62. IEEE Computer Society (2014)

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). doi: 10.1007/978-3-642-54792-8_15 CrossRef

10.

Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157–1210 (2010) CrossRef

11.

d’Amorim, M., Roşu, G.: Efficient monitoring of \(\omega \)-languages. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 364–378. Springer, Heidelberg (2005). doi: 10.1007/11513988_36 CrossRef

12.

Devriese, D., Piessens, F.: Noninterference through secure multi-execution. In: Proceedings of SP, pp. 109–124. IEEE Computer Society (2010)

13.

Dimitrova, R., Finkbeiner, B., Kovács, M., Rabe, M.N., Seidl, H.: Model checking information flow in reactive systems. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 169–185. Springer, Heidelberg (2012). doi: 10.1007/978-3-642-27940-9_12 CrossRef

14.

Dimitrova, R., Finkbeiner, B., Rabe, M.N.: Monitoring temporal information flow. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012. LNCS, vol. 7609, pp. 342–357. Springer, Heidelberg (2012). doi: 10.1007/978-3-642-34026-0_26 CrossRef

15.

Finkbeiner, B., Hahn, C.: Deciding hyperproperties. In: Proceedings of CONCUR, LIPIcs, vol. 59, pp. 13:1–13:14. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2016)

16.

Finkbeiner, B., Hahn, C., Stenger, M.: EAHyper: satisfiability, implication, and equivalence checking of hyperproperties. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10427. Springer, Cham (2017). doi: 10.1007/978-3-319-63390-9_29 CrossRef

17.

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). doi: 10.1007/978-3-319-21690-4_3 CrossRef

18.

Le Guernic, G., Banerjee, A., Jensen, T., Schmidt, D.A.: Automata-based confidentiality monitoring. In: Okada, M., Satoh, I. (eds.) ASIAN 2006. LNCS, vol. 4435, pp. 75–89. Springer, Heidelberg (2007). doi: 10.1007/978-3-540-77505-8_7 CrossRef

19.

Kovács, M., Seidl, H.: Runtime enforcement of information flow security in tree manipulating processes. In: Barthe, G., Livshits, B., Scandariato, R. (eds.) ESSoS 2012. LNCS, vol. 7159, pp. 46–59. Springer, Heidelberg (2012). doi: 10.1007/978-3-642-28166-2_6 CrossRef

20.

Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems - Safety. Springer, New York (1995) CrossRefMATH

21.

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

22.

Pnueli, A.: The temporal logic of programs. In: Proceedings of FOCS, pp. 46–57. IEEE Computer Society (1977)

23.

Pnueli, A., Zaks, A.: PSL model checking and run-time verification via testers. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 573–586. Springer, Heidelberg (2006). doi: 10.1007/11813040_38 CrossRef

24.

Roscoe, A.W.: CSP and determinism in security modelling. In: Proceedings of SP, pp. 114–127. IEEE Computer Society (1995)

25.

Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Sel. Areas Commun. 21(1), 5–19 (2003) CrossRef

26.

Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. In: Proceedings of STOC, pp. 159–168. ACM (1982)

27.

Suh, G.E., Lee, J.W., Zhang, D., Devadas, S.: Secure program execution via dynamic information flow tracking. In: Proceedings of ASPLOS, pp. 85–96. ACM (2004)

28.

Tabakov, D., Rozier, K.Y., Vardi, M.Y.: Optimized temporal monitors for systemc. Formal Methods Syst. Des. 41(3), 236–268 (2012) CrossRefMATH

29.

Vanhoef, M., Groef, W.D., Devriese, D., Piessens, F., Rezk, T.: Stateful declassification policies for event-driven programs. In: Proceedings of CSF, pp. 293–307. IEEE Computer Society (2014)

30.

Zdancewic, S., Myers, A.C.: Observational determinism for concurrent program security. In: Proceedings of CSF, p. 29. IEEE Computer Society (2003)

Title: Monitoring Hyperproperties
Authors: Bernd Finkbeiner
Christopher Hahn
Marvin Stenger
Leander Tentrup
Publisher: Springer International Publishing
Book: Runtime Verification
Print ISBN: 978-3-319-67530-5

Electronic ISBN: 978-3-319-67531-2

Copyright Year: 2017
DOI: https://doi.org/10.1007/978-3-319-67531-2_12

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