Abstract
The paper considers the complexity of verifying that a finite state system satisfies a number of definitions of information flow security. The systems model considered is one in which agents operate synchronously with awareness of the global clock. This enables timing based attacks to be captured, whereas previous work on this topic has dealt primarily with asynchronous systems. Versions of the notions of nondeducibility on inputs, nondeducibility on strategies, and an unwinding based notion are formulated for this model. All three notions are shown to be decidable, and their computational complexity is characterised.
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
Agat, J.: Transforming out timing leaks. In: Proc. ACM Symp. on Principles of Programming Languages, pp. 40–53 (2000)
Bossi, A., Focardi, R., Piazza, C., Rossi, S.: Bisimulation and unwinding for verifying possibilistic security properties. In: Proc. Int. Conf. on Verication, Model Checking, and Abstract Interpretation, pp. 223–237 (2003)
Beauquier, D., Lanotte, R.: Hiding information in multi level security systems. In: Dimitrakos, T., Martinelli, F., Ryan, P.Y.A., Schneider, S. (eds.) FAST 2006. LNCS, vol. 4691, pp. 250–269. Springer, Heidelberg (2007)
D’Souza, D., Holla, R., Kulkarni, J., Ramesh, R.K., Sprick, B.: On the decidability of model-checking information flow properties. In: Proc. Int. Conf. on Information Systems Security, pp. 26–40 (2008)
Focardi, R., Gorrieri, R.: A classification of security properties for process algebras. Journal of Computer Security, 5–33 (1995)
Focardi, R., Gorrieri, R.: The compositional security checker: A tool for the verification of information flow security properties. Technical Report UBLCS-96-14, Università di Bologna (August 1996)
Focardi, R., Gorrieri, R., Martinelli, F.: Information flow analysis in a discrete-time process algebra. In: Proc. Computer Security Foundation Workshop, pp. 170–184 (2000)
Goguen, J.A., Meseguer, J.: Unwinding and inference control. In: Proc. IEEE Symp. on Security and Privacy, p. 75 (1984)
Köpf, B., Basin, D.A.: Timing-sensitive information flow analysis for synchronous systems. In: Gollmann, D., Meier, J., Sabelfeld, A. (eds.) ESORICS 2006. LNCS, vol. 4189, pp. 243–262. Springer, Heidelberg (2006)
Kocher, P.C.: Timing attacks on implementations of Diffie-Hellman, RSA, DSS, and other systems. In: Koblitz, N. (ed.) CRYPTO 1996. LNCS, vol. 1109, pp. 104–113. Springer, Heidelberg (1996)
Kanellakis, P.C., Smolka, S.A.: CCS expressions, finite state processes, and three problems of equivalence. In: Proc. 2nd Annual ACM Symp. on Principles of Distributed Computing, New York, NY, pp. 228–240 (1983)
Mantel, H.: Possiblistic definitions of security – an assembly kit. In: Proc. Computer Security Foundations Workshop, pp. 185–199 (2000)
Mantel, H.: Unwinding security properties. In: Cuppens, F., Deswarte, Y., Gollmann, D., Waidner, M. (eds.) ESORICS 2000. LNCS, vol. 1895, pp. 238–254. Springer, Heidelberg (2000)
McCullough, D.: Noninterference and the composability of security properties. In: Proc. IEEE Symp. on Security and Privacy, pp. 177–186 (1988)
Reif, J.H.: The complexity of two-player games of incomplete information. Journal of Computer and System Science 29(2), 274–301 (1984)
Rushby, J.: Noninterference, transitivity, and channel-control security policies. Technical report, SRI international (December 1992)
Stockmeyer, L.J., Chandra, A.K.: Provably difficult combinatorial games. SIAM Journal of Computing 8(2), 151–174 (1979)
Stockmeyer, L.J., Meyer, A.R.: Word problems requiring exponential time (preliminary report). In: Proc. ACM Symp. on Theory of computing, pp. 1–9 (1973)
van der Meyden, R., Zhang, C.: A comparison of semantic models for noninterference. In: Dimitrakos, T., Martinelli, F., Ryan, P.Y.A., Schneider, S. (eds.) FAST 2006. LNCS, vol. 4691, pp. 235–249. Springer, Heidelberg (2007)
van der Meyden, R., Zhang, C.: Algorithmic verification on noninterference properties. ENTCS 168, 61–75 (2007)
van der Meyden, R., Zhang, C.: Information flow in systems with schedulers. In: Proc. Computer Security Foundation Symp., June 2008, pp. 301–312 (2008)
Volpano, D.M., Smith, G.: A type-based approach to program security. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997, FASE 1997, and TAPSOFT 1997. LNCS, vol. 1214, pp. 607–621. Springer, Heidelberg (1997)
Wittbold, J.T., Johnson, D.M.: Information flow in nondeterministic systems. In: Proc. IEEE Symp. on Security and Privacy, pp. 144–161 (1990)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cassez, F., van der Meyden, R., Zhang, C. (2010). The Complexity of Synchronous Notions of Information Flow Security. In: Ong, L. (eds) Foundations of Software Science and Computational Structures. FoSSaCS 2010. Lecture Notes in Computer Science, vol 6014. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-12032-9_20
Download citation
DOI: https://doi.org/10.1007/978-3-642-12032-9_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-12031-2
Online ISBN: 978-3-642-12032-9
eBook Packages: Computer ScienceComputer Science (R0)