Abstract
Two new logics for verification of hyperproperties are proposed. Hyperproperties characterize security policies, such as noninterference, as a property of sets of computation paths. Standard temporal logics such as LTL, CTL, and CTL* can refer only to a single path at a time, hence cannot express many hyperproperties of interest. The logics proposed here, HyperLTL and HyperCTL*, add explicit and simultaneous quantification over multiple paths to LTL and to CTL*. This kind of quantification enables expression of hyperproperties. A model checking algorithm for the proposed logics is given. For a fragment of HyperLTL, a prototype model checker has been implemented.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Alur, R., Černý, P., Chaudhuri, S.: Model checking on trees with path equivalences. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 664–678. Springer, Heidelberg (2007)
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)
Andersen, H.R.: A polyadic modal mu-calculus. Technical Report 1994-145, Technical University of Denmark, DTU (1994)
Balliu, M., Dam, M., Guernic, G.L.: Epistemic temporal logic for information flow security. In: Proc. Workshop on Programming Languages and Analysis for Security (June 2011)
Banerjee, A., Naumann, D.A.: Stack-based access control and secure information flow. Journal of Functional Programming 15(2), 131–177 (2005)
Barthe, G., Crespo, J.M., Kunz, C.: Beyond 2-safety: Asymmetric product programs for relational program verification. In: Artemov, S., Nerode, A. (eds.) LFCS 2013. LNCS, vol. 7734, pp. 29–43. Springer, Heidelberg (2013)
Barthe, G., D’Argenio, P.R., Rezk, T.: Secure information flow by self-composition. In: Proc. IEEE Computer Security Foundations Workshop, pp. 100–114 (June 2004)
Bradfield, J., Stirling, C.: Modal mu-calculi. In: Handbook of Modal Logic, pp. 721–756. Elsevier, Amsterdam (2007)
Bryans, J.W., Koutny, M., Mazaré, L., Ryan, P.Y.A.: Opacity generalised to transition systems. In: Dimitrakos, T., Martinelli, F., Ryan, P.Y.A., Schneider, S. (eds.) FAST 2005. LNCS, vol. 3866, pp. 81–95. Springer, Heidelberg (2006)
Chadha, R., Delaune, S., Kremer, S.: Epistemic logic for the applied pi calculus. In: Lee, D., Lopes, A., Poetzsch-Heffter, A. (eds.) FMOODS 2009. LNCS, vol. 5522, pp. 182–197. Springer, Heidelberg (2009)
Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NuSMV: A new symbolic model verifier. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 495–499. Springer, Heidelberg (1999)
Clark, D., Hunt, S., Malacaria, P.: Quantified interference for a while language. Electronic Notes in Theoretical Computer Science 112, 149–166 (2005)
Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., Sánchez, C.: Temporal logics for hyperproperties (January 2014), http://arxiv.org/abs/1401.4492
Clarkson, M.R., Myers, A.C., Schneider, F.B.: Quantifying information flow with beliefs. Journal of Computer Security 17(5), 655–701 (2009)
Clarkson, M.R., Schneider, F.B.: Hyperproperties. Journal of Computer Security 18(6), 1157–1210 (2010)
Cook, B., Koskinen, E., Vardi, M.: Temporal property verification as a program analysis task. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 333–348. Springer, Heidelberg (2011)
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)
Emerson, E.A., Halpern, J.Y.: “Sometimes” and “not never” revisited: On branching versus linear time temporal logic. Journal of the ACM 33(1), 151–178 (1986)
Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning About Knowledge. MIT Press, Cambridge (1995)
Focardi, R., Gorrieri, R.: Classification of security properties (Part I: Information flow. In: Focardi, R., Gorrieri, R. (eds.) FOSAD 2000. LNCS, vol. 2171, pp. 331–396. Springer, Heidelberg (2001)
Gastin, P., Oddoux, D.: Fast LTL to Büchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 53–65. Springer, Heidelberg (2001)
Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Proc. Protocol Specification, Testing and Verification, pp. 3–18 (June 1995)
Goguen, J.A., Meseguer, J.: Security policies and security models. In: Proc. IEEE Symposium on Security and Privacy, pp. 11–20 (April 1982)
Gray III, J.W.: Toward a mathematical foundation for information flow security. In: Proc. IEEE Symposium on Security and Privacy, pp. 210–234 (May 1991)
Gray III, J.W., Syverson, P.F.: A logical approach to multilevel security of probabilistic systems. Distributed Computing 11(2), 73–90 (1998)
Halpern, J.Y., O’Neill, K.R.: Secrecy in multiagent systems. ACM Transactions on Information and System Security 12(1), 5:1–5:47 (2008)
Hammer, C., Snelting, G.: Flow-sensitive, context-sensitive, and object-sensitive information flow control based on program dependence graphs. International Journal of Information Security 8(6), 399–422 (2009)
Holzmann, G.J.: The model checker SPIN. IEEE Transactions on Software Engineering 23, 279–295 (1997)
Huisman, M., Blondeel, H.-C.: Model-checking secure information flow for multi-threaded programs. In: Mödersheim, S., Palamidessi, C. (eds.) TOSCA 2011. LNCS, vol. 6993, pp. 148–165. Springer, Heidelberg (2012)
Huisman, M., Worah, P., Sunesen, K.: A temporal logic characterisation of observational determinism. In: Proc. IEEE Computer Security Foundations Workshop, pp. 3–15 (July 2006)
Köpf, B., Basin, D.: An information-theoretic model for adaptive side-channel attacks. In: Proc. ACM Conference on Computer and Communications Security, pp. 286–296 (October 2007)
Lamport, L.: Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering 3(2), 125–143 (1977)
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, New York (1992)
Mantel, H.: Possibilistic definitions of security—an assembly kit. In: Proc. IEEE Computer Security Foundations Workshop, pp. 185–199 (July 2000)
McCullough, D.: Noninterference and the composability of security properties. In: Proc. IEEE Symposium on Security and Privacy, pp. 177–186 (April 1988)
McCullough, D.: A hookup theorem for multilevel security. Proc. IEEE Transactions on Software Engineering 16(6), 563–568 (1990)
McLean, J.: Proving noninterference and functional correctness using traces. Journal of Computer Security 1(1), 37–58 (1992)
McLean, J.: A general theory of composition for trace sets closed under selective interleaving functions. In: Proc. IEEE Symposium on Security and Privacy, pp. 79–93 (April 1994)
Millen, J.K.: Unwinding forward correctability. In: Proc. IEEE Computer Security Foundations Workshop, pp. 2–10 (June 1994)
Milushev, D., Clarke, D.: Towards incrementalization of holistic hyperproperties. In: Degano, P., Guttman, J.D. (eds.) POST 2012. LNCS, vol. 7215, pp. 329–348. Springer, Heidelberg (2012)
Milushev, D., Clarke, D.: Incremental hyperproperty model checking via games. In: Riis Nielson, H., Gollmann, D. (eds.) NordSec 2013. LNCS, vol. 8208, pp. 247–262. Springer, Heidelberg (2013)
Milushev, D.V.: Reasoning about Hyperproperties. PhD thesis, Katholieke Universiteit Leuven (June 2013)
Myers, A.C.: JFlow: Practical mostly-static information flow control. In: Proc. ACM Symposium on Principles of Programming Languages, pp. 228–241 (1999)
Pnueli, A.: The temporal logic of programs. In: Proc. Foundations of Computer Science, pp. 46–57 (September 1977)
Rogers, H.: Theory of Recursive Functions and Effective Computability. MIT Press, Cambridge (1987)
Roscoe, A.W.: CSP and determinism in security modelling. In: Proc. IEEE Symposium on Security and Privacy, pp. 114–127 (May 1995)
Ryan, P.Y.A., Peacock, T.: Opacity—further insights on an information flow property. Technical Report CS-TR-958, Newcastle University (April 2006)
Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE Journal on Selected Areas in Communications 21(1), 5–19 (2003)
Sabelfeld, A., Sands, D.: Dimensions and principles of declassification. In: Proc. IEEE Computer Security Foundations Workshop, pp. 255–269 (2005)
Sistla, A.P., Vardi, M.Y., Wolper, P.: The complementation problem for Büchi automata with appplications to temporal logic. Theoretical Computer Science 49, 217–237 (1987)
Smith, G.: On the foundations of quantitative information flow. In: de Alfaro, L. (ed.) FOSSACS 2009. LNCS, vol. 5504, pp. 288–302. Springer, Heidelberg (2009)
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)
Tsay, Y.-K., Chen, Y.-F., Tsai, M.-H., Wu, K.-N., Chan, W.-C.: GOAL: A graphical tool for manipulating Büchi automata and temporal formulae. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 466–471. Springer, Heidelberg (2007)
van der Meyden, R.: Axioms for knowledge and time in distributed systems with perfect recall. In: Proc. IEEE Symposium on Logic in Computer Science, pp. 448–457 (1993)
van der Meyden, R., Wilke, T.: Preservation of epistemic properties in security protocol implementations. In: Proc. ACM Conference on Theoretical Aspects of Rationality and Knowledge, pp. 212–221 (2007)
van der Meyden, R., Zhang, C.: Algorithmic verification of noninterference properties. Electronic Notes in Theoretical Computer Science 168, 61–75 (2007)
Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency. LNCS, vol. 1043, pp. 238–266. Springer, Heidelberg (1996)
Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Information and Computation 115(1), 1–37 (1994)
Wolper, P.: Constructing automata from temporal logic formulas: A tutorial. In: Brinksma, E., Hermanns, H., Katoen, J.-P. (eds.) FMPA 2000. LNCS, vol. 2090, pp. 261–277. Springer, Heidelberg (2001)
Yasuoka, H., Terauchi, T.: On bounding problems of quantitative information flow. In: Gritzalis, D., Preneel, B., Theoharidou, M. (eds.) ESORICS 2010. LNCS, vol. 6345, pp. 357–372. Springer, Heidelberg (2010)
Zdancewic, S., Myers, A.C.: Observational determinism for concurrent program security. In: Proc. IEEE Computer Security Foundations Workshop, pp. 29–43 (June 2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., Sánchez, C. (2014). Temporal Logics for Hyperproperties. In: Abadi, M., Kremer, S. (eds) Principles of Security and Trust. POST 2014. Lecture Notes in Computer Science, vol 8414. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-54792-8_15
Download citation
DOI: https://doi.org/10.1007/978-3-642-54792-8_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-54791-1
Online ISBN: 978-3-642-54792-8
eBook Packages: Computer ScienceComputer Science (R0)