Information flow vs. resource access in the asynchronous pi-calculus

ABSTRACT

We propose an extension of the asynchronous π-calculus in which a variety of security properties may be captured using types. These are an extension of the input/output types for the π-calculus in which I/O capabilities are assigned specific security levels. The main innovation is a uniform typing system that, by varying slightly the allowed set of types, captures different notions of security.We first define a typing system that ensures that processes running at security level σ cannot access resources with a security level higher than σ. The notion of access control guaranteed by this system is formalized in terms of a Type Safety Theorem.We then show that, by restricting the allowed types, our system prohibits implicit information flow from high-level to low-level processes. We prove that low-level behavior can not be influenced by changes to high-level behavior. This is formalized as a noninterference theorem with respect to may testing.

REFERENCES

• 1: Martín Abadi, Secrecy by Typing inSecurity Protocols, Proceedings of the Third International Symposium on Theoretical Aspects of Computer Software, p.611-638, September 23-26, 1997
• 2: Bell, D. E. and LaPadula, L. J. 1995. Secure computer system: Unified exposition and multics interpretation. Tech. rep. MTR-2997. MITRE Corporation.
• 3: Chiara Bodei , Pierpaolo Degano , Flemming Nielson , Hanne Riis Nielson, Control Flow Analysis for the pi-calculus, Proceedings of the 9th International Conference on Concurrency Theory, p.84-98, September 08-11, 1998
• 4: Chiara Bodei , Pierpaolo Degano , Flemming Nielson , Hanne Riis Nielson, Static Analysis of Processes for No and Read-Up nad No Write-Down, Proceedings of the Second International Conference on Foundations of Software Science and Computation Structure, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'99, p.120-134, March 22-28, 1999
• 5: Boudol, G. 1992. Asynchrony and the π-calculus. Tech. Rep. 1702. INRIA-Sophia Antipolis.
• 6: Gérard Boudol , Ilaria Castellani, Noninterference for Concurrent Programs, Proceedings of the 28th International Colloquium on Automata, Languages and Programming,, p.382-395, July 08-12, 2001
• 7: Ilaria Castellani , Matthew Hennessy, Testing Theories for Asynchronous Languages, Proceedings of the 18th Conference on Foundations of Software Technology and Theoretical Computer Science, p.90-101, December 17-19, 1998
• 8: De Nicola, R. and Hennessy, M. 1984. Testing equivalences for processes. Theoret. Comput. Sci. 24, 83--113.
• 9: 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]
• 10: Focardi, R., Ghelli, A., and Gorrieri, R. 1997. Using noninterference for the analysis of security protocols. In Proceedings of DIMACS Workshop on Design and Formal Verification of Security Protocols.
• 11: Focardi, R. and Gorrieri, R. 1995. A classification of security properties for process algebras. J. Comput. Sec. 3, 1.
• 12: Riccardo Focardi , Roberto Gorrieri, The Compositional Security Checker: A Tool for the Verification of Information Flow Security Properties, IEEE Transactions on Software Engineering, v.23 n.9, p.550-571, September 1997 [doi>10.1109/32.629493]
• 13: Focardi, R. and Gorrieri, R. 1997b. Noninterference: Past, present and future. In Proceedings of DARPA Workshop on Foundations for Secure Mobile Code.
• 14: Cédric Fournet , Georges Gonthier , Jean-Jacques Lévy , Luc Maranget , Didier Rémy, A Calculus of Mobile Agents, Proceedings of the 7th International Conference on Concurrency Theory, p.406-421, August 26-29, 1996
• 15: Goguen, J. A. and Meseguer, J. 1992 Security policies and security models. In IEEE Symp. Sec. Priv.
• 16: Nevin Heintze , Jon G. Riecke, The SLam calculus: programming with secrecy and integrity, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.365-377, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268976]
• 17: Matthew Hennessy , James Riely, Resource access control in systems of mobile agents, Information and Computation, v.173 n.1, p.82-120, February 25, 2002 [doi>10.1006/inco.2001.3089]
• 18: Kohei Honda , Mario Tokoro, On Asynchronous Communication Semantics, Proceedings of the Workshop on Object-Based Concurrent Computing, p.21-51, July 15-16, 1991
• 19: Kohei Honda , Vasco Thudichum Vasconcelos , Nobuko Yoshida, Secure Information Flow as Typed Process Behaviour, Proceedings of the 9th European Symposium on Programming Languages and Systems, p.180-199, April 02, 2000
• 20: R. Milner, Communication and Concurrency, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
• 21: Robin Milner , Joachim Parrow , David Walker, Modal logics for mobile processes, Theoretical Computer Science, v.114 n.1, p.149-171, June 14 1993
• 22: Pierce, B. and Sangiorgi, D. 1996. Typing and subtyping for mobile processes. Math. Struct. Comput. Sci. 6, 5, 409--454. (Extended abstract in LICS '93).
• 23: Benjamin C. Pierce , David N. Turner, Pict: a programming language based on the Pi-Calculus, Proof, language, and interaction: essays in honour of Robin Milner, MIT Press, Cambridge, MA, 2000
• 24: Gregory R. Andrews , Richard P. Reitman, An Axiomatic Approach to Information Flow in Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.2 n.1, p.56-76, Jan. 1980 [doi>10.1145/357084.357088]
• 25: James Riely , Matthew Hennessy, Trust and partial typing in open systems of mobile agents, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.93-104, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292551]
• 26: A. W. Roscoe , J. C. P. Woodcock , L. Wulf, Non-Interference Through Determinism, Proceedings of the Third European Symposium on Research in Computer Security, p.33-53, November 07-09, 1994
• 27: P Y A Ryan , S A Schneider, Process Algebra and Non-interference, Proceedings of the 1999 IEEE Computer Security Foundations Workshop, p.214, June 28-30, 1999
• 28: 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]
• 29: Dennis Volpano , Cynthia Irvine , Geoffrey Smith, A sound type system for secure flow analysis, Journal of Computer Security, v.4 n.2-3, p.167-187, Jan. 1996
• 30: Nobuko Yoshida, Graph Types for Monadic Mobile Processes, Proceedings of the 16th Conference on Foundations of Software Technology and Theoretical Computer Science, p.371-386, December 18-20, 1996

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.2 COMPUTER-COMMUNICATION NETWORKS
      C.2.0 General
          Subjects: Security and protection (e.g., firewalls)

Additional Classification:
  C. Computer Systems Organization
  C.2 COMPUTER-COMMUNICATION NETWORKS
      C.2.1 Network Architecture and Design
          Subjects: Distributed networks

  D. Software
  D.4 OPERATING SYSTEMS
      D.4.6 Security and Protection
          Subjects: Information flow controls

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Process models; Operational semantics
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

General Terms:
Design, Security, Theory, Verification

Keywords:
Distributed process language, I/O subtyping, information flow, may testing, noninterference, pi-calculus, security, security types