Information flow inference for free

ABSTRACT

This paper shows how to systematically extend an arbitrary type system with dependency information, and how soundness and non-interference proofs for the new system may rely upon, rather than duplicate, the soundness proof of the original system. This allows enriching virtually any of the type systems known today with information flow analysis, while requiring only a minimal proof effort.Our approach is based on an untyped operational semantics for a labelled calculus akin to core ML. Thus, it is simple, and should be applicable to other computing paradigms, such as object or process calculi.The paper also discusses access control, and shows it may be viewed as entirely independent of information flow control. Letting the two mechanisms coexist, without interacting, yields a simple and expressive type system, which allows, in particular, "selective" declassification.

REFERENCES

• 1: 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]
• 2: Martín Abadi , Butler Lampson , Jean-Jacques Lévy, Analysis and caching of dependencies, Proceedings of the first ACM SIGPLAN international conference on Functional programming, p.83-91, May 24-26, 1996, Philadelphia, Pennsylvania, United States
• 3: Alexander Aiken , Manuel Fähndrich , Jeffrey S. Foster , Zhendong Su, A Toolkit for Constructing Type- and Constraint-Based Program Analyses, Proceedings of the Second International Workshop on Types in Compilation, p.78-96, March 25-27, 1998
• 4: 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]
• 5: Jean-Pierre Banâtre , Ciarán Bryce , Daniel Le Métayer, Compile-Time Detection of Information Flow in Sequential Programs, Proceedings of the Third European Symposium on Research in Computer Security, p.55-73, November 07-09, 1994
• 6: Dorothy Elizabeth Rob Denning, Cryptography and Data Security, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1982
• 7: 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]
• 8: J. S. Fenton. Memoryless subsystems. The Computer Journal, 17(2):143-147, May 1974.
• 9: Cédric Fournet , Cosimo Laneve , Luc Maranget , Didier Rémy, Implicit Typing à la ML for the Join-Calculus, Proceedings of the 8th International Conference on Concurrency Theory, p.196-212, July 01-04, 1997
• 10: You-Chin Fuh , Prateek Mishra, Polymorphic Subtype Inference: Closing the Theory-Practice Gap, Proceedings of the International Joint Conference on Theory and Practice of Software Development, Volume 2: Advanced Seminar on Foundations of Innovative Software Development II and Colloquium on Current Issues in Programming Languages, p.167-183, March 13-17, 1989
• 11: J. Goguen and J. Meseguer. Security policies and security models. In Proceedings of the 1982 IEEE Symposium on Security and Privacy, pages 11-20, Apr. 1982.
• 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: Butler W. Lampson, A note on the confinement problem, Communications of the ACM, v.16 n.10, p.613-615, Oct. 1973 [doi>10.1145/362375.362389]
• 14: A. Myers, Mostly-Static Decentralized Information Flow Control, Massachusetts Institute of Technology, Cambridge, MA, 1999
• 15: A. C. Myers and B. Liskov. Complete, safe information ?ow withdecentralized labels. In Proceedings of the 1998 IEEE Symposium on Security and Privacy, pages 186-197, May 1998.
• 16: Martin Odersky , Martin Sulzmann , Martin Wehr, Type inference with constrained types, Theory and Practice of Object Systems, v.5 n.1, p.35-55, Jan. 1999 [doi>10.1002/(SICI)1096-9942(199901/03)5:1<35::AID-TAPO4>3.0.CO;2-4]
• 17: 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]
• 18: J. Palsberg and P. ~rb~k. Trust in the A-calculus. Lecture Notes in Computer Science, 983:314-330, 1995.
• 19: F. Pottier. Simplifying subtyping constraints: a theory. Submitted for journal publication, Dec. 1998.
• 20: F. Pottier. Type inference in the presence of subtyping: from theory to practice. Technical Report 3483, INRIA, Sept. 1998.
• 21: Didier Rémy, Projective ML, Proceedings of the 1992 ACM conference on LISP and functional programming, p.66-75, June 22-24, 1992, San Francisco, California, United States
• 22: Didier Rémy , Jérôme Vouillon, Objective ML: a simple object-oriented extension of ML, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.40-53, January 15-17, 1997, Paris, France [doi>10.1145/263699.263707]
• 23: John L. Ross , Mooly Sagiv, Building a bridge between pointer aliases and program dependences, Nordic Journal of Computing, v.5 n.4, p.361-386, Winter 1998
• 24: Geoffrey Smith, Polymorphic Type Inference with Overloading and Subtyping, Proceedings of the International Joint Conference CAAP/FASE on Theory and Practice of Software Development, p.671-685, April 13-17, 1993
• 25: A. Stoughton. Access ?ow: A protection model which integrates access control and information ?ow. In Proceedings of the 1981 IEEE Symposium on Security and Privacy, pages 9-18, 1981.
• 26: Valery Trifonov , Scott F. Smith, Subtyping Constrained Types, Proceedings of the Third International Symposium on Static Analysis, p.349-365, September 24-26, 1996
• 27: Dennis M. Volpano , Geoffrey Smith, A Type-Based Approach to Program Security, Proceedings of the 7th International Joint Conference CAAP/FASE on Theory and Practice of Software Development, p.607-621, April 14-18, 1997
• 28: Andrew K. Wright , Matthias Felleisen, A syntactic approach to type soundness, Information and Computation, v.115 n.1, p.38-94, Nov. 15, 1994 [doi>10.1006/inco.1994.1093]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
  D.4 OPERATING SYSTEMS
      D.4.6 Security and Protection
          Subjects: Access controls

  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

General Terms:
Design, Languages, Performance, Reliability, Security, Theory, Verification