Advertisement

Static Confidentiality Enforcement for Distributed Programs

  • Andrei Sabelfeld
  • Heiko Mantel
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2477)

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.

Keywords

Type System Secure Information Communicate Sequential Process Secure Program High Channel 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    M. Abadi. Secrecy by typing in security protocols. Journal of the ACM, 46(5):749–786, September 1999.Google Scholar
  2. 2.
    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.Google Scholar
  3. 3.
    M. Abadi and B. Blanchet. Secrecy types for asymmetric communication. In FOSSACS’01, LNCS 2030, pages 25–41, April 2001.Google Scholar
  4. 4.
    M. Abadi and A. D. Gordon. A calculus for cryptographic protocols: The spi calculus. In Proc. of Conference on Computer and Communications Security, 1997.Google Scholar
  5. 5.
    M. Abadi and P. Rogaway. Reconciling two views of cryptography (the computational soundness of formal encryption). Journal of Cryptology, 15(2), 2002.Google Scholar
  6. 6.
    J. Agat. Transforming out timing leaks. In Proc. of Symposium on Principles of Programming Languages, pages 40–53, January 2000.Google Scholar
  7. 7.
    J. Agat and D. Sands. On confidentiality and algorithms. In Proc. of IEEE Symposium on Security and Privacy, May 2001.Google Scholar
  8. 8.
    G. R. Andrews. Foundations of Multithreaded, Parallel, and Distributed Programming. Addison Wesley, 2000.Google Scholar
  9. 9.
    J. Armstrong, R. Virding, C. Wikström, and M. Williams. Concurrent Programming in Erlang. Prentice-Hall, 2nd edition, 1996.Google Scholar
  10. 10.
    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.Google Scholar
  11. 11.
    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.Google Scholar
  12. 12.
    G. Boudol and I. Castellani. Noninterference for concurrent programs. In ICALP’01, LNCS 2076, pages 382–395, July 2001.Google Scholar
  13. 13.
    E. S. Cohen. Information transmission in computational systems. ACM SIGOPS Operating Systems Review, 11(5):133–139, 1977.CrossRefGoogle Scholar
  14. 14.
    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.Google Scholar
  15. 15.
    D. E. Denning. A lattice model of secure information flow. Communications of the ACM, 19(5):236–243, May 1976.Google Scholar
  16. 16.
    D. E. Denning. Cryptography and Data Security. Addison-Wesley, 1982.Google Scholar
  17. 17.
    D. E. Denning and P. J. Denning. Certification of programs for secure information flow. Communications of the ACM, 20(7):504–513, July 1977.Google Scholar
  18. 18.
    R. Focardi and R. Gorrieri. A classification of security properties for process algebras. Journal of Computer Security, 3(1):5–33, 1995.Google Scholar
  19. 19.
    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.Google Scholar
  20. 20.
    J. A. Goguen and J. Meseguer. Security policies and security models. In Proc. of IEEE Symposium on Security and Privacy. April 1982.Google Scholar
  21. 21.
    J. Gosling, B. Joy, and G. Steele. The Java Language Specification. Addison-Wesley, 1996.Google Scholar
  22. 22.
    N. Heintze and J. G. Riecke. The SLam calculus: programming with secrecy and integrity. In Proc. of Symposium on Principles of Programming Languages, 1998.Google Scholar
  23. 23.
    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.Google Scholar
  24. 24.
    C. Hoare. Communicating Sequential Processes (CSP). Prentice Hall, 1985.Google Scholar
  25. 25.
    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.Google Scholar
  26. 26.
    K. Honda and N. Yoshida. A uniform type structure for secure information flow. In Proc. of Symposium on Principles of Programming Languages, January 2002.Google Scholar
  27. 27.
    B. W. Lampson. A note on the confinement problem. Commun. ACM, 16(10):613–615, Oct. 1973.Google Scholar
  28. 28.
    P. Laud. Semantics and program analysis of computationally secure information flow. In Proc. of European Symposium on Programming, LNCS 2028, April 2001.Google Scholar
  29. 29.
    K. R. M. Leino and R. Joshi. A semantic approach to secure information flow. Science of Computer Programming, 37(1–3):113–138, 2000.zbMATHMathSciNetGoogle Scholar
  30. 30.
    H. Mantel. Possibilistic definitions of security-an assembly kit-. In Proc. of IEEE Computer Security Foundations Workshop, pages 185–199, July 2000.Google Scholar
  31. 31.
    H. Mantel. On the composition of secure systems. In Proc. of IEEE Symposium on Security and Privacy, May 2002.Google Scholar
  32. 32.
    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.Google Scholar
  33. 33.
    H. Mantel and A. Sabelfeld. A unifying approach to the security of distributed and multi-threaded programs. Journal of Computer Security, 2002. To appear.Google Scholar
  34. 34.
    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.Google Scholar
  35. 35.
    J. McLean. The specification and modeling of computer security. Computer, 23(1), January 1990.Google Scholar
  36. 36.
    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.Google Scholar
  37. 37.
    R. Milner. Communication and Concurrency. Prentice Hall, 1989.Google Scholar
  38. 38.
    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.Google Scholar
  39. 39.
    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.Google Scholar
  40. 40.
    A. D. Pierro, C. Hankin, and H. Wiklicky. Approximate non-interference. In Proc. of IEEE Computer Security Foundations Workshop, June 2002.Google Scholar
  41. 41.
    R. P. Reitman. Information flow in parallel programs: an axiomatic approach. PhD thesis, Cornell University, 1978.Google Scholar
  42. 42.
    P. Ryan, S. Schneider, M. Goldsmith, G. Lowe, and B. Roscoe. The Modelling and Analysis of Security Protocols: the CSP Approach. Addison-Wesley, 2001.Google Scholar
  43. 43.
    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.Google Scholar
  44. 44.
    A. Sabelfeld and D. Sands. Probabilistic noninterference for multi-threaded programs. In Proc. of IEEE Computer Security Foundations Workshop, July 2000.Google Scholar
  45. 45.
    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.zbMATHCrossRefGoogle Scholar
  46. 46.
    G. Smith. A new type system for secure information flow. In Proc. of IEEE Computer Security Foundations Workshop, pages 115–125, June 2001.Google Scholar
  47. 47.
    G. Smith and D. Volpano. Secure information flow in a multi-threaded imperative language. In Proc. of Symposium on Principles of Programming Languages, 1998.Google Scholar
  48. 48.
    D. Volpano. Safety versus secrecy. In Proc. of Symposium on Static Analysis, LNCS 1694, pages 303–311, September 1999.CrossRefGoogle Scholar
  49. 49.
    D. Volpano and G. Smith. Probabilistic noninterference in a concurrent language. Journal of Computer Security, 7(2,3):231–253, November 1999.Google Scholar
  50. 50.
    D. Volpano, G. Smith, and C. Irvine. A sound type system for secure flow analysis. Journal of Computer Security, 4(3):167–187, 1996.Google Scholar
  51. 51.
    S. Zdancewic and A. C. Myers. Secure information flow via linear continuations. Higher Order and Symbolic Computation, 2002. To appear.Google Scholar
  52. 52.
    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.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Andrei Sabelfeld
    • 1
  • Heiko Mantel
    • 2
  1. 1.Department of Computer ScienceCornell UniversityIthacaUSA
  2. 2.German Research Center for Artificial Intelligence (DFKI)SaarbrückenGermany

Personalised recommendations