A uniform type structure for secure information flow

ABSTRACT

The π-calculus is a formalism of computing in which we can compositionally represent dynamics of major programming constructs by decomposing them into a single communication primitive, the name passing. This work reports our experience in using a linear/affine typed π-calculus for the analysis and development of type systems of programming languages, focussing on secure information flow analysis. After presenting a basic typed calculus for secrecy, we demonstrate its usage by a sound embedding of the dependency core calculus (DCC) and by the development of a novel type discipline for imperative programs which extends both a secure multi-threaded imperative language by Smith and Volpano and (a call-by-value version of) DCC. In each case, the embedding gives a simple proof of noninterference.

REFERENCES

• 1: Abadi, M., Secrecy in programming-language semantics, MFPS XV, ENTCS, 20 (April 1999).
• 2: Martín Abadi , Anindya Banerjee , Nevin Heintze , Jon G. Riecke, A core calculus of dependency, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.147-160, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292555]
• 3: Samson Abramsky , Radha Jagadeesan , Pasquale Malacaria, Full abstraction for PCF, Information and Computation, v.163 n.2, p.409-470, Dec 2000 [doi>10.1006/inco.2000.2930]
• 4: S. Abramsky , K. Honda , G. McCusker, A Fully Abstract Game Semantics for General References, Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science, p.334, June 21-24, 1998
• 5: 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]
• 6: Berger, M., Honda, K. and Yoshida, N., Sequentiality and tile -Calculus, TLCA01, LNCS 2044, 29-45, Springer, 2001.
• 7: Boudol, G., Asynchrony and the pi-calculus, INRIA Research Report 1702, 1992.
• 8: 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
• 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: Riccardo Focardi , Roberto Gorrieri , Fabio Martinelli, Non Interference for the Analysis of Cryptographic Protocols, Proceedings of the 27th International Colloquium on Automata, Languages and Programming, p.354-372, July 09-15, 2000
• 11: Jean-Yves Girard, Linear logic, Theoretical Computer Science, v.50 n.1, p.1-102, Jan. 30, 1987 [doi>10.1016/0304-3975(87)90045-4]
• 12: 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]
• 13: Matthew Hennessy , James Riely, Information Flow vs. Resource Access in the Asynchronous Pi-Calculus, Proceedings of the 27th International Colloquium on Automata, Languages and Programming, p.415-427, July 09-15, 2000
• 14: Kohei Honda, Types for Dynamic Interaction, Proceedings of the 4th International Conference on Concurrency Theory, p.509-523, August 23-26, 1993
• 15: Kohei Honda, Composing processes, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.344-357, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237802]
• 16: Kohei Honda , Vasco Thudichum Vasconcelos , Makoto Kubo, Language Primitives and Type Discipline for Structured Communication-Based Programming, Proceedings of the 7th European Symposium on Programming: Programming Languages and Systems, p.122-138, March 28-April 04, 1998
• 17: Kohei Honda , Mario Tokoro, An Object Calculus for Asynchronous Communication, Proceedings of the European Conference on Object-Oriented Programming, p.133-147, July 15-19, 1991
• 18: 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
• 19: Kohei Honda , Nobuko Yoshida, On reduction-based process semantics, Theoretical Computer Science, v.151 n.2, p.437-486, Nov. 27, 1995
• 20: Kohei Honda , Nobuko Yoshida, Game-theoretic analysis of call-by-value computation, Theoretical Computer Science, v.221 n.1-2, p.393-456, June 28, 1999 [doi>10.1016/S0304-3975(99)00039-0]
• 21: Brian T. Howard, Inductive, coinductive, and pointed types, Proceedings of the first ACM SIGPLAN international conference on Functional programming, p.102-109, May 24-26, 1996, Philadelphia, Pennsylvania, United States
• 22: The Haskell home page, http://haskell.org.
• 23: J. M. E. Hyland , C.-H. L. Ong, On full abstraction for PCF: I, II, and III, Information and Computation, v.163 n.2, p.285-408, Dec 2000 [doi>10.1006/inco.2000.2917]
• 24: Naoki Kobayashi , Benjamin C. Pierce , David N. Turner, Linearity and the pi-calculus, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.358-371, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237804]
• 25: Milner, R., Functions as Processes, MSCS. 2(2):119 141, 1992,
• 26: Robin Milner , Joachim Parrow , David Walker, A calculus of mobile processes, I, Information and Computation, v.100 n.1, p.1-40, Sept. 1992 [doi>10.1016/0890-5401(92)90008-4]
• 27: John C. Mitchell, Foundations of programming languages, MIT Press, Cambridge, MA, 1996
• 28: P. Ørbæk , J. Palsberg, Trust in the λ-calculus, Journal of Functional Programming, v.7 n.6, p.557-591, November 1997 [doi>10.1017/S0956796897002906]
• 29: François Pottier , Sylvain Conchon, Information flow inference for free, Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, p.46-57, September 2000
• 30: Pierce, B and Sangiorgi.D, Typing and subtyping for mobile processes, MSCS 6(5):409-453, 1996.
• 31: 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
• 32: Davide Sangiorgi, &pgr;-calculus, internal mobility, and agent-passing calculi, Theoretical Computer Science, v.167 n.1-2, p.235-274, Oct. 30, 1996
• 33: Andrei Sabelfeld , David Sands, A Per Model of Secure Information Flow in Sequential Programs, Proceedings of the 8th European Symposium on Programming Languages and Systems, p.40-58, March 22-28, 1999
• 34: 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
• 35: 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]
• 36: Mads Tofte, Type inference for polymorphic references, Information and Computation, v.89 n.1, p.1-34, Nov. 1990 [doi>10.1016/0890-5401(90)90018-D]
• 37: Vasco Thudichum Vasconcelos, Typed Concurrent Objects, Proceedings of the 8th European Conference on Object-Oriented Programming, p.100-117, July 04-08, 1994
• 38: 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
• 39: 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
• 40: Yoshida, N., Berger, M. and Honda, K., Strong Normalisation in the re-Calculus, LICS'01, 311-322, (C1) (C2) (C3) IEEE, 2001.
• 41: Yoshida, N., Honda, K. and Berger, M., Linearity and Bisimulation, To appear as MCS technical report, Leicester, 2001.
• 42: Steve Zdancewic , Andrew C. Myers, Secure Information Flow and CPS, Proceedings of the 10th European Symposium on Programming Languages and Systems, p.46-61, April 02-06, 2001