Abstract
Preserving the confidentiality of data in a distributed system is an increasingly important problem of current security research. Distributed programming often involves message passing over a publicly observable medium, which opens up various opportunities for eavesdropping. Not only may the contents of messages sent on a public channel reveal confidential data, but merely observing the presence of a message on a channel for encrypted traffic may leak information. Another source of leaks is blocking, which may change the observable behavior of a process that attempts to receive on an empty channel.
In this article, we investigate the interplay between, on the one side, public, encrypted, and private (or hidden) channels of communication and, on the other side, blocking and nonblocking communication primitives for a simple multi-threaded language. We argue for timing-sensitive security and give a compositional timing-sensitive confidentiality specification. A key contribution of this article is a security-type system that statically enforces confidentiality. That the type system is not over-restrictive is exemplified by a typable distributed file-server program.
This research was supported by the Department of the Navy, Office of Naval Research, ONR Grant N00014-01-1-0968. Any opinions, findings, conclusions, or recommendations contained in this material are those of the authors and do not necessarily reflect the views of the Office of Naval Research. This work was supported, in part, by TFR, while the first author was at the Department of Computer Science, Chalmers University of Technology and University of Göteborg, Sweden. This work was supported, in part, by the German Research Foundation (DFG).
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
M. Abadi. Secrecy by typing in security protocols. Journal of the ACM, 46(5):749–786, September 1999.
M. Abadi, A. Banerjee, N. Heintze, and J. Riecke. A core calculus of dependency. In Proc. of Symposium on Principles of Programming Languages, January 1999.
M. Abadi and B. Blanchet. Secrecy types for asymmetric communication. In FOSSACS’01, LNCS 2030, pages 25–41, April 2001.
M. Abadi and A. D. Gordon. A calculus for cryptographic protocols: The spi calculus. In Proc. of Conference on Computer and Communications Security, 1997.
M. Abadi and P. Rogaway. Reconciling two views of cryptography (the computational soundness of formal encryption). Journal of Cryptology, 15(2), 2002.
J. Agat. Transforming out timing leaks. In Proc. of Symposium on Principles of Programming Languages, pages 40–53, January 2000.
J. Agat and D. Sands. On confidentiality and algorithms. In Proc. of IEEE Symposium on Security and Privacy, May 2001.
G. R. Andrews. Foundations of Multithreaded, Parallel, and Distributed Programming. Addison Wesley, 2000.
J. Armstrong, R. Virding, C. Wikström, and M. Williams. Concurrent Programming in Erlang. Prentice-Hall, 2nd edition, 1996.
J.-P. Banâtre and C. Bryce. Information flow control in a parallel language framework. In Proc. of IEEE Computer Security Foundations Workshop, June 1993.
A. Banerjee and D. A. Naumann. Secure information flow and pointer confinement in a Java-like language. In Proc. of IEEE Computer Security Foundations Workshop, June 2002.
G. Boudol and I. Castellani. Noninterference for concurrent programs. In ICALP’01, LNCS 2076, pages 382–395, July 2001.
E. S. Cohen. Information transmission in computational systems. ACM SIGOPS Operating Systems Review, 11(5):133–139, 1977.
E. S. Cohen. Information transmission in sequential programs. In R. A. DeMillo, D. P. Dobkin, A. K. Jones, and R. J. Lipton, editors, Foundations of Secure Computation, pages 297–335. Academic Press, 1978.
D. E. Denning. A lattice model of secure information flow. Communications of the ACM, 19(5):236–243, May 1976.
D. E. Denning. Cryptography and Data Security. Addison-Wesley, 1982.
D. E. Denning and P. J. Denning. Certification of programs for secure information flow. Communications of the ACM, 20(7):504–513, July 1977.
R. Focardi and R. Gorrieri. A classification of security properties for process algebras. Journal of Computer Security, 3(1):5–33, 1995.
R. Focardi, R. Gorrieri, and F. Martinelli. Information flow analysis in a discrete-time process algebra. In Proc. of IEEE Computer Security Foundations Workshop, pages 170–184, July 3–5 2000.
J. A. Goguen and J. Meseguer. Security policies and security models. In Proc. of IEEE Symposium on Security and Privacy. April 1982.
J. Gosling, B. Joy, and G. Steele. The Java Language Specification. Addison-Wesley, 1996.
N. Heintze and J. G. Riecke. The SLam calculus: programming with secrecy and integrity. In Proc. of Symposium on Principles of Programming Languages, 1998.
M. Hennessy and J. Riely. Information flow vs resource access in the asynchronous pi-calculus (extended abstract). In ICALP’00, LNCS 1853, pages 415–427, 2000.
C. Hoare. Communicating Sequential Processes (CSP). Prentice Hall, 1985.
K. Honda, V. Vasconcelos, and N. Yoshida. Secure information flow as typed process behaviour. In Proc. of European Symposium on Programming, LNCS 1782, pages 180–199, 2000.
K. Honda and N. Yoshida. A uniform type structure for secure information flow. In Proc. of Symposium on Principles of Programming Languages, January 2002.
B. W. Lampson. A note on the confinement problem. Commun. ACM, 16(10):613–615, Oct. 1973.
P. Laud. Semantics and program analysis of computationally secure information flow. In Proc. of European Symposium on Programming, LNCS 2028, April 2001.
K. R. M. Leino and R. Joshi. A semantic approach to secure information flow. Science of Computer Programming, 37(1–3):113–138, 2000.
H. Mantel. Possibilistic definitions of security-an assembly kit-. In Proc. of IEEE Computer Security Foundations Workshop, pages 185–199, July 2000.
H. Mantel. On the composition of secure systems. In Proc. of IEEE Symposium on Security and Privacy, May 2002.
H. Mantel and A. Sabelfeld. A generic approach to the security of multi-threaded programs. In Proc. of IEEE Computer Security Foundations Workshop, June 2001.
H. Mantel and A. Sabelfeld. A unifying approach to the security of distributed and multi-threaded programs. Journal of Computer Security, 2002. To appear.
D. McCullough. Specifications for multi-level security and hook-up property. In Proc. of IEEE Symposium on Security and Privacy, pages 161–166. May 1987.
J. McLean. The specification and modeling of computer security. Computer, 23(1), January 1990.
J. McLean. A general theory of composition for trace sets closed under selective interleaving functions. In Proc. of IEEE Symposium on Security and Privacy, 1994.
R. Milner. Communication and Concurrency. Prentice Hall, 1989.
M. Mizuno and A. Oldehoeft. Information flow control in a distributed object-oriented system with statically-bound object variables. In Proc. of National Computer Security Conference, pages 56–67, 1987.
B. Pfitzmann and M. Waidner. A model for asynchronous reactive systems and its application to secure message transmission. In Proc. of IEEE Symposium on Security and Privacy, pages 184–200, 2001.
A. D. Pierro, C. Hankin, and H. Wiklicky. Approximate non-interference. In Proc. of IEEE Computer Security Foundations Workshop, June 2002.
R. P. Reitman. Information flow in parallel programs: an axiomatic approach. PhD thesis, Cornell University, 1978.
P. Ryan, S. Schneider, M. Goldsmith, G. Lowe, and B. Roscoe. The Modelling and Analysis of Security Protocols: the CSP Approach. Addison-Wesley, 2001.
A. Sabelfeld. The impact of synchronisation on secure information flow in concurrent programs. In Proc. of International Conference on Perspectives of System Informatics, LNCS 2244, pages 227–241, July 2001.
A. Sabelfeld and D. Sands. Probabilistic noninterference for multi-threaded programs. In Proc. of IEEE Computer Security Foundations Workshop, July 2000.
A. Sabelfeld and D. Sands. A per model of secure information flow in sequential programs. Higher-Order and Symbolic Computation, 14(1):59–91, 2001.
G. Smith. A new type system for secure information flow. In Proc. of IEEE Computer Security Foundations Workshop, pages 115–125, June 2001.
G. Smith and D. Volpano. Secure information flow in a multi-threaded imperative language. In Proc. of Symposium on Principles of Programming Languages, 1998.
D. Volpano. Safety versus secrecy. In Proc. of Symposium on Static Analysis, LNCS 1694, pages 303–311, September 1999.
D. Volpano and G. Smith. Probabilistic noninterference in a concurrent language. Journal of Computer Security, 7(2,3):231–253, November 1999.
D. Volpano, G. Smith, and C. Irvine. A sound type system for secure flow analysis. Journal of Computer Security, 4(3):167–187, 1996.
S. Zdancewic and A. C. Myers. Secure information flow via linear continuations. Higher Order and Symbolic Computation, 2002. To appear.
S. Zdancewic, L. Zheng, N. Nystrom, and A. C. Myers. Untrusted hosts and confidentiality: Secure program partitioning. In Proc. of ACM Symposium on Operating System Principles, October 2001.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sabelfeld, A., Mantel, H. (2002). Static Confidentiality Enforcement for Distributed Programs. In: Hermenegildo, M.V., Puebla, G. (eds) Static Analysis. SAS 2002. Lecture Notes in Computer Science, vol 2477. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45789-5_27
Download citation
DOI: https://doi.org/10.1007/3-540-45789-5_27
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-44235-6
Online ISBN: 978-3-540-45789-3
eBook Packages: Springer Book Archive