Abstract
A compiler is fully-abstract if the compilation from source language programs to target language programs reflects and preserves behavioural equivalence. Such compilers have important security benefits, as they limit the power of an attacker interacting with the program in the target language to that of an attacker interacting with the program in the source language. Proving compiler full-abstraction is, however, rather complicated. A common proof technique is based on the back-translation of target-level program contexts to behaviourally-equivalent source-level contexts. However, constructing such a back-translation is problematic when the source language is not strong enough to embed an encoding of the target language. For instance, when compiling from the simply-typed λ-calculus (λτ) to the untyped λ-calculus (λu), the lack of recursive types in λτ prevents such a back-translation. We propose a general and elegant solution for this problem. The key insight is that it suffices to construct an approximate back-translation. The approximation is only accurate up to a certain number of steps and conservative beyond that, in the sense that the context generated by the back-translation may diverge when the original would not, but not vice versa. Based on this insight, we describe a general technique for proving compiler full-abstraction and demonstrate it on a compiler from λτ to λu . The proof uses asymmetric cross-language logical relations and makes innovative use of step-indexing to express the relation between a context and its approximate back-translation. We believe this proof technique can scale to challenging settings and enable simpler, more scalable proofs of compiler full-abstraction.
- M. Abadi. Protection in programming-language translations. In Secure Internet programming, pages 19–34. Springer-Verlag, 1999. ISBN 3-540-66130-1. M. Abadi and G. D. Plotkin. On protection by layout randomization. ACM Transactions on Information and System Security, 15: 8:1–8:29, July 2012. ISSN 1094-9224. doi: 10.1145/2240276. Google ScholarDigital Library
- 2240279.Google Scholar
- M. Abadi, A. Banerjee, N. Heintze, and J. G. Riecke. A core calculus of dependency. In Principles of Programming Languages, pages 147–160. ACM, 1999. doi: 10.1145/292540.292555. Google ScholarDigital Library
- P. Agten, R. Strackx, B. Jacobs, and F. Piessens. Secure compilation to modern processors. In Computer Security Foundations, pages 171–185, 2012. Google ScholarDigital Library
- A. Ahmed and M. Blume. Typed closure conversion preserves observational equivalence. In International Conference on Functional Programming, pages 157–168. ACM, 2008. doi: 10.1145/ 1411204.1411227. Google ScholarDigital Library
- A. Ahmed and M. Blume. An equivalence-preserving CPS translation via multi-language semantics. In International Conference on Functional Programming, pages 431–444. ACM, 2011. doi: 10.1145/2034773.2034830. Google ScholarDigital Library
- N. Benton and C.-K. Hur. Biorthogonality, step-indexing and compiler correctness. In International Conference on Functional Programming, volume 44, pages 97–108. ACM, 2009. Google ScholarDigital Library
- doi: 10.1145/1596550.1596567.Google Scholar
- N. Benton and C.-K. Hur. Realizability and compositional compiler correctness for a polymorphic language. Technical report, MSR, 2010.Google Scholar
- W. J. Bowman and A. Ahmed. Noninterference for free. In International Conference on Functional Programming. ACM, 2015. Google ScholarDigital Library
- P.-L. Curien. Definability and full abstraction. Electron. Notes Theor. Comput. Sci., 172:301–310, 2007. ISSN 1571-0661. doi: 10.1016/j.entcs.2007.02.011. D. Devriese, M. Patrignani, and F. Piessens. Fully abstract compilation by approximate back-translation: Technical appendix. Technical Report CW 687, Dept. of Computer Science, KU Leuven, 2016. Google ScholarDigital Library
- D. Dreyer, G. Neis, and L. Birkedal. The impact of higher-order state and control effects on local relational reasoning. In International Conference on Functional Programming, pages 143–156, 2010. doi: 10.1145/1863543.1863566. Google ScholarDigital Library
- C. Fournet, N. Swamy, J. Chen, P.-E. Dagand, P.-Y. Strub, and B. Livshits. Fully abstract compilation to JavaScript. In Principles of Programming Languages, pages 371–384. ACM, 2013. Google ScholarDigital Library
- doi: 10.1145/2429069.2429114.Google Scholar
- D. Gorla and U. Nestman. Full abstraction for expressiveness: History, myths and facts. Math. Struct. Comp. Science, 2014.Google Scholar
- C.-K. Hur and D. Dreyer. A Kripke logical relation between ML and assembly. In Principles of Programming Languages, pages 133–146. ACM, 2011. doi: 10.1145/1926385.1926402. Google ScholarDigital Library
- C.-K. Hur, D. Dreyer, G. Neis, and V. Vafeiadis. The marriage of bisimulations and Kripke logical relations. In Principles of Programming Languages, pages 59–72. ACM, 2012. doi: 10.1145/2103656.2103666. Google ScholarDigital Library
- R. Jagadeesan, C. Pitcher, J. Rathke, and J. Riely. Local memory via layout randomization. In Computer Security Foundations Symposium, pages 161–174. IEEE Computer Society, 2011. doi: 10.1109/CSF.2011.18. A. Kennedy. Securing the .NET programming model. Theor. Comput. Sci., 364(3):311–317, Nov. 2006. ISSN 0304-3975. Google ScholarDigital Library
- doi: 10.1016/j.tcs.2006.08.014. D. MacQueen, G. Plotkin, and R. Sethi. An ideal model for recursive polymorphic types. In Principles of Programming Languages, pages 165–174. ACM, 1984. doi: 10.1145/800017. Google ScholarDigital Library
- 800528.Google Scholar
- J. Matthews and A. Ahmed. Parametric polymorphism through run-time sealing or, theorems for low, low prices! In Programming Languages and Systems, volume 4960 of LNCS, pages 16–31. Springer Berlin Heidelberg, 2008. doi: 10.1007/ 978-3-540-78739-6_2. J. Matthews and R. B. Findler. Operational semantics for multilanguage programs. ACM Transactions on Programming Languages and Systems, 31:12:1–12:44, Apr. 2009. ISSN 0164- 0925. doi: 10.1145/1498926.1498930. Google ScholarDigital Library
- G. McCusker. Full abstraction by translation. Advances in Theory and Formal Methods of Computing, 1996.Google Scholar
- J. C. Mitchell. On abstraction and the expressive power of programming languages. Science of Computer Programming, 21(2):141 – 163, 1993. ISSN 0167-6423. doi: 10.1016/0167-6423(93) 90004-9. G. Morrisett, K. Crary, N. Glew, D. Grossman, R. Samuels, F. Smith, D. Walker, S. Weirich, and S. Zdancewic. TALx86: A realistic typed assembly language. In Second Workshop on Compiler Support for System Software, pages 25–35, 1999. Google ScholarDigital Library
- G. Neis, D. Dreyer, and A. Rossberg. Non-parametric parametricity. In International Conference on Functional Programming, pages 135–148. ACM, 2009. doi: 10.1145/1596550.1596572. Google ScholarDigital Library
- G. Neis, C.-K. Hur, J.-O. Kaiser, C. McLaughlin, D. Dreyer, and V. Vafeiadis. Pilsner: A compositionally verified compiler for a higher-order imperative language. In International Conference on Functional Programming. ACM, 2015. Google ScholarDigital Library
- J. Parrow. General conditions for full abstraction. Math. Struct. Comp. Science, 2014.Google Scholar
- M. Patrignani. The Tome of Secure Compilation: Fully Abstract Compilation to Protected Modules Architectures. PhD thesis, KU Leuven, Leuven, Belgium, May 2015.Google Scholar
- M. Patrignani, P. Agten, R. Strackx, B. Jacobs, D. Clarke, and F. Piessens. Secure compilation to protected module architectures. ACM Trans. Program. Lang. Syst., 37(2):6:1–6:50, Apr. 2015. ISSN 0164-0925. doi: 10.1145/2699503. Google ScholarDigital Library
- J. T. Perconti and A. Ahmed. Verifying an open compiler using multi-language semantics. In ESOP, volume 8410 of Lecture Notes in Computer Science, pages 128–148, 2014.Google Scholar
- B. C. Pierce. Types and programming languages. MIT press, 2002. Google ScholarDigital Library
- G. D. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5:223–255, 1977.Google ScholarCross Ref
- doi: 10.1016/ 0304-3975(77)90044-5. J. G. Riecke. Fully abstract translations between functional languages. Mathematical Structures in Computer Science, 3:387–415, 12 1993. ISSN 1469-8072.Google ScholarCross Ref
- doi: 10.1017/ S0960129500000293.Google Scholar
- E. Ritter and A. M. Pitts. A fully abstract translation between a Î˙z-calculus with reference types and standard ml. In M. Dezani-Ciancaglini and G. Plotkin, editors, Typed Lambda Calculi and Applications, volume 902 of LNCS, pages 397–413. Springer Berlin Heidelberg, 1995. ISBN 978-3-540-59048-4. doi: 10. 1007/BFb0014067. Google ScholarDigital Library
- D. Scott. Data types as lattices. SIAM Journal on Computing, 5(3): 522–587, 1976. doi: 10.1137/0205037.Google ScholarDigital Library
- N. Shikuma and A. Igarashi. Proving noninterference by a fully complete translation to the simply typed λ-calculus. In M. Okada and I. Satoh, editors, Advances in Computer Science - ASIAN 2006. Secure Software and Related Issues, volume 4435 of LNCS, pages 301–315. Springer Berlin Heidelberg, 2007. doi: 10.1007/978-3-540-77505-8_24. S. F. Smith. The coverage of operational semantics. In Higher Order Operational Techniques in Semantics, Publications of the Newton Institute, pages 307–346. Cambridge University Press, 1998. Google ScholarDigital Library
Index Terms
- Fully-abstract compilation by approximate back-translation
Recommendations
Fully abstract compilation via universal embedding
ICFP 2016: Proceedings of the 21st ACM SIGPLAN International Conference on Functional ProgrammingA fully abstract compiler guarantees that two source components are observationally equivalent in the source language if and only if their translations are observationally equivalent in the target. Full abstraction implies the translation is secure: ...
Fully-abstract compilation by approximate back-translation
POPL '16: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming LanguagesA compiler is fully-abstract if the compilation from source language programs to target language programs reflects and preserves behavioural equivalence. Such compilers have important security benefits, as they limit the power of an attacker ...
Fully abstract compilation via universal embedding
ICFP '16A fully abstract compiler guarantees that two source components are observationally equivalent in the source language if and only if their translations are observationally equivalent in the target. Full abstraction implies the translation is secure: ...
Comments