François Pottier
Vincent Simonet
Skip Abstract Section
Abstract
This paper presents a type-based information flow analysis for a call-by-value λ-calculus equipped with references, exceptions and let-polymorphism, which we refer to as ML. The type system is constraint-based and has decidable type inference. Its noninterference proof is reasonably light-weight, thanks to the use of a number of orthogonal techniques. First, a syntactic segregation between values and expressions allows a lighter formulation of the type system. Second, noninterference is reduced to subject reduction for a nonstandard language extension. Lastly, a semi-syntactic approach to type soundness allows dealing with constraint-based polymorphism separately.
- Abadi, M., Banerjee, A., Heintze, N., and Riecke, J. G. 1999. A core calculus of dependency. In Conference Record of the 26th ACM Symposium on Principles of Programming Languages. ACM Press, San Antonio, Texas, 147--160. URL: http://www.soe.ucsc.edu/abadi/Papers/flowpopl.ps.]] Google Scholar
Digital Library
- Abadi, M., Lampson, B., and Lévy, J.-J. 1996. Analysis and caching of dependencies. In Proceedings of the 1996 ACM SIGPLAN International Conference on Functional Programming. ACM Press, Philadelphia, Pennsylvania, 83--91. URL: http://www.soe.ucsc.edu/∼abadi/Papers/make-preprint.ps.]] Google ScholarDigital Library
- Banerjee, A. and Naumann, D. 2002. Secure information flow and pointer confinement in a Java-like language. In Proceedings of the 15th IEEE Computer Security Foundations Workshop (CSFW 15). Cape Breton, Nova Scotia, 253--267. URL: http://www.cs.stevens-tech.edu/∼naumann/csfw15.ps.]] Google ScholarDigital Library
- Bell, D. E. and LaPadula, L. J. 1975. Secure computer systems: Unified exposition and Multics interpretation. Tech. Rep. MTR-2997, The MITRE Corp., Bedford, Massachusetts. July. URL: http://www.mitre.org/resources/centers/infosec/infosec.html.]]Google Scholar
- Denning, D. E. 1982. Cryptography and Data Security. Addison-Wesley, Reading, Massachusetts.]] Google ScholarDigital Library
- Fähndrich, M. 1999. Bane: A library for scalable constraint-based program analysis. Ph.D. thesis, University of California at Berkeley. URL: http://research.microsoft.com/∼maf/diss.ps.]]Google Scholar
- Field, J. and Teitelbaum, T. 1990. Incremental reduction in the lambda calculus. In Proceedings of the 1990 ACM Conference on Lisp and Functional Programming. ACM Press, 307--322.]] Google ScholarDigital Library
- Flanagan, C., Sabry, A., Duba, B. F., and Felleisen, M. 1993. The essence of compiling with continuations. In Proceedings of the ACM SIGPLAN'93 Conference on Programming Language Design and Implementation. ACM Press, Albuquerque, New Mexico, 237--247. URL: http://www.cs.rice.edu/CS/PLT/Publications/pldi93-fsdf.ps.gz.]] Google ScholarDigital Library
- Goguen, J. and Meseguer, J. 1982. Security policies and security models. In Proceedings of the 1982 IEEE Symposium on Security and Privacy. IEEE Computer Society Press, Oakland, California, 11--20.]]Google Scholar
- Heintze, N. and Riecke, J. G. 1998. The SLam calculus: Programming with secrecy and integrity. In Conference Record of the 25th ACM Symposium on Principles of Programming Languages. ACM Press, San Diego, California, 365--377. URL: http://cm.bell-labs.com/cm/cs/who/nch/slam.ps.]] Google ScholarDigital Library
- Leroy, X., Doligez, D., Mauny, M., and Weis, P. 1997. The Caml Light system, release 0.74. URL: http://caml.inria.fr/.]]Google Scholar
- Leroy, X., Doligez, D., Garrigue, J., Rémy, D., and Vouillon, J. 2002. The Objective Caml system, release 3.06. URL: http://caml.inria.fr/.]]Google Scholar
- Milner, R., Tofte, M., Harper, R., and MacQueen, D. 1997. The Definition of Standard ML (Revised). The MIT Press.]] Google ScholarDigital Library
- Moggi, E. 1989. An abstract view of programming languages. Tech. Rep. ECS-LFCS-90-113, University of Edinburgh. June. URL: http://www.disi.unige.it/person/MoggiE/ftp/abs-view.ps.gz.]]Google Scholar
- Mycroft, A. 1984. Polymorphic type schemes and recursive definitions. In Proceedings of the 6th International Symposium on Programming, M. Paul and B. Robinet, Eds. Lecture Notes in Computer Science, vol. 167. Toulouse, France, 217--228.]] Google ScholarDigital Library
- Myers, A. C. 1999a. JFlow: practical mostly-static information flow control. In Proceedings of the 26th ACM SIGPLAN-SIGACT on Principles of Programming Languages. ACM Press, San Antonio, Texas, 228--241. URL: http://www.cs.cornell.edu/andru/papers/popl99/myers-popl99.ps.gz.]] Google ScholarDigital Library
- Myers, A. C. 1999b. Mostly-static decentralized information flow control. Ph.D. thesis, Massachusetts Institute of Technology. Technical Report MIT/LCS/TR-783. URL: http://www.cs.cornell.edu/andru/release/tr783.ps.gz.]] Google ScholarDigital Library
- Odersky, M., Sulzmann, M., and Wehr, M. 1999. Type inference with constrained types. Theory and Practice of Object Systems 5, 1, 35--55. URL: http://www.cs.mu.oz.au/∼sulzmann/publications/tapos.ps.]] Google ScholarDigital Library
- Pottier, F. 2000. Wallace: an efficient implementation of type inference with subtyping. URL: http://pauillac.inria.fr/∼fpottier/wallace/.]]Google Scholar
- Pottier, F. 2001. A semi-syntactic soundness proof for HM(X). Research Report 4150, INRIA. Mar. URL:ftp://ftp.inria.fr/INRIA/publication/RR/RR-4150.ps.gz.]]Google Scholar
- Pottier, F. 2002. A simple view of type-secure information flow in the π-calculus. In Proceedings of the 15th IEEE Computer Security Foundations Workshop. Cape Breton, Nova Scotia, 320--330. URL: http://pauillac.inria.fr/∼fpottier/publis/fpottier-csfw15.ps.gz.]] Google ScholarDigital Library
- Pottier, F. and Conchon, S. 2000. Information flow inference for free. In Proceedings of the the 5th ACM SIGPLAN International Conference on Functional Programming (ICFP'00). ACM Press, Montréal, Canada, 46--57. URL: http://pauillac.inria.fr/∼fpottier/publis/fpottier-conchon-icfp00.ps.gz.]] Google ScholarDigital Library
- Pottier, F. and Simonet, V. 2002a. Information flow inference for ML. In Proceedings of the 29th ACM Symposium on Principles of Programming Languages (POPL'02). ACM Press, Portland, Oregon, 319--330. URL: http://pauillac.inria.fr/∼fpottier/publis/fpottier-simonet-popl02.ps.gz.]] Google ScholarDigital Library
- Pottier, F. and Simonet, V. 2002b. Information flow inference for ML. Full version. URL: http://pauillac.inria.fr/∼fpottier/publis/fpottier-simonet-popl02-long.ps.gz.]]Google Scholar
- Rehof, J. 1997. Minimal typings in atomic subtyping. In Conference Record of the 24th ACM Symposium on Principles of Programming Languages. ACM Press, Paris, France, 278--291. URL: http://research.microsoft.com/∼rehof/popl97.ps.]] Google ScholarDigital Library
- Rémy, D. 1993. Type inference for records in a natural extension of ML. In Theoretical Aspects Of Object-Oriented Programming. Types, Semantics and Language Design, C. A. Gunter and J. C. Mitchell, Eds. MIT Press. URL:ftp://ftp.inria.fr/INRIA/Projects/cristal/Didier.Remy/taoop1.ps.gz.]] Google ScholarDigital Library
- Simonet, V. 2002. Fine-grained information flow analysis for a λ-calculus with sum types. In Proceedings of the 15th IEEE Computer Security Foundations Workshop (CSFW 15). Cape Breton, Nova Scotia, 223--237. URL: http://cristal.inria.fr/∼simonet/publis/simonet-csfw-02.ps.gz.]] Google ScholarDigital Library
- Sulzmann, M. 2000. Completenss of constraint-based inference. URL: http://www.cs.mu.oz.au/sulzmann/publications/constraint-inference.ps.]]Google Scholar
- Sulzmann, M., Müller, M., and Zenger, C. 1999. Hindley/Milner style type systems in constraint form. Research Report ACRC--99--009, University of South Australia, School of Computer and Information Science. July. URL: http://www.ps.uni-sb.de/∼mmueller/papers/hm-constraints.ps.gz.]]Google Scholar
- Volpano, D. and Smith, G. 1997a. Eliminating covert flows with minimum typings. In 10th IEEE Computer Security Foundations Workshop. Rockport, MA, 156--168. URL: http://www.cs.nps.navy.mil/people/faculty/volpano/papers/csfw97.ps.Z.]] Google ScholarDigital Library
- Volpano, D. and Smith, G. 1997b. A type-based approach to program security. Lecture Notes in Computer Science 1214, 607--621. URL: http://www.cs.nps.navy.mil/people/faculty/volpano/papers/tapsoft97.ps.Z.]] Google ScholarDigital Library
- Volpano, D., Smith, G., and Irvine, C. 1996. A sound type system for secure flow analysis. J. Computer Security 4, 3, 167--187. URL: http://www.cs.nps.navy.mil/people/faculty/volpano/papers/jcs96.ps.Z.]] Google ScholarDigital Library
- Wadler, P. 1992. Comprehending monads. Mathematical Structures in Computer Science 2, 461--493. URL: http://www.research.avayalabs.com/user/wadler/papers/monads/monads.ps.gz.]]Google ScholarCross Ref
- Wright, A. K. 1995. Simple imperative polymorphism. Lisp and Symbolic Computation 8, 4 (Dec.), 343--356. URL: http://www.cs.rice.edu/CS/PLT/Publications/lasc95-w.ps.gz.]] Google ScholarDigital Library
- Wright, A. K. and Felleisen, M. 1994. A syntactic approach to type soundness. Information and Computation 115, 1 (Nov.), 38--94. URL: http://www.cs.rice.edu/CS/PLT/Publications/ic94-wf.ps.gz.]] Google ScholarDigital Library
- Zdancewic, S. and Myers, A. C. 2001. Secure information flow and CPS. In Proceedings of the 2001 European Symposium on Programming (ESOP'01), D. Sands, Ed. Lecture Notes in Computer Science. Springer Verlag, Genova, Italy. URL: http://www.cs.cornell.edu/zdance/lincont.ps.]] Google ScholarDigital Library
- Zdancewic, S. and Myers, A. C. 2002. Secure information flow via linear continuations. Higher Order and Symbolic Computation. 15, 2-3, 209--234, URL: http://www.cs.cornell.edu/andru/papers/hosc01.ps.gz.]] Google ScholarDigital Library
Index Terms
- Information flow inference for ML
Recommendations
Information flow inference for ML
POPL '02: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languagesThis paper presents a type-based information flow analysis for a call-by-value λ-calculus equipped with references, exceptions and let-polymorphism, which we refer to as Core ML. The type system is constraint-based and has decidable type inference. Its ...
Information flow inference for ML
This paper presents a type-based information flow analysis for a call-by-value λ-calculus equipped with references, exceptions and let-polymorphism, which we refer to as Core ML. The type system is constraint-based and has decidable type inference. Its ...
From ML type inference to stratified type inference
Proceedings of the tenth ACM SIGPLAN international conference on Functional programmingHindley and Milner's type system, in its purest form, allows what one might call full type inference. Even when a program contains no explicit type information, its very structure gives rise to a conjunction of type equations (or, more generally, to a ...
Comments