Skip to main content
SpringerLink
Log in
SpringerLink
Log in

Runtime Verification for HyperLTL

  • Conference paper
  • First Online:
Runtime Verification (RV 2016)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10012))

Included in the following conference series:

Abstract

Information flow security often involves reasoning about multiple execution traces. This subtlety stems from the fact that an intruder may gain knowledge about the system through observing and comparing several executions. The monitoring of such properties of sets of traces, also known as hyperproperties, is a challenge for runtime verification, because most monitoring techniques are limited to the analysis of a single trace. In this tutorial, we discuss this challenge with respect to HyperLTL, a temporal logic for the specification of hyperproperties.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Agrawal, S., Bonakdarpour, B.: Runtime verification of \(k\)-safety hyperproperties in hyperltl. In: Proceedings of the 29th IEEE Computer Security Foundations Symposium (CSF) (2016, to appear)

    Google Scholar 

  2. Alur, R., Černý, P., Zdancewic, S.: Preserving secrecy under refinement. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol. 4052, pp. 107–118. Springer, Heidelberg (2006). doi:10.1007/11787006_10

    Chapter  Google Scholar 

  3. Balliu, M., Dam, M., Guernic, G.L.: Epistemic temporal logic for information flow security. In: Proceedings of the 2011 Workshop on Programming Languages and Analysis for Security, PLAS 2011, San Jose, CA, p. 6, June 2011

    Google Scholar 

  4. Barthe, G., D’Argenio, P.R., Rezk, T.: Secure information flow by self-composition. In: CSFW, pp. 100–114 (2004)

    Google Scholar 

  5. Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol. 20(4), 14 (2011)

    Article  Google Scholar 

  6. 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

    Chapter  Google Scholar 

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

    Article  Google Scholar 

  8. 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

    Chapter  Google Scholar 

  9. 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

    Chapter  Google Scholar 

  10. Finkbeiner, B., Hahn, C.: Deciding hyperproperties. In: Proceedings of the CONCUR 2016 (2016)

    Google Scholar 

  11. Finkbeiner, B., Rabe, M.N.: The linear-hyper-branching spectrum of temporal logics. IT Inform. Technol. 56(6), 273–279 (2014)

    Article  Google Scholar 

  12. Finkbeiner, B., Rabe, M.N., Sanchez, C.: Algorithms for model checking HyperLTL and HyperCTL*. In: Proceedings CAV 2015 (2015)

    Google Scholar 

  13. Finkbeiner, B., Seidl, H., Müller, C.: Specifying and verifying secrecy in workflows with arbitrarily many agents. In: Proceedings of the ATVA 2016 (2016)

    Google Scholar 

  14. Mostafa, M., Bonakdarpour, B.: Decentralized runtime verification of LTL specifications in distributed systems. In: IEEE International Parallel and Distributed Processing Symposium (IPDPS), pp. 494–503 (2015)

    Google Scholar 

  15. 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

    Chapter  Google Scholar 

  16. Rabe, M.N.: A Temporal Logic Approach to Information-flow Control. Ph.D. thesis, Saarland University (2016)

    Google Scholar 

  17. Shamir, A.: How to share a secret. Commun. ACM 22(11), 612–613 (1979)

    Article  MathSciNet  MATH  Google Scholar 

  18. Terauchi, T., Aiken, A.: Secure information flow as a safety problem. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 352–367. Springer, Heidelberg (2005). doi:10.1007/11547662_24

    Chapter  Google Scholar 

  19. Zdancewic, S., Myers, A.C.: Observational determinism for concurrent program security. In: Proceedings IEEE Computer Security Foundations Workshop, pp. 29–43, June 2003

    Google Scholar 

Download references

Acknowledgment

This work was partially supported by the German Research Foundation (DFG) in the Collaborative Research Center 1223 and by Canada NSERC Discovery Grant 418396-2012 and NSERC Strategic Grants 430575-2012 and 463324-2014.

Author information

Authors and Affiliations

  1. McMaster University, Hamilton, Canada

    Borzoo Bonakdarpour

  2. Saarland University, Saarbrücken, Germany

    Bernd Finkbeiner

Authors
  1. Borzoo Bonakdarpour
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Bernd Finkbeiner
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Borzoo Bonakdarpour .

Editor information

Editors and Affiliations

  1. Université Grenoble Alpes, Inria, Grenoble, France

    Yliès Falcone

  2. IMDEA Software Institute, Madrid, Spain

    César Sánchez

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this paper

Cite this paper

Bonakdarpour, B., Finkbeiner, B. (2016). Runtime Verification for HyperLTL. In: Falcone, Y., Sánchez, C. (eds) Runtime Verification. RV 2016. Lecture Notes in Computer Science(), vol 10012. Springer, Cham. https://doi.org/10.1007/978-3-319-46982-9_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-46982-9_4

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-46981-2

  • Online ISBN: 978-3-319-46982-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation