Marco Patrignani
Skip Abstract Section
Abstract
A fully abstract compiler prevents security features of the source language from being bypassed by an attacker operating at the target language level. Unfortunately, developing fully abstract compilers is very complex, and it is even more so when the target language is an untyped assembly language. To provide a fully abstract compiler that targets untyped assembly, it has been suggested to extend the target language with a protected module architecture—an assembly-level isolation mechanism which can be found in next-generation processors. This article provides a fully abstract compilation scheme whose source language is an object-oriented, high-level language and whose target language is such an extended assembly language. The source language enjoys features such as dynamic memory allocation and exceptions. Secure compilation of first-order method references, cross-package inheritance, and inner classes is also presented. Moreover, this article contains the formal proof of full abstraction of the compilation scheme. Measurements of the overhead introduced by the compilation scheme indicate that it is negligible.
- Martín Abadi. 1999. Protection in programming-language translations. In Secure Internet Programming. Springer-Verlag, London, UK, 19--34. Google Scholar
Digital Library
- Martín Abadi and Gordon D. Plotkin. 2012. On protection by layout randomization. ACM Trans. Inf. Syst. Secur. 15, 2, Article 8 (July 2012), 29 pages. DOI:http://dx.doi.org/10.1145/2240276.2240279 Google ScholarDigital Library
- Saleh E. Abdullahi and Graem A. Ringwood. 1998. Garbage collecting the internet: A survey of distributed garbage collection. ACM Comput. Surv. 30, 3 (Sept. 1998), 330--373. DOI:http://dx.doi.org/10.1145/292469.292471 Google ScholarDigital Library
- Pieter Agten, Bart Jacobs, and Frank Piessens. 2015. Sound modular verification of C code executing in an unverified context. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’15). Google ScholarDigital Library
- Pieter Agten, Raoul Strackx, Bart Jacobs, and Frank Piessens. 2012. Secure compilation to modern processors. In Proceedings of the 2012 IEEE 25th Computer Security Foundations Symposium (CSF’12). IEEE Computer Society, Washington, DC, Article 12, 15 pages. DOI:http://dx.doi.org/10.1109/CSF.2012.12 Google ScholarDigital Library
- Amal Ahmed and Matthias Blume. 2011. An equivalence-preserving CPS translation via multi-language semantics. SIGPLAN Not. 46, 9, Article 30 (Sept. 2011), 14 pages. DOI:http://dx.doi.org/10.1145/2034574.2034830 Google ScholarDigital Library
- Ittai Anati, Shay Gueron, S. Johnson, and V. Scarlata. 2013. Innovative technology for CPU based attestation and sealing. In Proceedings of the 2nd International Workshop on Hardware and Architectural Support for Security and Privacy (HASP’13), Vol. 13.Google Scholar
- Niels Avonds, Raoul Strackx, Pieter Agten, and Frank Piessens. 2013. Salus: Non-hierarchical memory access rights to enforce the principle of least privilege. In Security and Privacy in Communication Networks (SecureComm’13).Google Scholar
- Adam Chlipala. 2007. A certified type-preserving compiler from lambda calculus to assembly language. SIGPLAN Not. 42, 6, Article 5 (June 2007), 12 pages. DOI:http://dx.doi.org/10.1145/1273442.1250742 Google ScholarDigital Library
- Pierre-Louis Curien. 2007. Definability and full abstraction. Electron. Notes Theor. Comput. Sci. 172 (April 2007), 301--310. DOI:http://dx.doi.org/10.1016/j.entcs.2007.02.011 Google ScholarDigital Library
- Frank S. de Boer, Marcello M. Bonsangue, Martin Steffen, and Erika ÁbrahÁm. 2005. A fully abstract semantics for UML components. In Proceedings of the 3rd International Conference on Formal Methods for Components and Objects (FMCO’04). Springer-Verlag, Berlin, 49--69. DOI:http://dx.doi.org/10.1007/11561163_3 Google ScholarDigital Library
- Roland Ducournau. 2011. Implementing statically typed object-oriented programming languages. ACM Comput. Surv. 43, 3, Article 18 (April 2011), 48 pages. DOI:http://dx.doi.org/10.1145/1922649.1922655 Google ScholarDigital Library
- Karim Eldefrawy, Aurélien Francillon, Daniele Perito, and Gene Tsudik. 2012. SMART: Secure and minimal architecture for (establishing a dynamic) root of trust. In Proceedings of the 19th Annual Network and Distributed System Security Symposium (NDSS’12).Google Scholar
- Ulfar Erlingsson, Yves Younan, and Frank Piessens. 2010. Low-level software security by example. In Handbook of Information and Communication Security. Springer, Berlin, 663--658.Google Scholar
- David Flanagan. 1998. Java in a Nutshell. Deutsche Ausgabe der 2. A. O’Reilly.Google Scholar
- Cedric Fournet, Nikhil Swamy, Juan Chen, Pierre-Evariste Dagand, Pierre-Yves Strub, and Benjamin Livshits. 2013. Fully abstract compilation to JavaScript. SIGPLAN Not. 48, 1, Article 26 (Jan. 2013), 14 pages. DOI:http://dx.doi.org/10.1145/2480359.2429114 Google ScholarDigital Library
- J. A. Halderman, S. D. Schoen, N. Heninger, W. Clarkson, W. Paul, J. A. Calandrino, A. J. Feldman, J. Appelbaum, and E. W. Felten. 2008. Lest we remember: Cold boot attacks on encryption keys. In Proceedings of the USENIX Security Symposium. 45--60. Google ScholarDigital Library
- Matthew Hoekstra, Reshma Lal, Pradeep Pappachan, Vinay Phegade, and Juan Del Cuvillo. 2013. Using innovative instructions to create trustworthy software solutions. In Proceedings of the 2nd International Workshop on Hardware and Architectural Support for Security and Privacy. ACM, 11. Retrieved from Google ScholarDigital Library
- Andrei Homescu, Steven Neisius, Per Larsen, Stefan Brunthaler, and Michael Franz. 2013. Profile-guided automated software diversity. In Proceedings of the 2013 IEEE/ACM International Symposium on Code Generation and Optimization (CGO’13). IEEE Computer Society, Washington, DC, 1--11. DOI:http://dx.doi.org/10.1109/CGO.2013.6494997 Google ScholarDigital Library
- Intel Corporation. 2013. Software Guard Extensions Programming Reference. Retrieved from http://software.intel.com/sites/default/files/329298-001.pdf.Google Scholar
- Radha Jagadeesan, Corin Pitcher, Julian Rathke, and James Riely. 2011. Local memory via layout randomization. In Proceedings of the 2011 IEEE 24th Computer Security Foundations Symposium (CSF’11). IEEE Computer Society, Washington, DC, 161--174. DOI:http://dx.doi.org/10.1109/CSF.2011.18 Google ScholarDigital Library
- Alan Jeffrey and Julian Rathke. 2005a. A fully abstract may testing semantics for concurrent objects. Theor. Comput. Sci. 338, 1--3 (June 2005), 17--63. DOI:http://dx.doi.org/10.1016/j.tcs.2004.10.012 Google ScholarDigital Library
- Alan Jeffrey and Julian Rathke. 2005b. Java Jr.: Fully abstract trace semantics for a core Java language. In ESOP’05 (LNCS), Vol. 3444. Springer, 423--438. DOI:http://dx.doi.org/10.1007/978-3-540-31987-0_29 Google ScholarCross Ref
- Andrew Kennedy. 2006. Securing the .NET programming model. Theor. Comput. Sci. 364, 3 (Nov. 2006), 311--317. DOI:http://dx.doi.org/10.1016/j.tcs.2006.08.014 Google ScholarDigital Library
- Per Larsen, Stefan Brunthaler, and Michael Franz. 2014. Security through diversity: Are we there yet? IEEE Security & Privacy 12, 2 (2014), 28--35. DOI:http://dx.doi.org/10.1109/MSP.2013.129Google ScholarCross Ref
- Chris Lattner and Vikram Adve. 2004. LLVM: A compilation framework for lifelong program analysis & transformation. In Proceedings of the 2004 International Symposium on Code Generation and Optimization (CGO’’04). Google ScholarDigital Library
- Xavier Leroy. 2009. A formally verified compiler back-end. J. Autom. Reason. 43, 4 (Dec. 2009), 363--446. DOI:http://dx.doi.org/10.1007/s10817-009-9155-4 Google ScholarDigital Library
- Jonathan M. McCune, Yanlin Li, Ning Qu, Zongwei Zhou, Anupam Datta, Virgil Gligor, and Adrian Perrig. 2010. TrustVisor: Efficient TCB reduction and attestation. In SP’10. IEEE, Washington, DC, 143--158. DOI:http://dx.doi.org/10.1109/SP.2010.17 Google ScholarDigital Library
- Jonathan M. McCune, Bryan J. Parno, Adrian Perrig, Michael K. Reiter, and Hiroshi Isozaki. 2008. Flicker: An execution infrastructure for TCB minimization. SIGOPS Oper. Syst. Rev. 42, 4, Article 24 (April 2008), 14 pages. DOI:http://dx.doi.org/10.1145/1357010.1352625 Google ScholarDigital Library
- Frank McKeen, Ilya Alexandrovich, Alex Berenzon, Carlos V. Rozas, Hisham Shafi, Vedvyas Shanbhogue, and Uday R. Savagaonkar. 2013. Innovative instructions and software model for isolated execution. In HASP’13. ACM, Article 10, 1 pages. DOI:http://dx.doi.org/10.1145/2487726.2488368 Google ScholarDigital Library
- Greg Morrisett, David Walker, Karl Crary, and Neal Glew. 1999. From system f to typed assembly language. ACM Trans. Program. Lang. Syst. 21, 3 (May 1999), 527--568. DOI:http://dx.doi.org/10.1145/319301.319345 Google ScholarDigital Library
- Job Noorman, Pieter Agten, Wilfried Daniels, Raoul Strackx, Anthony Van Herrewege, Christophe Huygens, Bart Preneel, Ingrid Verbauwhede, and Frank Piessens. 2013. Sancus: Low-cost trustworthy extensible networked devices with a zero-software Trusted Computing Base. In Proceedings of the 22nd USENIX Conference on Security Symposium. USENIX Association. Google ScholarDigital Library
- Marco Patrignani and Dave Clarke. 2014. Fully abstract trace semantics of low-level isolation mechanisms. In Proceedings of the 29th Annual ACM Symposium on Applied Computing (SAC’14). Google ScholarDigital Library
- Marco Patrignani, Dave Clarke, and Frank Piessens. 2013. Secure compilation of object-oriented components to protected module architectures. In APLAS’13 (LNCS), Vol. 8301. 176--191. Google ScholarDigital Library
- Gordon D. Plotkin. 1977. LCF considered as a programming language. Theoretical Computer Science 5 (1977), 223--255.Google ScholarCross Ref
- Ryan Roemer, Erik Buchanan, Hovav Shacham, and Stefan Savage. 2012. Return-oriented programming: Systems, languages, and applications. ACM Trans. Inf. Syst. Secur. 15, 1, Article 2 (March 2012), 34 pages. DOI:http://dx.doi.org/10.1145/2133375.2133377 Google ScholarDigital Library
- Hovav Shacham, Matthew Page, Ben Pfaff, Eu-Jin Goh, Nagendra Modadugu, and Dan Boneh. 2004. On the effectiveness of address-space randomization. In Proceedings of the 11th ACM Conference on Computer and Communications Security (CCS’04). ACM, New York, NY, 298--307. DOI:http://dx.doi.org/10.1145/1030083.1030124 Google ScholarDigital Library
- Lenin Singaravelu, Calton Pu, Hermann Härtig, and Christian Helmuth. 2006. Reducing TCB complexity for security-sensitive applications: Three case studies. SIGOPS Oper. Syst. Rev. 40, 4, Article 13 (April 2006), 14 pages. DOI:http://dx.doi.org/10.1145/1218063.1217951 Google ScholarDigital Library
- Raoul Strackx, Job Noorman, Ingrid Verbauwhede, Bart Preneel, and Frank Piessens. 2013. Protected software module architectures. In Proceedings of the ISSE 2013 Securing Electronic Business Processes, Helmut Reimer, Norbert Pohlmann, and Wolfgang Schneider (Eds.). Springer, 241--251. DOI:http://dx.doi.org/10.1007/978-3-658-03371-2_21Google ScholarCross Ref
- Raoul Strackx and Frank Piessens. 2012. Fides: Selectively hardening software application components against kernel-level or process-level Malware. In Proceedings of the 2012 ACM conference on Computer and Communications Security (CCS’12). ACM, New York, NY, 2--13. DOI:http://dx.doi.org/10.1145/2382196.2382200 Google ScholarDigital Library
- Raoul Strackx, Frank Piessens, and Bart Preneel. 2010. Efficient isolation of trusted subsystems in embedded systems. In SecureComm. 344--361.Google Scholar
- Raoul Strackx, Yves Younan, Pieter Philippaerts, Frank Piessens, Sven Lachmund, and Thomas Walter. 2009. Breaking the memory secrecy assumption. In Proceedings of the 2nd European Workshop on System Security (EUROSEC’09). ACM, New York, NY. DOI:http://dx.doi.org/10.1145/1519144.1519145 Google ScholarDigital Library
- Marko van Dooren, Dave Clarke, and Bart Jacobs. 2013. Subobject-oriented programming. In Formal Methods for Components and Objects (Lecture Notes in Computer Science), Vol. 7866. Springer, Berlin, 38--82. DOI:http://dx.doi.org/10.1007/978-3-642-40615-7_2Google ScholarCross Ref
- Amit Vasudevan, Sagar Chaki, Limin Jia, Jonathan McCune, James Newsome, and Anupam Datta. 2013. Design, implementation and verification of an extensible and modular hypervisor framework. In Proceedings of the 2013 IEEE Symposium on Security and Privacy (SP’13). IEEE Computer Society, Washington, DC, 430--444. DOI:http://dx.doi.org/10.1109/SP.2013.36 Google ScholarDigital Library
- Richard Wartell, Vishwath Mohan, Kevin W. Hamlen, and Zhiqiang Lin. 2012. Binary stirring: Self-randomizing instruction addresses of legacy x86 binary code. In Proceedings of the 2012 ACM Conference on Computer and Communications Security (CCS’12). ACM, New York, NY, 157--168. DOI:http://dx.doi.org/10.1145/2382196.2382216 Google ScholarDigital Library
- Johannes Winter and Kurt Dietrich. 2012. A hijacker’s guide to the LPC bus., In Proceedings of the 8th European conference on Public Key Infrastructures, Services, and Applications (EuroPKI’11). 176--193. Google ScholarDigital Library
- Emmett Witchel, Josh Cates, and Krste Asanović. 2002. Mondrian memory protection. SIGPLAN Not. 37, 10 (Oct. 2002), 304--316. DOI:http://dx.doi.org/10.1145/605432.605429 Google ScholarDigital Library
- Yves Younan. 2008. Efficient Countermeasures for Software Vulnerabilities due to Memory Management Errors. Ph.D. Dissertation. Informatics Section, Department of Computer Science, Faculty of Engineering Science.Google Scholar
- Yves Younan, Wouter Joosen, and Frank Piessens. 2012. Runtime countermeasures for code injection attacks against C and C++ programs. Comput. Surveys 44, 3 (2012), 17:1--17:28. Google ScholarDigital Library
Index Terms
- Secure Compilation to Protected Module Architectures
Recommendations
Robustly Safe Compilation, an Efficient Form of Secure Compilation
Security-preserving compilers generate compiled code that withstands target-level attacks such as alteration of control flow, data leaks, or memory corruption. Many existing security-preserving compilers are proven to be fully abstract, meaning that they ...
Formal Approaches to Secure Compilation: A Survey of Fully Abstract Compilation and Related Work
Secure compilation is a discipline aimed at developing compilers that preserve the security properties of the source programs they take as input in the target programs they produce as output. This discipline is broad in scope, targeting languages with a ...
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: ...
Comments