Information flow security of multi-threaded distributed programs

ABSTRACT

We study noninterference in the setting of multi-threaded distributed programs in which threads share local memories and multi-threaded processes communicate over an insecure network using encryption primitives to secure messages. We extend a simple imperative language with cryptographic operations which are modelled as special expressions respecting the Dolev-Yao assumptions. Then, we adapt to our setting the notion of patterns proposed by Abadi and Rogaway for modelling the equivalence of cryptographic expressions. Based on this notion, we naturally obtain a definition of strongly secure programs corresponding to the one proposed by Sabelfeld and Sands for programs without cryptography. This is, to the best of our knowledge, the first definition of noninterference in a multi-threaded distributed setting, with insecure channels and cryptography. We prove compositionality of secure programs and we adapt the type system of Sabelfeld and Sands to our setting, proving its correctness.

REFERENCES

• 1: Martín Abadi, Secrecy by typing in security protocols, Journal of the ACM (JACM), v.46 n.5, p.749-786, Sept. 1999 [doi>10.1145/324133.324266]
• 2: Martín Abadi , Jan Jürjens, Formal Eavesdropping and Its Computational Interpretation, Proceedings of the 4th International Symposium on Theoretical Aspects of Computer Software, p.82-94, October 29-31, 2001
• 3: Martin Abadi , Phillip Rogaway, Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption), Journal of Cryptology, v.20 n.3, p.395-395, July 2007 [doi>10.1007/s00145-007-0203-0]
• 4: Johan Agat, Transforming out timing leaks, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.40-53, January 19-21, 2000, Boston, MA, USA [doi>10.1145/325694.325702]
• 5: Aslan Askarov, Daniel Hedin, and Andrei Sabelfeld. Cryptographically-masked flows. In Proceedings of the International Static Analysis Symposium, Seoul, Korea, August 2006. Springer-Verlag.
• 6: Matteo Centenaro and Riccardo Focardi. Information flow security of multi-threaded distributed programs (full version). http://www.dsi.unive.it/~mcentena/centenaro-focardi.pdf, 2008.
• 7: Tom Chothia, Dominic Duggan, and Jan Vitek. Type-based distributed access control. In Proceedings of the 16th IEEE Computer Security Foundations Workshop (CSFW?03), Asilomar, CA, USA, July 2003.
• 8: Dorothy E. Denning , Peter J. Denning, Certification of programs for secure information flow, Communications of the ACM, v.20 n.7, p.504-513, July 1977 [doi>10.1145/359636.359712]
• 9: J. A. Goguen and J. Meseguer. Security policies and security models. In IEEE Computer Society Press, editor, Proceedings of the 1982 IEEE Symposium on Security and Privacy, pages 11--20, 1982.
• 10: Peeter Laud, Secrecy types for a simulatable cryptographic library, Proceedings of the 12th ACM conference on Computer and communications security, November 07-11, 2005, Alexandria, VA, USA [doi>10.1145/1102120.1102126]
• 11: Peeter Laud, On the computational soundness of cryptographically masked flows, Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 07-12, 2008, San Francisco, California, USA
• 12: Heiko Mantel , Andrei Sabelfeld, A unifying approach to the security of distributed and multi-threaded programs, Journal of Computer Security, v.11 n.4, p.615-676, July 2003
• 13: Andrei Sabelfeld and Heiko Mantel. Static confidentiality enforcement for distributed programs. In Proceeding of the 9th International Static Analysis Symposium, volume 2477, Madrid, Spain, September 2002. Springer.
• 14: Andrei Sabelfeld and Andrew C. Myers. Language-based information-flow security. IEEE Journal on Selected Areas in Communications, 21(1), January 2003.
• 15: Andrei Sabelfeld , David Sands, Probabilistic Noninterference for Multi-Threaded Programs, Proceedings of the 13th IEEE workshop on Computer Security Foundations, p.200, July 03-05, 2000
• 16: Geoffrey Smith, A New Type System for Secure Information Flow, Proceedings of the 14th IEEE workshop on Computer Security Foundations, p.115, June 11-13, 2001
• 17: Geoffrey Smith, Secure information flow with random assignment and encryption, Proceedings of the fourth ACM workshop on Formal methods in security, p.33-44, November 03-03, 2006, Alexandria, Virginia, USA [doi>10.1145/1180337.1180341]
• 18: Geoffrey Smith , Dennis Volpano, Secure information flow in a multi-threaded imperative language, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.355-364, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268975]
• 19: Jeffrey A. Vaughan , Steve Zdancewic, A Cryptographic Decentralized Label Model, Proceedings of the 2007 IEEE Symposium on Security and Privacy, p.192-206, May 20-23, 2007 [doi>10.1109/SP.2007.5]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Program analysis

General Terms:
Languages, Security, Theory, Verification

Keywords:
bisimulation, information flow, language-based security, symbolic cryptography