Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Leveraging Applications of Formal Methods

ISoLA 2018: Leveraging Applications of Formal Methods, Verification and Validation. Verification pp 8–27Cite as

Monitoring Hyperproperties by Combining Static Analysis and Runtime Verification

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11245))

Abstract

Hyperproperties are properties whose reasoning involve sets of traces. Examples of hyperproperties include information-flow security properties, properties of coding/decoding systems, linearizability and other consistency criteria, as well as privacy properties like data minimality. We study the problem of runtime verification of hyperproperties expressed as HyperLTL formulas that involve quantifier alternation. We first show that even for a simple class of temporal formulas, virtually no \(\forall \exists \) property can be monitored, independently of the observations performed. To manage this problem, we propose to use a combination of static analysis with runtime verification. By using static analysis/verification, one typically obtains a model of the system that allows to limit the source of “hypothetical” traces to a sound over-approximation of the traces of the system. This idea allows to extend the effective monitorability of hyperproperties to a larger class of systems and properties. We exhibit some examples where instances of this idea have been exploited, and discuss preliminary work towards a general method. A second contribution of this paper is the idea of departing from the convention that all traces come from executions of a single system. We show cases where traces are extracted from the observed traces of agents, from projections of a single global trace, or from executions of different (but related) programs.

This is a preview of subscription content, 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

Learn about institutional subscriptions

Notes

  1. 1.

    The definition of offline monitoring also includes when traces are obtained from other sources than the program running in its real environment (e.g., in a simulation environment, or traces not coming from the real program but from a model, for instance).

  2. 2.

    The General Data Protection Regulation (EU—2016/679) was adopted on 27 April 2016, and it will enter into application 25 May 2018.

  3. 3.

    A stronger version of distributed minimality, which is a \(\forall \forall \) hyperproperty, is given in [36].

  4. 4.

    Note that the pair ((0, 1), (1, 1)) would not satisfy the definition, but this is fine as the definition only requires that at least one such tuple exists.

  5. 5.

    We speculate that the abstract model \(\widehat{P}\) may be computed using different techniques, e.g., predicate abstraction, symbolic execution, etc.

References

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

    Google Scholar 

  2. Ahrendt, W., Beckert, B., Bubel, R., Hähnle, R., Schmitt, P.H., Ulbrich, M. (eds.) Deductive Software Verification - The KeY Book. From Theory to Practice. LNCS, vol. 10001. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-49812-6

  3. Antignac, T., Sands, D., Schneider, G.: Data minimisation: a language-based approach (long version). Technical report abs/1611.05642, CoRR-arXiv.org (2016)

    Google Scholar 

  4. Antignac, T., Sands, D., Schneider, G.: Data minimisation: a language-based approach. In: De Capitani di Vimercati, S., Martinelli, F. (eds.) SEC 2017. IAICT, vol. 502, pp. 442–456. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-58469-0_30

    Chapter  Google Scholar 

  5. Assaf, M., Naumann, D.A.: Calculational design of information flow monitors. In: CSF 2016, pp. 210–224 (2016)

    Google Scholar 

  6. Austin, T.H., Flanagan, C.: Efficient purely-dynamic information flow analysis. In: ACM Transaction on Programming Languages and Systems, pp. 113–124 (2009)

    Google Scholar 

  7. Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Rule-based runtime verification. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 44–57. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24622-0_5

    Chapter  MATH  Google Scholar 

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

    Google Scholar 

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

    Article  Google Scholar 

  10. Beckert, B., Klebanov, V., Ulbrich, M.: Regression verification for Java using a secure information flow calculus. In: Proceedings of the 17th Workshop on Formal Techniques for Java-Like Programs (FTfJP 2015), pp. 6:1–6:6. ACM (2015)

    Google Scholar 

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

    Google Scholar 

  12. 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). https://doi.org/10.1007/978-3-662-54580-5_5

    Chapter  Google Scholar 

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

    Google Scholar 

  14. Chudnov, A., Naumann, D.A.: Information flow monitor inlining. In: Proceedings of CSF, pp. 200–214 (2010)

    Google Scholar 

  15. Chugh, R., Meister, J.A., Jhala, R., Lerner, S.: Staged information flow for JavaScript. In: Proceedings of PLDI, pp. 50–62 (2009)

    Google Scholar 

  16. Clark, D., Hunt, S.: Non-interference for deterministic interactive programs. In: Degano, P., Guttman, J., Martinelli, F. (eds.) FAST 2008. LNCS, vol. 5491, pp. 50–66. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-01465-9_4

    Chapter  Google Scholar 

  17. Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Form. Methods Syst. Des. 19(1), 7–34 (2001)

    Article  Google Scholar 

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

    Chapter  Google Scholar 

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

    Article  Google Scholar 

  20. Colombo, C., Pace, G.J., Schneider, G.: LARVA – safer monitoring of real-time Java programs (Tool Paper). In: SEFM 2009, pp. 33–37. IEEE Computer Society (2009)

    Google Scholar 

  21. D’Angelo, B., et al.: LOLA: runtime monitoring of synchronous systems. In: TIME 2005, pp. 166–174. IEEE CS Press (2005)

    Google Scholar 

  22. Devriese, D., Piessens, F.: Noninterference through secure multi-execution. In: 31st IEEE Symposium on Security and Privacy, S&P, pp. 109–124 (2010)

    Google Scholar 

  23. Eisner, C., Fisman, D., Havlicek, J., Lustig, Y., McIsaac, A., Van Campenhout, D.: Reasoning with temporal logic on truncated paths. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 27–39. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45069-6_3

    Chapter  Google Scholar 

  24. Enck, W.: Taintdroid: an information-flow tracking system for realtime privacy monitoring on smartphones. ACM Trans. Comput. Syst. 32, 5 (2014)

    Article  Google Scholar 

  25. European Commission: Proposal for a Regulation of the European Parliament and of the Council on the protection of individuals with regard to the processing of personal data and on the free movement of such data (GDPR). Technical report 2012/0011 (COD). European Commission, January 2012

    Google Scholar 

  26. Finkbeiner, B., Hahn, C., Stenger, M., Tentrup, L.: Monitoring hyperproperties. In: Lahiri, S., Reger, G. (eds.) RV 2017. LNCS, vol. 10548, pp. 190–207. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-67531-2_12

    Chapter  Google Scholar 

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

    Chapter  Google Scholar 

  28. Goguen, J.A., Meseguer, J.: Security policies and security models. In: Proceedings of IEEE Symposium on Security and Privacy, pp. 11–20 (1982)

    Google Scholar 

  29. Havelund, K., Roşu, G.: Synthesizing monitors for safety properties. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 342–356. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-46002-0_24

    Chapter  MATH  Google Scholar 

  30. Magazinius, J., Russo, A., Sabelfeld, A.: On-the-fly inlining of dynamic security monitors. Comput. Secur. 31(7), 827–843 (2012)

    Article  Google Scholar 

  31. Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems. Springer, New York (1995). https://doi.org/10.1007/978-1-4612-4222-2

    Book  MATH  Google Scholar 

  32. Myers, A.C.: JFlow: practical mostly-static information flow control. In: POPL 1999, pp. 228–241 (1999)

    Google Scholar 

  33. Myers, A.C., Liskov, B.: Complete, safe information flow with decentralized labels (1998)

    Google Scholar 

  34. Nair, S., Simpson, P.N.D., Crispo, B., Tanenbaum, A.S.: A virtual machine based information flow control system for policy enforcement. ENTCS 197(1), 3–16 (2008)

    Google Scholar 

  35. Pinisetty, S., Antignac, T., Sands, D., Schneider, G.: Monitoring data minimisation. Technical report abs/1801.02484, CoRR-arXiv.org (2018)

    Google Scholar 

  36. Pinisetty, S., Sands, D., Schneider, G.: Runtime verification of hyperproperties for deterministic programs. In: FormaliSE@ICSE 2018, pp. 20–29. ACM (2018)

    Google Scholar 

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

    Google Scholar 

  38. 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). https://doi.org/10.1007/11813040_38

    Chapter  Google Scholar 

  39. Pottier, F., Simonet, V.: Information flow inference for ML. In: POPL 2002, pp. 319–330 (2002)

    Google Scholar 

  40. Roşu, G., Havelund, K.: Rewriting-based techniques for runtime verification. Autom. Softw. Eng. 12(2), 151–197 (2005)

    Article  Google Scholar 

  41. Russo, A., Sabelfeld, A.: Dynamic vs. static flow-sensitive security analysis. In: CSF 2010, pp. 186–199 (2010)

    Google Scholar 

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

    Article  Google Scholar 

  43. Sen, K., Roşu, G.: Generating optimal monitors for extended regular expressions. ENTCS 89(2), 226–245 (2003)

    Google Scholar 

  44. Treiber, R.K.: Systems programming: coping with parallelism. Technical report RJ 5118, IBM Almaden Research Center, April 1986

    Google Scholar 

  45. Zdancewic, S., Myers, A.C.: Observational determinism for concurrent program security. In: Computer Security Foundations Workshop, pp. 29–43 (2003)

    Google Scholar 

  46. Zhang, X., Leucker, M., Dong, W.: Runtime verification with predictive semantics. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 418–432. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-28891-3_37

    Chapter  Google Scholar 

  47. Zhu, Y., Jung, J., Song, D., Kohno, T., Wetherall, D.: Privacy scope: a precise information flow tracking system for finding application leaks. Technical report, EECS Department, University of California, Berkeley, October 2009

    Google Scholar 

Download references

Acknowledgment

We would like to thank Sandro Stucki for his useful comments on early drafts of the paper, and in particular in formulation of the data minimisation property. This research has been partially supported by: the NSF SaTC-1813388, a grant from Iowa State University, EU H2020 project Elastest (nr. 731535), the Spanish MINECO Project “RISCO (TIN2015-71819-P)”, the Swedish Research Council (Vetenskapsrådet) under grant Nr. 2015-04154 (PolUser: Rich User-Controlled Privacy Policies), and by the EU ICT COST Action IC1402 ARVI (Runtime Verification beyond Monitoring).

Author information

Authors and Affiliations

  1. Iowa State University, Ames, USA

    Borzoo Bonakdarpour

  2. IMDEA Software Institute, Madrid, Spain

    Cesar Sanchez

  3. University of Gothenburg, Gothenburg, Sweden

    Gerardo Schneider

Authors
  1. Borzoo Bonakdarpour
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Cesar Sanchez
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Gerardo Schneider
    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. University of Limerick, Limerick, Ireland

    Tiziana Margaria

  2. TU Dortmund, Dortmund, Germany

    Bernhard Steffen

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Bonakdarpour, B., Sanchez, C., Schneider, G. (2018). Monitoring Hyperproperties by Combining Static Analysis and Runtime Verification. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation. Verification. ISoLA 2018. Lecture Notes in Computer Science(), vol 11245. Springer, Cham. https://doi.org/10.1007/978-3-030-03421-4_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-03421-4_2

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-03420-7

  • Online ISBN: 978-3-030-03421-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation