Abstract
Hyperproperties were proposed as an abstract formalization of security policies, but unfortunately they lack a generic verification methodology. In an attempt to remedy this, we introduced the notion of incremental hyperproperties (IHPs), motivated by the observation that they have a clearer and more feasible verification methodology. To show that verification is indeed feasible, a decidable IHP verification methodology via games is presented and evaluated. The main advantage of the approach is that the games in combination with winning strategy evidence give valuable intuition about the security of a system and are very helpful when analyzing systems w.r.t. policy specifications.
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
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Andersen, H.R.: A Polyadic Modal μ-Calculus. Technical Report 1994-145, Technical University of Denmark, DTU (1994)
Bradfield, J., Stirling, C.: Modal mu-calculi. In: Handbook of Modal Logic, pp. 721–756. Elsevier (2007)
Clarkson, M.R., Schneider, F.B.: Hyperproperties. Journal of Computer Security 18, 1157–1210 (2010)
Friedmann, O.: An exponential lower bound for the latest deterministic strategy iteration algorithms. Logical Methods in Computer Science 7(3) (2011)
Friedmann, O., Lange, M.: Solving parity games in practice. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 182–196. Springer, Heidelberg (2009)
Friedmann, O., Lange, M.: A Solver for Modal Fixpoint Logics. Electron. Notes Theor. Comput. Sci. 262, 99–111 (2010)
Groote, J.F., Mathijssen, A., Reniers, M., Usenko, Y., van Weerdenburg, M.: The Formal Specification Language mCRL2. In: Brinksma, E., Harel, D., Mader, A., Stevens, P., Wieringa, R. (eds.) Methods for Modelling Software Systems (MMOSS). Dagstuhl Seminar Proceedings, vol. 06351, Dagstuhl, Germany (2007)
Jurdziński, M., Paterson, M., Zwick, U.: A deterministic subexponential algorithm for solving parity games. In: Proceedings of ACM-SIAM Symposium on Discrete Algorithms, SODA 2006, pp. 117–123. ACM/SIAM (2006)
Kalai, G.: Linear programming, the simplex algorithm and simple polytopes. Mathematical Programming 79, 217–233 (1997)
Mantel, H.: A Uniform Framework for the Formal Specification and Verification of Information Flow Security. PhD thesis, Universität des Saarlandes, Saarbrücken, Germany (July 2003)
Matoušek, J., Sharir, M., Welzl, E.: A subexponential bound for linear programming. In: Proceedings of the Eighth Annual Symposium on Computational Geometry, SCG 1992, pp. 1–8. ACM, New York (1992)
McCullough, D.: Specifications for multi-level security and a hook-up. In: Proceedings of the 1987 IEEE Symposium on Security and Privacy, pp. 161–166. IEEE Computer Society, Los Alamitos (1987)
Milushev, D.: Reasoning about Hyperproperties. PhD thesis, KU Leuven, Heverlee, Belgium (June 2013)
Milushev, D., Clarke, D.: Coinductive unwinding of security-relevant hyperproperties. In: Jøsang, A., Carlsson, B. (eds.) NordSec 2012. LNCS, vol. 7617, pp. 121–136. Springer, Heidelberg (2012)
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)
Rutten, J.J.M.M.: Automata and Coinduction (An Exercise in Coalgebra). In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 194–218. Springer, Heidelberg (1998)
Schewe, S.: An optimal strategy improvement algorithm for solving parity and payoff games. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol. 5213, pp. 369–384. Springer, Heidelberg (2008)
Stirling, C.: Modal and temporal properties of processes. Springer, New York (2001)
Stevens, P., Stirling, C.: Practical model-checking using games. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 85–101. Springer, Heidelberg (1998)
Vöge, J., Jurdziński, M.: A Discrete Strategy Improvement Algorithm for Solving Parity Games. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 202–215. Springer, Heidelberg (2000)
Zakinthinos, A., Lee, E.S.: A general theory of security properties. In: Proceedings of the IEEE Symposium on Security and Privacy, SP 1997, pp. 94–102. IEEE Computer Society, Washington, DC (1997)
Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theoretical Computer Science 200(1-2), 135–183 (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Milushev, D., Clarke, D. (2013). Incremental Hyperproperty Model Checking via Games. In: Riis Nielson, H., Gollmann, D. (eds) Secure IT Systems. NordSec 2013. Lecture Notes in Computer Science, vol 8208. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-41488-6_17
Download citation
DOI: https://doi.org/10.1007/978-3-642-41488-6_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-41487-9
Online ISBN: 978-3-642-41488-6
eBook Packages: Computer ScienceComputer Science (R0)