Advertisement

Monitoring Hyperproperties by Combining Static Analysis and Runtime Verification

  • Borzoo BonakdarpourEmail author
  • Cesar Sanchez
  • Gerardo Schneider
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, 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.

Notes

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

References

  1. 1.
    Agrawal, S., Bonakdarpour, B.: Runtime verification of \(k\)-safety hyperproperties in HyperLTL. In: CSF 2016, pp. 239–252 (2016)Google Scholar
  2. 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-6Google Scholar
  3. 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. 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_30CrossRefGoogle Scholar
  5. 5.
    Assaf, M., Naumann, D.A.: Calculational design of information flow monitors. In: CSF 2016, pp. 210–224 (2016)Google Scholar
  6. 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. 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_5CrossRefzbMATHGoogle Scholar
  8. 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. 9.
    Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol. 20(4), 14 (2011)CrossRefGoogle Scholar
  10. 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. 11.
    Bonakdarpour, B., Finkbeiner, B.: The complexity of monitoring hyperproperties. In: CSF 2018 (2018, to appear)Google Scholar
  12. 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_5CrossRefGoogle Scholar
  13. 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. 14.
    Chudnov, A., Naumann, D.A.: Information flow monitor inlining. In: Proceedings of CSF, pp. 200–214 (2010)Google Scholar
  15. 15.
    Chugh, R., Meister, J.A., Jhala, R., Lerner, S.: Staged information flow for JavaScript. In: Proceedings of PLDI, pp. 50–62 (2009)CrossRefGoogle Scholar
  16. 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_4CrossRefGoogle Scholar
  17. 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)CrossRefGoogle Scholar
  18. 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_15CrossRefGoogle Scholar
  19. 19.
    Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157–1210 (2010)CrossRefGoogle Scholar
  20. 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. 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. 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. 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_3CrossRefGoogle Scholar
  24. 24.
    Enck, W.: Taintdroid: an information-flow tracking system for realtime privacy monitoring on smartphones. ACM Trans. Comput. Syst. 32, 5 (2014)CrossRefGoogle Scholar
  25. 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 2012Google Scholar
  26. 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_12CrossRefGoogle Scholar
  27. 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_3CrossRefGoogle Scholar
  28. 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. 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_24CrossRefzbMATHGoogle Scholar
  30. 30.
    Magazinius, J., Russo, A., Sabelfeld, A.: On-the-fly inlining of dynamic security monitors. Comput. Secur. 31(7), 827–843 (2012)CrossRefGoogle Scholar
  31. 31.
    Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems. Springer, New York (1995).  https://doi.org/10.1007/978-1-4612-4222-2CrossRefzbMATHGoogle Scholar
  32. 32.
    Myers, A.C.: JFlow: practical mostly-static information flow control. In: POPL 1999, pp. 228–241 (1999)Google Scholar
  33. 33.
    Myers, A.C., Liskov, B.: Complete, safe information flow with decentralized labels (1998)Google Scholar
  34. 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. 35.
    Pinisetty, S., Antignac, T., Sands, D., Schneider, G.: Monitoring data minimisation. Technical report abs/1801.02484, CoRR-arXiv.org (2018)Google Scholar
  36. 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. 37.
    Pnueli, A.: The temporal logic of programs. In: FOCS 1977, pp. 46–67. IEEE Computer Society Press (1977)Google Scholar
  38. 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_38CrossRefGoogle Scholar
  39. 39.
    Pottier, F., Simonet, V.: Information flow inference for ML. In: POPL 2002, pp. 319–330 (2002)CrossRefGoogle Scholar
  40. 40.
    Roşu, G., Havelund, K.: Rewriting-based techniques for runtime verification. Autom. Softw. Eng. 12(2), 151–197 (2005)CrossRefGoogle Scholar
  41. 41.
    Russo, A., Sabelfeld, A.: Dynamic vs. static flow-sensitive security analysis. In: CSF 2010, pp. 186–199 (2010)Google Scholar
  42. 42.
    Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Sel. Areas Commun. 21(1), 5–19 (2003)CrossRefGoogle Scholar
  43. 43.
    Sen, K., Roşu, G.: Generating optimal monitors for extended regular expressions. ENTCS 89(2), 226–245 (2003)Google Scholar
  44. 44.
    Treiber, R.K.: Systems programming: coping with parallelism. Technical report RJ 5118, IBM Almaden Research Center, April 1986Google Scholar
  45. 45.
    Zdancewic, S., Myers, A.C.: Observational determinism for concurrent program security. In: Computer Security Foundations Workshop, pp. 29–43 (2003)Google Scholar
  46. 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_37CrossRefGoogle Scholar
  47. 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 2009Google Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • Borzoo Bonakdarpour
    • 1
    Email author
  • Cesar Sanchez
    • 2
  • Gerardo Schneider
    • 3
  1. 1.Iowa State UniversityAmesUSA
  2. 2.IMDEA Software InstituteMadridSpain
  3. 3.University of GothenburgGothenburgSweden

Personalised recommendations