Abstract
There has long been speculation in the scientific literature on how to dynamically enforce parametricity such as that yielded by System F. Almost 20 years ago, Sumii and Pierce proposed a formal compiler from System F into the cryptographic lambda calculus: an untyped lambda calculus extended with an idealised model of encryption. They conjectured that this compiler was fully abstract, i.e. that compiled terms are contextually equivalent if and only if the original terms were, a property that can be seen as a form of secure compilation. The conjecture has received attention in several other publications since then, but remains open to this day.
More recently, several researchers have been looking at gradually-typed languages that extend System F. In this setting it is natural to wonder whether embedding System F into these gradually-typed languages preserves contextual equivalence and thus parametricity.
In this paper, we answer both questions negatively. We provide a concrete counterexample: two System F terms whose contextual equivalence is not preserved by the Sumii-Pierce compiler, nor the embedding into the polymorphic blame calculus. This counterexample relies on the absence in System F of what we call a universal type, i.e., a type that all other types can be injected into and extracted from. As the languages in which System F is compiled have a universal type, the compilation cannot be fully abstract; this paper explains why.
We believe this paper thus sheds light on recent results in the field of gradually typed languages and it provides a perspective for further research into secure compilation of polymorphic languages.
Supplemental Material
Available for Download
This file contains a single PDF file containing the technical appendix described in the article, containing proofs and technical details supporting the results described in the paper.
- Martín Abadi. 1998. Protection in Programming-Language Translations. In ICALP’98. 868–883. Google ScholarCross Ref
- Martín Abadi, Luca Cardelli, Benjamin Pierce, and Gordon Plotkin. 1991. Dynamic Typing in a Statically Typed Language. ACM Trans. Program. Lang. Syst. 13, 2 (April 1991), 237–268. DOI: Google ScholarDigital Library
- Martín Abadi, Cédric Fournet, and Georges Gonthier. 1998. Secure Implementation of Channel Abstractions. In IEEE Symposium on Logic in Computer Science. 105–116. Google ScholarCross Ref
- Martín Abadi, Cédric Fournet, and Georges Gonthier. 1999. Secure Communications Processing for Distributed Languages. In IEEE Symposium on Security and Privacy. 74–88.Google Scholar
- Martín Abadi, Cédric Fournet, and Georges Gonthier. 2000. Authentication Primitives and their Compilation. In Principles of Programming Languages. ACM, 302–315. DOI: Google ScholarDigital Library
- Martín Abadi and Gordon D. Plotkin. 2012. On Protection by Layout Randomization. ACM Transactions on Information and System Security 15, Article 8 (July 2012), 8:1–8:29 pages. DOI: Google ScholarDigital Library
- Pieter Agten, Raoul Strackx, Bart Jacobs, and Frank Piessens. 2012. Secure Compilation to Modern Processors. In Computer Security Foundations Symposium. IEEE, 171–185. DOI: Google ScholarDigital Library
- Amal Ahmed and Matthias Blume. 2008. Typed Closure Conversion Preserves Observational Equivalence. In International Conference on Functional Programming. ACM, 157–168. DOI: Google ScholarDigital Library
- Amal Ahmed, Justin Damner, Jeremy G. Siek, and Philip Wadler. 2017. Theorems for Free for Free. In ICFP.Google Scholar
- Amal Ahmed, Derek Dreyer, and Andreas Rossberg. 2009. State-dependent Representation Independence. In Principles of Programming Languages. ACM, 340–353. DOI: Google ScholarDigital Library
- Amal Ahmed, Robert Bruce Findler, Jeremy G. Siek, and Philip Wadler. 2011a. Blame for All. In Principles of Programming Languages. 201–214. Google ScholarDigital Library
- Amal Ahmed, Robert Bruce Findler, Jeremy G. Siek, and Philip Wadler. 2011b. Blame for All. Technical Report. https: //plt.eecs.northwestern.edu/blame- for- all/Google Scholar
- Amal Ahmed, Lindsey Kuper, and Jacob Matthews. 2011c. Parametric polymorphism through run-time sealing, or, Theorems for low, low prices! (April 2011). http://www.ccs.neu.edu/home/amal/papers/paramseal- tr.pdfGoogle Scholar
- Amal Ahmed, Jacob Matthews, Robert Bruce Findler, and Philip Wadler. 2009. Blame for All. In Workshop on Script-to-Program Evolution (STOP). 1–13. Google ScholarDigital Library
- Robert Atkey, Neil Ghani, and Patricia Johann. 2014. A relationally parametric model of dependent type theory. In Principles of Programming Languages. ACM, 503–515. DOI: Google ScholarDigital Library
- Michele Bugliesi and Marco Giunti. 2007. Secure Implementations of Typed Channel Abstractions. In Principles of Programming Languages. ACM, 251–262. DOI: Google ScholarDigital Library
- Matteo Cimini and Jeremy G. Siek. 2016. The Gradualizer: A Methodology and Algorithm for Generating Gradual Type Systems. In Principles of Programming Languages. ACM. DOI: Google ScholarDigital Library
- Dominique Devriese, Marco Patrignani, and Frank Piessens. 2016. Fully-abstract Compilation by Approximate Backtranslation. In Principles of Programming Languages. 164–177.Google Scholar
- Dominique Devriese, Marco Patrignani, Frank Piessens, and Steven Keuchel. 2017. Modular, Fully-Abstract Compilation by Approximate Back-Translation. to appear in LMCS. (2017). http://arxiv.org/abs/1703.09988Google Scholar
- D. Dreyer, A. Ahmed, and L. Birkedal. 2009. Logical Step-Indexed Logical Relations. In Logic In Computer Science. 71–80. Google ScholarDigital Library
- Robert Bruce Findler and Matthias Felleisen. 2002. Contracts for Higher-order Functions. In International Conference on Functional Programming. ACM. DOI: Google ScholarDigital Library
- Cedric Fournet, Nikhil Swamy, Juan Chen, Pierre-Evariste Dagand, Pierre-Yves Strub, and Benjamin Livshits. 2013. Fully Abstract Compilation to JavaScript. In Principles of Programming Languages. ACM, 371–384. DOI: Google ScholarDigital Library
- Ronald Garcia, Alison M. Clark, and ÃĽric Tanter. 2016. Abstracting Gradual Typing. In Principles of Programming Languages. ACM. DOI: Google ScholarDigital Library
- Jean-Yves Girard. 1972. Interprétation Fonctionelle et Élimination Des Coupures de l’arithmétique d’ordre Supérieur. Ph.D. Dissertation. Université Paris VII.Google Scholar
- Arjun Guha, Jacob Matthews, Robert Bruce Findler, and Shriram Krishnamurthi. 2007. Relationally-parametric Polymorphic Contracts. In Symposium on Dynamic Languages. ACM. DOI: Google ScholarDigital Library
- Yuu Igarashi, Taro Sekiyama, and Atsushi Igarashi. 2017. On Polymorphic Gradual Typing. In International Conference on Functional Programming. ACM. Google ScholarDigital Library
- Radha Jagadeesan, Corin Pitcher, Julian Rathke, and James Riely. 2011. Local Memory via Layout Randomization. In Computer Security Foundations Symposium. IEEE Computer Society, 161–174. DOI: Google ScholarDigital Library
- Yannis Juglaret, Cătălin Hriţcu, Arthur Azevedo de Amorim, and Benjamin C. Pierce. 2016. Beyond Good and Evil: Formalizing the Security Guarantees of Compartmentalizing Compilation. In Computer Security Foundations Symposium. Google ScholarCross Ref
- Yannis Juglaret, Catalin Hritcu, Arthur Azevedo de Amorim, Benjamin C. Pierce, Antal Spector-Zabusky, and Andrew Tolmach. 2015. Towards a Fully Abstract Compiler Using Micro-Policies: Secure Compilation for Mutually Distrustful Components. CoRR abs/1510.00697 (2015). http://arxiv.org/abs/1510.00697Google Scholar
- Adriaan Larmuseau, Marco Patrignani, and Dave Clarke. 2015. A Secure Compiler for ML Modules. In Programming Languages and Systems - 13th Asian Symposium. 29–48. DOI: Google ScholarCross Ref
- Adriaan Larmuseau, Marco Patrignani, and Dave Clarke. 2016. Implementing a Secure Abstract Machine. In Symposium on Applied Computing. ACM, 2041–2048. DOI: Google ScholarDigital Library
- John R. Longley. 2003. Universal Types and What They are Good For. In Domain Theory, Logic and Computation. Springer, Dordrecht, 25–63. DOI: Google ScholarCross Ref
- Jacob Matthews and Amal Ahmed. 2008. Parametric Polymorphism through Run-Time Sealing or, Theorems for Low, Low Prices! LNCS, Vol. 4960. 16–31. Google ScholarCross Ref
- Jacob Matthews and Robert Bruce Findler. 2009. Operational Semantics for Multi-language Programs. ACM Trans. Program. Lang. Syst. 31, 3 (April 2009), 12:1–12:44. DOI: Google ScholarDigital Library
- James H. Morris, Jr. 1973a. Protection in Programming Languages. Commun. ACM 16, 1 (Jan. 1973), 15–21. DOI: Google ScholarDigital Library
- James H. Morris, Jr. 1973b. Types Are Not Sets. In Principles of Programming Languages. 120–124. Google ScholarDigital Library
- Georg Neis, Derek Dreyer, and Andreas Rossberg. 2009. Non-parametric Parametricity. In ICFP ’09. 135–148. Google ScholarDigital Library
- Georg Neis, Derek Dreyer, and Andreas Rossberg. 2011. Non-parametric parametricity. Journal of Functional Programming 21 (2011), 497–562. Google ScholarDigital Library
- Marco Patrignani, Pieter Agten, Raoul Strackx, Bart Jacobs, Dave Clarke, and Frank Piessens. 2015. Secure Compilation to Protected Module Architectures. ACM Trans. Program. Lang. Syst. 37, Article 6 (April 2015), 6:1–6:50 pages. DOI: Google ScholarDigital Library
- Marco Patrignani, Dominique Devriese, and Frank Piessens. 2016. On Modular and Fully Abstract Compilation. In Computer Security Foundations Symposium. Google ScholarCross Ref
- Benjamin Pierce. 2002. Types and Programming Languages. MIT Press.Google ScholarDigital Library
- Benjamin Pierce and Eijiro Sumii. 2000. Relating Cryptography and Polymorphism. (2000). http://www.kb.ecei.tohoku.ac. jp/~sumii/pub/infohide.pdf manuscript.Google Scholar
- Gordon D. Plotkin. 1977. LCF Considered as a Programming Language. Theoretical Computer Science 5 (1977), 223–255. Google ScholarCross Ref
- John C. Reynolds. 1974. Towards a Theory of Type Structure. In Programming Symposium. Lecture Notes in Computer Science, Vol. 19. Springer-Verlag, 408–423. Google ScholarCross Ref
- J. C. Reynolds. 1983. Types, Abstraction, and Parametric Polymorphism. In Information Processing. North Holland, 513–523.Google Scholar
- Jeremy Siek and Philip Wadler. 2016. The key to blame: Gradual typing meets cryptography. (2016). http://homepages.inf. ed.ac.uk/wadler/papers/blame- key/blame- key.pdf draft.Google Scholar
- Jeremy G. Siek and Walid Taha. 2006. Gradual Typing for Functional Languages. In SCHEME. 81–92.Google Scholar
- Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, and John Tang Boyland. 2015. Refined Criteria for Gradual Typing. In Summit on Advances in Programming Languages (Leibniz International Proceedings in Informatics (LIPIcs)), Vol. 32. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 274–293. DOI: Google ScholarCross Ref
- Richard Statman. 1991. A local translation of untyped [lambda] calculus into simply typed [lambda] calculus. Technical Report. http://repository.cmu.edu/cgi/viewcontent.cgi?article=1454&context=mathGoogle Scholar
- Christopher Strachey. 2000. Fundamental Concepts in Programming Languages. Higher-Order and Symbolic Computation 13, 1-2 (April 2000), 11–49. DOI: Google ScholarDigital Library
- Eijiro Sumii and Benjamin C. Pierce. 2003. Logical Relations for Encryption. J. Comput. Secur. 11, 4 (July 2003), 521–554. Google ScholarCross Ref
- Eijiro Sumii and Benjamin C. Pierce. 2004. A Bisimulation for Dynamic Sealing. In Principles of Programming Languages. 161–172. Google ScholarDigital Library
- Asumu Takikawa, Daniel Feltey, Ben Greenman, Max S. New, Jan Vitek, and Matthias Felleisen. 2016. Is Sound Gradual Typing Dead?. In Principles of Programming Languages. ACM. DOI: Google ScholarDigital Library
- Philip Wadler. 1989. Theorems for Free!. In Functional Programming Languages and Computer Architecture. ACM, 347–359. Google ScholarDigital Library
- Philip Wadler. 2007. The Girard-Reynolds isomorphism (second edition). Theoretical Computer Science 375, 1 (2007). DOI: Google ScholarDigital Library
- Philip Wadler and Robert Bruce Findler. 2009. Well-Typed Programs Can’t Be Blamed. In Programming Languages and Systems. Springer, Berlin, Heidelberg, 1–16. DOI: Google ScholarDigital Library
- R. N. M. Watson, J. Woodruff, P. G. Neumann, S. W. Moore, J. Anderson, D. Chisnall, N. Dave, B. Davis, K. Gudka, B. Laurie, S. J. Murdoch, R. Norton, M. Roe, S. Son, and M. Vadera. 2015. CHERI: A Hybrid Capability-System Architecture for Scalable Software Compartmentalization. In IEEE Symposium on Security and Privacy. DOI: Google ScholarDigital Library
Index Terms
- Parametricity versus the universal type
Recommendations
Graduality and parametricity: together again for the first time
Parametric polymorphism and gradual typing have proven to be a difficult combination, with no language yet produced that satisfies the fundamental theorems of each: parametricity and graduality. Notably, Toro, Labrada, and Tanter (POPL 2019) conjecture ...
Gradual parametricity, revisited
Bringing the benefits of gradual typing to a language with parametric polymorphism like System F, while preserving relational parametricity, has proven extremely challenging: first attempts were formulated a decade ago, and several designs were recently ...
Theorems for free for free: parametricity, with and without types
The polymorphic blame calculus integrates static typing, including universal types, with dynamic typing. The primary challenge with this integration is preserving parametricity: even dynamically-typed code should satisfy it once it has been cast to a ...
Comments