Hostname: page-component-78c5997874-mlc7c Total loading time: 0 Render date: 2024-11-05T13:20:18.124Z Has data issue: false hasContentIssue false
  • English
  • Français

Non-termination and secure information flow†

Published online by Cambridge University Press:  27 October 2011

GEOFFREY SMITH  and
RAFAEL ALPÍZAR
GEOFFREY SMITH
Affiliation:
School of Computing and Information Sciences, Florida International University, Miami, FL 33199U.S.A. Email: [email protected]; [email protected]
RAFAEL ALPÍZAR
Affiliation:
School of Computing and Information Sciences, Florida International University, Miami, FL 33199U.S.A. Email: [email protected]; [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

In secure information flow analysis, the classic Denning restrictions allow a program's termination to be affected by the values of its H variables, resulting in potential information leaks. In an effort to quantify such leaks, in this paper we study a simple imperative language with random assignments. As a thought experiment, we propose a ‘stripping’ operation on programs, which eliminates all ‘high computation’, and prove the fundamental property that stripping cannot decrease the probability of any low outcome. To prove this property, we first introduce a new notion of fast probabilistic simulation on Markov chains and show that it implies a key reachability property. Viewing the stripping function as a binary relation, we then prove that stripping is a fast simulation. As an application, we prove that, under the Denning restrictions, well-typed probabilistic programs are guaranteed to satisfy an approximate probabilistic non-interference property, provided that their probability of non-termination is small.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 21 , Special Issue 6: Programming Language Interference and Dependence , December 2011 , pp. 1183 - 1205
Copyright
Copyright © Cambridge University Press 2011

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Abadi, M., Corin, R. and Fournet, C. (2006) Computational secrecy by typing for the pi calculus. In: Kobayashi, N. (ed.) Fourth Asian Symposium on Programming Languages and Systems (APLAS 2006). Springer-Verlag Lecture Notes in Computer Science 4279 253–269.CrossRefGoogle Scholar
Abadi, M., Fournet, C. and Gonthier, G. (1998) Secure implementation of channel abstractions. In: LICS '98: Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society 105.Google Scholar
Agat, J. (2000) Transforming out timing leaks. In: Proceedings 27th ACM Symposium on Principles of Programming Languages POPL, ACM 40–53.Google Scholar
Alpízar, R. and Smith, G. (2009) Secure information flow for distributed systems. In: Proceedings Formal Aspects of Security and Trust (FAST 2009), Eindhoven, Netherlands.Google Scholar
Askarov, A., Hunt, S., Sabelfeld, A. and Sands, D. (2008) Termination-insensitive noninterference leaks more than just a bit. In: Proceedings 13th European Symposium on Research in Computer Security (ESORICS'08). Springer-Verlag Lecture Notes in Computer Science 5283 333–348.CrossRefGoogle Scholar
Baier, C., Katoen, J.-P., Hermanns, H. and Wolf, V. (2005) Comparative branching-time semantics for Markov chains. Information and Computation 200 (2)149–214.CrossRefGoogle Scholar
Bellare, M. and Rogaway, P. (2005) Introduction to modern cryptography. Available at http://www-cse.ucsd.edu/users/mihir/cse207/classnotes.html.Google Scholar
Denning, D. and Denning, P. (1977) Certification of programs for secure information flow. Communications of the ACM 20 (7)504–513.CrossRefGoogle Scholar
Di Pierro, A., Hankin, C. and Wiklicky, H. (2002) Approximate non-interference. In: Proceedings 15th IEEE Computer Security Foundations Workshop, IEEE Computer Society 1–17.Google Scholar
Feller, W. (1968) An Introduction to Probability Theory and Its Applications, Volume I (third edition), John Wiley and Sons.Google Scholar
Focardi, R. and Centenaro, M. (2008) Information flow security of multi-threaded distributed programs. In: PLAS '08: Proceedings of the Third ACM SIGPLAN Workshop on Programming Languages and Analysis for Security, ACM 113–124.CrossRefGoogle Scholar
Fournet, C. and Rezk, T. (2008) Cryptographically sound implementations for typed information-flow security. In: Proceedings 35th Symposium on Principles of Programming Languages, ACM.Google Scholar
Gray, J. W. III (1990) Probabilistic interference. In Proceedings 1990 IEEE Symposium on Security and Privacy, IEEE Computer Society 170–179.CrossRefGoogle Scholar
Jonsson, B. and Larsen, K. (1991) Specification and refinement of probabilistic processes. In: Proceedings 6th IEEE Symposium on Logic in Computer Science, IEEE Computer Society 266–277.Google Scholar
Kemeny, J. and Snell, J. L. (1960) Finite Markov Chains, Van Nostrand.Google Scholar
Larsen, K. G. and Skou, A. (1991) Bisimulation through probabilistic testing. Information and Computation 94 (1)1–28.CrossRefGoogle Scholar
Laud, P. and Vene, V. (2005) A type system for computationally secure information flow. In: Proceedings of the 15th International Symposium on Fundamentals of Computational Theory. Springer-Verlag Lecture Notes in Computer Science 3623 365–377.CrossRefGoogle Scholar
Malacaria, P. (2007) Assessing security threats of looping constructs. In: Proceedings 34th Symposium on Principles of Programming Languages, ACM 225–235.Google Scholar
Myers, A. C., Chong, S., Nystrom, N., Zheng, L. and Zdancewic, S. (2006) Jif: Java + information flow, Cornell University. Available at http://www.cs.cornell.edu/jif/.Google Scholar
Sabelfeld, A. and Myers, A. C. (2003) Language-based information flow security. IEEE Journal on Selected Areas in Communications 21 (1)5–19.CrossRefGoogle Scholar
Sabelfeld, A. and Sands, D. (2000) Probabilistic noninterference for multi-threaded programs. In: Proceedings 13th IEEE Computer Security Foundations Workshop, IEEE Computer Society 200–214.Google Scholar
Smith, G. (2003) Probabilistic noninterference through weak probabilistic bisimulation. In: Proceedings 16th IEEE Computer Security Foundations Workshop, IEEE Computer Society 3–13.Google Scholar
Smith, G. (2006) Improved typings for probabilistic noninterference in a multi-threaded language. Journal of Computer Security 14 (6)591–623.CrossRefGoogle Scholar
Smith, G. and Alpízar, R. (2006) Secure information flow with random assignment and encryption. In: Proceedings 4th ACM Workshop on Formal Methods in Security Engineering, ACM 33–43.CrossRefGoogle Scholar
Smith, G. and Alpízar, R. (2007) Fast probabilistic simulation, nontermination, and secure information flow. In Proceedings 2007 ACM SIGPLAN Workshop on Programming Languages and Analysis for Security, ACM 67–71.CrossRefGoogle Scholar
Smith, G. and Volpano, D. (1998) Secure information flow in a multi-threaded imperative language. In: Proceedings 25th Symposium on Principles of Programming Languages, ACM 355–364.Google Scholar
Volpano, D. and Smith, G. (1997) Eliminating covert flows with minimum typings. In: Proceedings 10th IEEE Computer Security Foundations Workshop, IEEE Computer Society 156–168.CrossRefGoogle Scholar
Volpano, D. and Smith, G. (1999) Probabilistic noninterference in a concurrent language. Journal of Computer Security 7 (2, 3)231–253.CrossRefGoogle Scholar
Volpano, D., Smith, G. and Irvine, C. (1996) A sound type system for secure flow analysis. Journal of Computer Security 4 (2, 3)167–187.CrossRefGoogle Scholar