research-article

Open access

Reconciling optimization with secure compilation

Authors:

Arnaud De Grandmaison,

Christophe Guillon,

Karine HeydemannAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 5, Issue OOPSLA

Article No.: 142, Pages 1 - 30

https://doi.org/10.1145/3485519

Published: 15 October 2021 Publication History

Abstract

Software protections against side-channel and physical attacks are essential to the development of secure applications. Such protections are meaningful at machine code or micro-architectural level, but they typically do not carry observable semantics at source level. This renders them susceptible to miscompilation, and security engineers embed input/output side-effects to prevent optimizing compilers from altering them. Yet these side-effects are error-prone and compiler-dependent. The current practice involves analyzing the generated machine code to make sure security or privacy properties are still enforced. These side-effects may also be too expensive in fine-grained protections such as control-flow integrity. We introduce observations of the program state that are intrinsic to the correct execution of security protections, along with means to specify and preserve observations across the compilation flow. Such observations complement the input/output semantics-preservation contract of compilers. We introduce an opacification mechanism to preserve and enforce a partial ordering of observations. This approach is compatible with a production compiler and does not incur any modification to its optimization passes. We validate the effectiveness and performance of our approach on a range of benchmarks, expressing the secure compilation of these applications in terms of observations to be made at specific program points.

References

[1]

Martín Abadi. 1998. Protection in programming-language translations. In Automata, Languages and Programming (ICALP) (LNCS, Vol. 1443). Springer.

[2]

Martín Abadi, Mihai Budiu, Úlfar Erlingsson, and Jay Ligatti. 2005. Control-flow Integrity. In Proceedings of the 12th ACM Conference on Computer and Communications Security (CCS ’05). ACM, New York, NY, USA. 340–353. isbn:1-59593-226-7 https://doi.org/10.1145/1102120.1102165

Digital Library

[3]

Martín Abadi and Gordon D. Plotkin. 2012. On protection by layout randomization. ACM Trans. on Information System Security, 15, 2 (2012).

Digital Library

[4]

Carmine Abate, Roberto Blanco, Deepak Garg, Catalin Hritcu, Marco Patrignani, and Jérémy Thibault. 2018. Exploring Robust Property Preservation for Secure Compilation. CoRR, abs/1807.04603 (2018), arxiv:1807.04603. arxiv:1807.04603

[5]

Carmine Abate, Roberto Blanco, Deepak Garg, Catalin Hritcu, Marco Patrignani, and Jérémy Thibault. 2019. Journey Beyond Full Abstraction: Exploring Robust Property Preservation for Secure Compilation. In 32nd IEEE Computer Security Foundations Symposium, CSF 2019, Hoboken, NJ, USA, June 25-28, 2019. 256–271. https://doi.org/10.1109/CSF.2019.00025

[6]

2003. aiT. https://www.absint.com/ait/index.htm

[7]

Gogul Balakrishnan and Thomas Reps. 2010. WYSINWYX: What You See is Not What You eXecute. ACM Trans. Program. Lang. Syst., 32, 6 (2010), Article 23, Aug., 84 pages. issn:0164-0925 https://doi.org/10.1145/1749608.1749612

Digital Library

[8]

Clément Ballabriga, Hugues Cassé, Christine Rochange, and Pascal Sainrat. 2010. OTAWA: An Open Toolbox for Adaptive WCET Analysis. In Software Technologies for Embedded and Ubiquitous Systems, Sang Lyul Min, Robert Pettit, Peter Puschner, and Theo Ungerer (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 35–46. isbn:978-3-642-16256-5

Digital Library

[9]

Hagai Bar-El, Hamid Choukri, David Naccache, Michael Tunstall, and Claire Whelan. 2004. The Sorcerer’s Apprentice Guide to Fault Attacks. IACR Cryptology ePrint Archive, 2004 (2004), 100. http://dblp.uni-trier.de/db/journals/iacr/iacr2004.html##Bar-ElCNTW04

[10]

Thierno Barry, Damien Couroussé, and Bruno Robisson. 2016. Compilation of a Countermeasure Against Instruction-Skip Fault Attacks. In Proceedings of the Third Workshop on Cryptography and Security in Computing Systems (CS2 ’16). ACM, New York, NY, USA. 1–6. isbn:978-1-4503-4065-6 https://doi.org/10.1145/2858930.2858931

Digital Library

[11]

Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, and Alix Trieu. 2020. Formal verification of a constant-time preserving C compiler. Proc. ACM Program. Lang., 4, POPL (2020), 7:1–7:30. https://doi.org/10.1145/3371075

Digital Library

[12]

Patrick Baudin, Jean C. Filliâtre, Thierry Hubert, Claude Marché, Benjamin Monate, Yannick Moy, and Virgile Prevosto. 2008. ACSL: ANSI/ISO C Specification Language Version 1.4. https://frama-c.com/download/acsl.pdf

[13]

Ali Galip Bayrak, Francesco Regazzoni, David Novo, and Paolo Ienne. 2013. Sleuth: Automated Verification of Software Power Analysis Countermeasures. In Cryptographic Hardware and Embedded Systems - CHES 2013, Guido Bertoni and Jean-Sébastien Coron (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 293–310. isbn:978-3-642-40349-1

[14]

Pascal Berthomé, Karine Heydemann, Xavier Kauffmann-Tourkestansky, and Jean-François Lalande. 2012. High level model of control flow attacks for smart card functional security. In 7th International Conference on Availability, Reliability and Security. IEEE Computer Society, Prague, Czech Republic. 224–229. https://doi.org/10.1109/ARES.2012.79

Digital Library

[15]

Jean-Baptiste Bréjon, Karine Heydemann, Emmanuelle Encrenaz, Quentin Meunier, and Son Tuan Vu. 2019. Fault attack vulnerability assessment of binary code. In 6th Workshop on Cryptography and Security in Computing Systems (CS2). Valencia, Italy. isbn:978-1-4503-6182-8/19/01 https://doi.org/10.1145/3304080.3304083

Digital Library

[16]

Nathan Burow, Scott A. Carr, Joseph Nash, Per Larsen, Michael Franz, Stefan Brunthaler, and Mathias Payer. 2017. Control-Flow Integrity: Precision, Security, and Performance. ACM Comput. Surv., 50, 1 (2017), Article 16, April, 33 pages. issn:0360-0300 https://doi.org/10.1145/3054924

Digital Library

[17]

Adam Chlipala. 2007. A Certified Type-preserving Compiler from Lambda Calculus to Assembly Language. In Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’07). ACM, New York, NY, USA. 54–65. isbn:978-1-59593-633-2 https://doi.org/10.1145/1250734.1250742

Digital Library

[18]

Pascal Cuoq, Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, and Boris Yakobowski. 2012. Frama-C: A Software Analysis Perspective. In 10th International Conference on Software Engineering and Formal Methods. 233–247. isbn:978-3-642-33825-0 https://doi.org/10.1007/978-3-642-33826-7_16

Digital Library

[19]

Ron Cytron, Jeanne Ferrante, Barry K. Rosen, Mark N. Wegman, and F. Kenneth Zadeck. 1991. Efficiently Computing Static Single Assignment Form and the Control Dependence Graph. ACM Trans. Program. Lang. Syst., 13, 4 (1991), Oct., 451–490. issn:0164-0925 https://doi.org/10.1145/115372.115320

Digital Library

[20]

Dominique Devriese, Marco Patrignani, and Frank Piessens. 2016. Fully-Abstract Compilation by Approximate Back-Translation. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’16). Association for Computing Machinery, New York, NY, USA. 164–177. isbn:9781450335492 https://doi.org/10.1145/2837614.2837618

Digital Library

[21]

V. D’Silva, M. Payer, and D. Song. 2015. The Correctness-Security Gap in Compiler Optimization. In 2015 IEEE Security and Privacy Workshops. 73–87.

[22]

Louis Dureuil, Guillaume Petiot, Marie-Laure Potet, Thanh-Ha Le, Aude Crohen, and Philippe de Choudens. 2016. FISSC: A Fault Injection and Simulation Secure Collection. 3–11. isbn:978-3-319-45476-4 https://doi.org/10.1007/978-3-319-45477-1_1

[23]

DWARF. 2017. DWARF Debugging Information Format Version 5. https://dwarfstd.org/doc/DWARF5.pdf

[24]

Kerstin Eder, John P. Gallagher, Pedro López-García, Henk Muller, Zorana Banković, Kyriakos Georgiou, Rémy Haemmerlé, Manuel V. Hermenegildo, Bishoksan Kafle, Steve Kerrison, Maja Kirkeby, Maximiliano Klemen, Xueliang Li, Umer Liqat, Jeremy Morse, Morten Rhiger, and Mads Rosendahl. 2016. ENTRA. Microprocess. Microsyst., 47, PB (2016), Nov., 278–286. issn:0141-9331 https://doi.org/10.1016/j.micpro.2016.07.003

Digital Library

[25]

Hassan Eldib and Chao Wang. 2014. Synthesis of Masking Countermeasures Against Side Channel Attacks. In Proceedings of the 16th International Conference on Computer Aided Verification - Volume 8559. Springer-Verlag, Berlin, Heidelberg. 114–130. isbn:978-3-319-08866-2 https://doi.org/10.1007/978-3-319-08867-9_8

Digital Library

[26]

Eli Bendersky. 2011. pyelftools - Python library for parsing ELF files and DWARF debugging information. https://github.com/eliben/pyelftools

[27]

Daniele Gorla and Uwe Nestmann. 2016. Full abstraction for expressiveness: history, myths and facts. Mathematical Structures in Computer Science, 26, 4 (2016), 639–654. https://doi.org/10.1017/S0960129514000279

[28]

Christoph Herbst, Elisabeth Oswald, and Stefan Mangard. 2006. An AES Smart Card Implementation Resistant to Power Analysis Attacks. In Proceedings of the 4th International Conference on Applied Cryptography and Network Security (ACNS’06). Springer-Verlag, Berlin, Heidelberg. 239–252. isbn:3-540-34703-8, 978-3-540-34703-3 https://doi.org/10.1007/11767480_16

Digital Library

[29]

Christoph Hillebold. 2014. Compiler-Assisted Integrits against Fault injection Attacks. Master’s thesis. University of Technology, Graz. http://chille.at/articles/master-thesis

[30]

Yuval Ishai, Amit Sahai, and David Wagner. 2003. Private Circuits: Securing Hardware against Probing Attacks. In Advances in Cryptology - CRYPTO 2003, Dan Boneh (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 463–481. isbn:978-3-540-45146-4

[31]

ISO. 2011. C11 Standard. /bib/iso/C11/n1570.pdf ISO/IEC 9899:2011.

[32]

Jean-François Lalande, Karine Heydemann, and Pascal Berthomé. 2014. Software countermeasures for control flow integrity of smart card C codes. In ESORICS - 19th European Symposium on Research in Computer Security, Miroslaw Kutylowski and Jaideep Vaidya (Eds.) (Lecture Notes in Computer Science, Vol. 8713). Springer International Publishing, Wroclaw, Poland. 200–218. https://doi.org/10.1007/978-3-319-11212-1_12

Digital Library

[33]

Ilya Levin. 2007. A byte-oriented AES-256 implementation. http://www.literatecode.com/aes256

[34]

Hanbing Li, Isabelle Puaut, and Erven Rohou. 2014. Traceability of Flow Information: Reconciling Compiler Optimizations and WCET Estimation. In Proceedings of the 22Nd International Conference on Real-Time Networks and Systems (RTNS ’14). ACM, New York, NY, USA. Article 97, 10 pages. isbn:978-1-4503-2727-5 https://doi.org/10.1145/2659787.2659805

Digital Library

[35]

LLVM. 2019. LLVM Language Reference Manual. https://llvm.org/docs/LangRef.html#metadata

[36]

Nicolas Moro, Amine Dehbaoui, Karine Heydemann, Bruno Robisson, and Emmanuelle Encrenaz. 2013. Electromagnetic Fault Injection: Towards a Fault Model on a 32-bit Microcontroller. In 2013 Workshop on Fault Diagnosis and Tolerance in Cryptography. 77–88. https://doi.org/10.1109/FDTC.2013.9

Digital Library

[37]

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, 2 (2015), Article 6, April, 50 pages. issn:0164-0925 https://doi.org/10.1145/2699503

Digital Library

[38]

Paul Bakker, ARM. 2019. mbedTLS. tls.mbed.org

[39]

Colin Percival. 2014. How to zero a buffer. http://www.daemonology.net/blog/2014-09-04-how-to-zero-a-buffer.html

[40]

Julien Proy, Karine Heydemann, Alexandre Berzati, and Albert Cohen. 2017. Compiler-Assisted Loop Hardening Against Fault Attacks. ACM Trans. Archit. Code Optim., 14, 4 (2017), Article 36, Dec., 25 pages. issn:1544-3566 https://doi.org/10.1145/3141234

Digital Library

[41]

Manuel Rigger, Stefan Marr, Stephen Kell, David Leopoldseder, and Hanspeter Mössenböck. 2018. An Analysis of X86-64 Inline Assembly in C Programs. SIGPLAN Not., 53, 3 (2018), March, 84–99. issn:0362-1340 https://doi.org/10.1145/3296975.3186418

Digital Library

[42]

Matthieu Rivain and Emmanuel Prouff. 2010. Provably Secure Higher-Order Masking of AES. In Cryptographic Hardware and Embedded Systems, CHES 2010, Stefan Mangard and François-Xavier Standaert (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 413–427. isbn:978-3-642-15031-9

Digital Library

[43]

Bernhard Schommer, Christoph Cullmann, Gernot Gebhard, Xavier Leroy, Michael Schmidt, and Simon Wegener. 2018. Embedded Program Annotations for WCET Analysis. In WCET 2018: 18th International Workshop on Worst-Case Execution Time Analysis. 63, Dagstuhl Publishing, Barcelona, Spain. https://doi.org/10.4230/OASIcs.WCET.2018.8

[44]

Yan Shoshitaishvili, Ruoyu Wang, Christopher Salls, Nick Stephens, Mario Polino, Audrey Dutcher, John Grosen, Siji Feng, Christophe Hauser, Christopher Kruegel, and Giovanni Vigna. 2016. SoK: (State of) The Art of War: Offensive Techniques in Binary Analysis. In IEEE Symposium on Security and Privacy.

[45]

Laurent Simon, David Chisnall, and Ross Anderson. 2018. What You Get is What You C: Controlling Side Effects in Mainstream C Compilers. In 2018 IEEE European Symposium on Security and Privacy (EuroS&P). 1–15. https://doi.org/10.1109/EuroSP.2018.00009

[46]

Daan Sprenkels. 2020. Side-channel resistant values. http://lists.llvm.org/pipermail/llvm-dev/2019-September/135079.html

[47]

Richard M. Stallman and GCC DeveloperCommunity. 2009. Using The Gnu Compiler Collection: A Gnu Manual For Gcc Version 4.3.3. CreateSpace, Paramount, CA. isbn:144141276X, 9781441412768

Digital Library

[48]

The OpenSSL Project. 2003. OpenSSL: The Open Source toolkit for SSL/TLS. April, www.openssl.org

[49]

Son Tuan Vu, Karine Heydemann, Arnaud de Grandmaison, and Albert Cohen. 2020. Secure Delivery of Program Properties through Optimizing Compilation. In Proceedings of the 29th International Conference on Compiler Construction (CC 2020). Association for Computing Machinery, New York, NY, USA. 14–26. isbn:9781450371209 https://doi.org/10.1145/3377555.3377897

Digital Library

[50]

Marc Witteman. 2018. Secure Application Programming in the Presence of Side Channel Attacks.

[51]

Zhaomo Yang, Brian Johannesmeyer, Anders Trier Olesen, Sorin Lerner, and Kirill Levchenko. 2017. Dead Store Elimination (Still) Considered Harmful. In Proceedings of the 26th USENIX Conference on Security Symposium (SEC’17). USENIX Association, USA. 1025–1040. isbn:9781931971409

Digital Library

[52]

Yuval Yarom, Daniel Genkin, and Nadia Heninger. 2017. CacheBleed: a timing attack on OpenSSL constant-time RSA. Journal of Cryptographic Engineering, 7 (2017), 02, https://doi.org/10.1007/s13389-017-0152-y

[53]

Bilgiday Yuce, Patrick Schaumont, and Marc Witteman. 2018. Fault Attacks on Secure Embedded Software: Threats, Design, and Evaluation. Journal of Hardware and Systems Security, 2, 2 (2018), 01 Jun, 111–130. issn:2509-3436 https://doi.org/10.1007/s41635-018-0038-1

Cited By

van der Wall SMeyer R(2025)SNIP: Speculative Execution and Non-Interference Preservation for Compiler TransformationsProceedings of the ACM on Programming Languages10.1145/37048879:POPL(1506-1535)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704887
Tsoupidi RLozano RTroubitsyna EPapadimitratos P(2023)Securing Optimized Code Against Power Side Channels2023 IEEE 36th Computer Security Foundations Symposium (CSF)10.1109/CSF57540.2023.00016(340-355)Online publication date: Jul-2023
https://doi.org/10.1109/CSF57540.2023.00016
Tsoupidi RTroubitsyna EPapadimitratos P(2023)Thwarting code-reuse and side-channel attacks in embedded systemsComputers and Security10.1016/j.cose.2023.103405133:COnline publication date: 1-Oct-2023
https://dl.acm.org/doi/10.1016/j.cose.2023.103405

Index Terms

Reconciling optimization with secure compilation
1. Software and its engineering
  1. Software notations and tools
    1. Compilers

Recommendations

Secure delivery of program properties through optimizing compilation
CC 2020: Proceedings of the 29th International Conference on Compiler Construction

Annotations and assertions capturing static program properties are ubiquitous, from robust software engineering to safety-critical or secure code. These may be functional or non-functional properties of control and data flow, memory usage, I/O and real ...
Debugging native extensions of dynamic languages
ManLang '18: Proceedings of the 15th International Conference on Managed Languages & Runtimes

Many dynamic programming languages such as Ruby and Python enable developers to use so called native extensions, code implemented in typically statically compiled languages like C and C++. However, debuggers for these dynamic languages usually lack ...
Tapir: Embedding Fork-Join Parallelism into LLVM's Intermediate Representation
PPoPP '17: Proceedings of the 22nd ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming

This paper explores how fork-join parallelism, as supported by concurrency platforms such as Cilk and OpenMP, can be embedded into a compiler's intermediate representation (IR). Mainstream compilers typically treat parallel linguistic constructs as ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 5, Issue OOPSLA

October 2021

2001 pages

EISSN:2475-1421

DOI:10.1145/3492349

Issue’s Table of Contents

Copyright © 2021 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 15 October 2021

Published in PACMPL Volume 5, Issue OOPSLA

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
582
Total Downloads

Downloads (Last 12 months)266
Downloads (Last 6 weeks)25

Reflects downloads up to 01 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

van der Wall SMeyer R(2025)SNIP: Speculative Execution and Non-Interference Preservation for Compiler TransformationsProceedings of the ACM on Programming Languages10.1145/37048879:POPL(1506-1535)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704887
Tsoupidi RLozano RTroubitsyna EPapadimitratos P(2023)Securing Optimized Code Against Power Side Channels2023 IEEE 36th Computer Security Foundations Symposium (CSF)10.1109/CSF57540.2023.00016(340-355)Online publication date: Jul-2023
https://doi.org/10.1109/CSF57540.2023.00016
Tsoupidi RTroubitsyna EPapadimitratos P(2023)Thwarting code-reuse and side-channel attacks in embedded systemsComputers and Security10.1016/j.cose.2023.103405133:COnline publication date: 1-Oct-2023
https://dl.acm.org/doi/10.1016/j.cose.2023.103405

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Figures

Tables

Media

View Issue’s Table of Contents