Max S. New
William J. Bowman
ABSTRACT
A 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: target-language attackers can make no more observations of a compiled component than a source-language attacker interacting with the original source component. Proving full abstraction for realistic compilers is challenging because realistic target languages contain features (such as control effects) unavailable in the source, while proofs of full abstraction require showing that every target context to which a compiled component may be linked can be back-translated to a behaviorally equivalent source context.
We prove the first full abstraction result for a translation whose target language contains exceptions, but the source does not. Our translation---specifically, closure conversion of simply typed λ-calculus with recursive types---uses types at the target level to ensure that a compiled component is never linked with attackers that have more distinguishing power than source-level attackers. We present a new back-translation technique based on a shallow embedding of the target language into the source language at a dynamic type. Then boundaries are inserted that mediate terms between the untyped embedding and the strongly-typed source. This technique allows back-translating non-terminating programs, target features that are untypeable in the source, and well-bracketed effects.
- M. Abadi. Protection in programming-language translations. In International Colloquium on Automata, Languages and Programming (ICALP), pages 868–883, 1998. Google Scholar
Digital Library
- M. Abadi and G. Plotkin. On protection by layout randomization. ACM Transactions on Information and Systems Security, 15(2), July 2012. Google ScholarDigital Library
- P. Agten, R. Strackx, B. Jacobs, and F. Piessens. Secure compilation to modern processors. In Computer Security Foundations Symposium (CSF), pages 171–185, 2012. Google ScholarDigital Library
- A. Ahmed. Step-indexed syntactic logical relations for recursive and quantified types. In European Symposium on Programming (ESOP), pages 69–83, Mar. 2006. Google ScholarDigital Library
- A. Ahmed. Verified Compilers for a Multi-Language World. In T. Ball, R. Bodik, S. Krishnamurthi, B. S. Lerner, and G. Morrisett, editors, 1st Summit on Advances in Programming Languages (SNAPL 2015), volume 32 of Leibniz International Proceedings in Informatics (LIPIcs), pages 15–31, 2015.Google Scholar
- A. Ahmed and M. Blume. Typed closure conversion preserves observational equivalence. In International Conference on Functional Programming (ICFP), Victoria, British Columbia, Canada, pages 157– 168, Sept. 2008. Google ScholarDigital Library
- A. Ahmed and M. Blume. An equivalence-preserving CPS translation via multi-language semantics. In International Conference on Functional Programming (ICFP), Tokyo, Japan, pages 431–444, Sept. 2011. Google ScholarDigital Library
- N. Benton. Embedded interpreters. Journal of Functional Programming, 15(04):503–542, 2005. Google ScholarDigital Library
- N. Benton and A. Kennedy. Exceptional syntax. Journal of Functional Programming, 11(04):395–410, 2001. Google ScholarDigital Library
- N. Benton, A. Kennedy, and G. Russell. Compiling Standard ML to Java bytecodes. In International Conference on Functional Programming (ICFP), Baltimore, Maryland, USA, pages 129–140, 1998. Google ScholarDigital Library
- W. J. Bowman and A. Ahmed. Noninterference for free. In International Conference on Functional Programming (ICFP), Vancouver, British Columbia, Canada, 2015. Google ScholarDigital Library
- D. Devriese, M. Patrignani, and F. Piessens. Fully-abstract compilation by approximate back-translation. In ACM Symposium on Principles of Programming Languages (POPL), St. Petersburg, Florida, page To appear, 2016. Google ScholarDigital Library
- D. Dreyer, G. Neis, and L. Birkedal. The impact of higher-order state and control effects on local relational reasoning. Journal of Functional Programming, 22(4&5):477–528, 2012. Google ScholarDigital Library
- V. D’Silva, M. Payer, and D. Song. The correctness-security gap in compiler optmization. In Language-theoretic Security IEEE Security and Privacy Workshop (LangSec), 2015. Google ScholarDigital Library
- M. Felleisen and R. Hieb. A revised report on the syntactic theories of sequential control and state. Theor. Comput. Sci., 103(2):235–271, 1992. Google ScholarDigital Library
- C. Fournet, N. Swamy, J. Chen, P.-E. Dagand, P.-Y. Strub, and B. Livshits. Fully abstract compilation to JavaScript. In ACM Symposium on Principles of Programming Languages (POPL), Rome, Italy, pages 371–384, 2013. Google ScholarDigital Library
- N. Glew. Object closure conversion. In Higher-Order Operational Techniques in Semantics (HOOTS ’99), Sept. 1999.Google Scholar
- R. Jagadeesan, C. Pitcher, J. Rathke, and J. Riely. Local memory via layout randomization. In Computer Security Foundations Symposium (CSF), pages 161–174, 2011. Google ScholarDigital Library
- A. Jeffrey. A fully abstract semantics for a concurrent functional language with monadic types. In IEEE Symposium on Logic in Computer Science (LICS), San Diego, California, 1995. Google ScholarDigital Library
- J. Kang, Y. Kim, C.-K. Hur, D. Dreyer, and V. Vafeiadis. Lightweight verification of separate compilation. In ACM Symposium on Principles of Programming Languages (POPL), St. Petersburg, Florida, pages 178–190. ACM, 2016. Google ScholarDigital Library
- A. Kennedy. Securing the .NET programming model. Theoretical Computer Science, 364(3):311–317, 2006. Google ScholarDigital Library
- J.-L. Krivine. Classical logic, storage operators and second-order lambda-calculus. Annals of Pure and Applied Logic, 68(1):53–78, 1994.Google ScholarCross Ref
- J. R. Longley. Universal types and what they are good for. In Domain theory, logic and computation, pages 25–63. Springer, 2003.Google Scholar
- J. Matthews and R. B. Findler. Operational semantics for multilanguage programs. In ACM Symposium on Principles of Programming Languages (POPL), Nice, France, pages 3–10, Jan. 2007. Google ScholarDigital Library
- A. Meyer and J. G. Riecke. Continuations may be unreasonable. In Conf. on LISP and functional programming, LFP ’88, pages 63–71, 1988. Google ScholarDigital Library
- Y. Minamide, G. Morrisett, and R. Harper. Typed closure conversion. In ACM Symposium on Principles of Programming Languages (POPL), St. Petersburg Beach, Florida, pages 271–283, Jan. 1996. 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 higherorder imperative language. In International Conference on Functional Programming (ICFP), Vancouver, British Columbia, Canada, Aug. 2015. Google ScholarDigital Library
- M. New, W. J. Bowman, and A. Ahmed. Fully abstract compilation via universal embeddding (technical appendix). July 2016.Google Scholar
- M. Patrignani, D. Clarke, and F. Piessens. Secure compilation of objectoriented components to protected module architectures. In Proceedings of the 11th Asian Symposium on Programming Languages and Systems (APLAS), Melbourne, Australia, Dec. 2013. Google ScholarDigital Library
- M. Patrignani, P. Agten, R. Strackx, B. Jacobs, D. Clarke, and F. Piessens. Secure compilation to protected module architectures. ACM Transactions on Programming Languages and Systems, 37(2): 6:1–6:50, Apr. 2015. Google ScholarDigital Library
- J. T. Perconti and A. Ahmed. Verifying an open compiler using multilanguage semantics. In European Symposium on Programming (ESOP), Apr. 2014. Google ScholarDigital Library
- A. M. Pitts and I. D. Stark. Operational reasoning for functions with local state. Higher order operational techniques in semantics, pages 227–273, 1998. Google ScholarDigital Library
- N. Ramsey. Embedding an interpreted language using higher-order functions and types. Journal of Functional Programming, 21(06): 585–615, 2011. Google ScholarDigital Library
- J. G. Riecke. Fully abstract translations between functional languages. In ACM Symposium on Principles of Programming Languages (POPL), Orlando, Florida, pages 245–254, 1991. Google ScholarDigital Library
- S. B. Sanjabi and C.-H. L. Ong. Fully abstract semantics of additive aspects by translation. In Proceedings of the 6th international conference on Aspect-oriented software development (AOSD), pages 135–148, 2007. Google ScholarDigital Library
- D. Scott. Data types as lattices. Siam Journal on computing, 5(3): 522–587, 1976.Google Scholar
- N. Shikuma and A. Igarashi. Proving noninterference by a fully complete translation to the simply typed λ-calculus. In Proceedings of the 11th Asian computing science conference on Advances in computer science: secure software and related issues, pages 301–315. Springer-Verlag, 2007. Google ScholarDigital Library
- N. Shikuma and A. Igarashi. Proving noninterference by a fully complete translation to the simply typed λ-calculus. Logical Methods in Computer Science, 4(3:10):1–31, 2008.Google Scholar
- G. Stewart, L. Beringer, S. Cuellar, and A. W. Appel. Compositional compcert. In ACM Symposium on Principles of Programming Languages (POPL), Mumbai, India, 2015. Google ScholarDigital Library
- S. Tse and S. Zdancewic. Translating dependency into parametricity. In International Conference on Functional Programming (ICFP), Snowbird, Utah, pages 115–125. ACM, 2004. Google ScholarDigital Library
- P. Wang, S. Cuellar, and A. Chlipala. Compiler verification meets cross-language linking via data abstraction. In ACM Symposium on Object Oriented Programming: Systems, Languages, and Applications (OOPSLA), Oct. 2014. Google ScholarDigital Library
Index Terms
- Fully abstract compilation via universal embedding
Recommendations
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: ...
Fully-abstract compilation by approximate back-translation
POPL '16A 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 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 ...
Comments