Typed closure conversion preserves observational equivalence

ABSTRACT

Language-based security relies on the assumption that all potential attacks are bound by the rules of the language in question. When programs are compiled into a different language, this is true only if the translation process preserves observational equivalence.

We investigate the problem of fully abstract compilation, i.e., compilation that both preserves and reflects observational equivalence. In particular, we prove that typed closure conversion for the polymorphic »-calculus with existential and recursive types is fully abstract. Our proof uses operational techniques in the form of a step-indexed logical relation and construction of certain wrapper terms that "back-translate" from target values to source values.

Although typed closure conversion has been assumed to be fully abstract, we are not aware of any previous result that actually proves this.

REFERENCES

• 1: Martín Abadi, Protection in Programming-Language Translations, Proceedings of the 25th International Colloquium on Automata, Languages and Programming, p.868-883, July 13-17, 1998
• 2: 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]
• 3: A. Ahmed. Step-indexed syntactic logical relations for recursive and quantified types. Technical Report TR-01-06, Harvard University, Mar. 2006. ttic.uchicago.edu/~amal.
• 4: A. Ahmed. Step-indexed syntactic logical relations for recursive and quantified types. In ESOP '06, Mar. 2006.
• 5: A. Ahmed and M. Blume. Typed closure conversion preserves observational equivalence. Technical Report TR-2008-07, Department of Computer Science, University of Chicago, July 2008.
• 6: Ken Arnold , James Gosling , David Holmes, Java(TM) Programming Language, The (4th Edition), Addison-Wesley Professional, 2005
• 7: Matthias Blume , David McAllester, Sound and complete models of contracts, Journal of Functional Programming, v.16 n.4-5, p.375-414, July 2006 [doi>10.1017/S0956796806005971]
• 8: Robert Cartwright , Matthias Felleisen, Observable sequentiality and full abstraction, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.328-342, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143232]
• 9: ECMA. ECMA-335: Common Language Infrastructure (CLI). ECMA (European Association for Standardizing Information and Communication Systems), Geneva, Switzerland, third edition, June 2005.
• 10: Matthias Felleisen , Robert Hieb, The revised report on the syntactic theories of sequential control and state, Theoretical Computer Science, v.103 n.2, p.235-271, 14 Sept. 1992 [doi>10.1016/0304-3975(92)90014-7]
• 11: Robert Bruce Findler , Matthias Felleisen, Contracts for higher-order functions, Proceedings of the seventh ACM SIGPLAN international conference on Functional programming, p.48-59, October 04-06, 2002, Pittsburgh, PA, USA
• 12: N. Glew. Object closure conversion. In Higher-Order Operational Techniques in Semantics (HOOTS '99), Sept. 1999.
• 13: Alan Jeffrey, A Fully Abstract Semantics for a Concurrent Functional Language with Monadic Types, Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science, p.255, June 26-29, 1995
• 14: Andrew Kennedy, Securing the .NET programming model, Theoretical Computer Science, v.364 n.3, p.311-317, 8 November 2006 [doi>10.1016/j.tcs.2006.08.014]
• 15: Xavier Leroy, Formal certification of a compiler back-end or: programming a compiler with a proof assistant, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.42-54, January 11-13, 2006, Charleston, South Carolina, USA
• 16: Xavier Leroy, Unboxed objects and polymorphic typing, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.177-188, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143205]
• 17: I. A. Mason and C. L. Talcott. Equivalence in functional languages with effects. J. Funct. Prog., 1(3):287--327, 1991.
• 18: Jacob Matthews , Robert Bruce Findler, Operational semantics for multi-language programs, Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 17-19, 2007, Nice, France
• 19: A. R. Meyer , K. Sieber, Towards fully abstract semantics for local variables, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.191-203, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73577]
• 20: Yasuhiko Minamide , Greg Morrisett , Robert Harper, Typed closure conversion, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.271-283, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237791]
• 21: Greg Morrisett , David Walker , Karl Crary , Neal Glew, From system F to typed assembly language, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.85-97, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268954]
• 22: Ketan Mulmuley, Full abstraction and semantic equivalence, MIT Press, Cambridge, MA, 1987
• 23: A. Nanevski, A. Ahmed, G. Morrisett, and L. Birkedal. Abstract predicates and mutable ADTs in Hoare Type Theory. In ESOP '07, pages 189--204, 2007.
• 24: Andrew M. Pitts, Existential Types: Logical Relations and Operational Equivalence, Proceedings of the 25th International Colloquium on Automata, Languages and Programming, p.309-326, July 13-17, 1998
• 25: G. D. Plotkin. Lambda-definability and logical relations. Memorandum SAI-RM-4, Univ. of Edinburgh, Oct. 1973.
• 26: J. C. Reynolds. Types, abstraction, and parametric polymorphism. Information Processing, pages 513--523, 1983.
• 27: Jon G. Riecke, Fully abstract translations between functional languages, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.245-254, January 21-23, 1991, Orlando, Florida, United States [doi>10.1145/99583.99617]
• 28: Zhong Shao, Flexible representation analysis, Proceedings of the second ACM SIGPLAN international conference on Functional programming, p.85-98, June 09-11, 1997, Amsterdam, The Netherlands
• 29: W. W. Tait. Intensional interpretations of functionals of finite type I. J. of Symbolic Logic, 32(2):198--212, June 1967.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics

General Terms:
Languages, Security

Keywords:
equivalence-preserving compilation, full abstraction, step-indexed logical relations, typed closure conversion