Abstract
Hyperproperties generalize trace properties by expressing relations between multiple computations. Hyperpropertes include policies from information-flow security, like observational determinism or noninterference, and many other system properties including promptness and knowledge. In this paper, we give an overview on the model checking problem for temporal hyperlogics. Our starting point is the model checking algorithm for HyperLTL, a reduction to Büchi automata emptiness. This basic construction can be extended with propositional quantification, resulting in an algorithm for HyperQPTL. It can also be extended with branching time, resulting in an algorithm for HyperCTL\(^*\). However, it is not possible to have both extensions at the same time: the model checking problem of HyperQCTL\(^*\) is undecidable. An attractive compromise is offered by MPL[E], i.e., monadic path logic extended with the equal-level predicate. The expressiveness of MPL[E] falls strictly between that of HyperCTL\(^*\) and HyperQCTL\(^*\). MPL[E] subsumes both HyperCTL\(^*\) and HyperKCTL\(^*\), the extension of HyperCTL\(^*\) with the knowledge operator. We show that the model checking problem for MPL[E] is still decidable.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Barthe, G., D’Argenio, P.R., Rezk, T.: Secure information flow by self-composition. Math. Struct. Comput. Sci. 21(6), 1207–1252 (2011)
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
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
Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157–1210 (2010)
Coenen, N., Finkbeiner, B., Hahn, C., Hofmann, J.: The hierarchy of hyperlogics. In: 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24–27, 2019, pp. 1–13. IEEE (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
Dimitrova, R., Finkbeiner, B., Torfah, H.: Probabilistic hyperproperties of Markov decision processes. In: Hung, D.V., Sokolsky, O. (eds.) ATVA 2020. LNCS, vol. 12302, pp. 484–500. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-59152-6_27
Finkbeiner, B.: Temporal hyperproperties. Bulletin of the EATCS, 123 (2017)
Finkbeiner, B., Hahn, C., Hofmann, J., Tentrup, L.: Realizing \(\omega \)-regular hyperproperties. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 40–63. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-53291-8_4
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
Finkbeiner, B., Zimmermann, M.: The first-order logic of hyperproperties. In: 34th Symposium on Theoretical Aspects of Computer Science, STACS 2017, Hannover, Germany, March 8–11, 2017, pp. 30:1–30:14 (2017)
Goguen, J.A., Meseguer, J.: Security policies and security models. In: IEEE Symposium on Security and Privacy, pp. 11–20, April 1982
Huisman, M., Worah, P., Sunesen, K.: A temporal logic characterisation of observational determinism. In: Proceedings of the IEEE Computer Security Foundations Workshop, pp. 3–15, July 2006
Kupferman, O., Piterman, N., Vardi, M.Y.: From liveness to promptness. Formal Methods Syst. Des. 34(2), 83–103 (2009)
McCullough, D.: Noninterference and the composability of security properties. In: Proceedings of the IEEE Symposium on Security and Privacy, pp. 177–186, April 1988
Pnueli, A.: The temporal logic of programs. FOCS 1977, 46–57 (1977)
Rabe, M.N.: A temporal logic approach to information-flow control. Ph.D. thesis, Saarland University (2016)
van der Meyden, R., Zhang, C.: Algorithmic verification of noninterference properties. Electr. Notes Theor. Comput. Sci. (ENTCS) 168, 61–75 (2007)
Acknowledgement
Most of the work reported in this paper has previously appeared in various publications [3, 5, 6, 9,10,11]. I am indebted to my coauthors Michael R. Clarkson, Norine Coenen, Christopher Hahn, Jana Hofmann, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, César Sánchez, Leander Tentrup, and Martin Zimmermann. This work was partially supported by the Collaborative Research Center “Foundations of Perspicuous Software Systems"(TRR: 248, 389792660) and the European Research Council (ERC) Grant OSARES (No. 683300).
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2021 Springer Nature Switzerland AG
About this paper
Cite this paper
Finkbeiner, B. (2021). Model Checking Algorithms for Hyperproperties (Invited Paper). In: Henglein, F., Shoham, S., Vizel, Y. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2021. Lecture Notes in Computer Science(), vol 12597. Springer, Cham. https://doi.org/10.1007/978-3-030-67067-2_1
Download citation
DOI: https://doi.org/10.1007/978-3-030-67067-2_1
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-67066-5
Online ISBN: 978-3-030-67067-2
eBook Packages: Computer ScienceComputer Science (R0)