{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,24]],"date-time":"2026-02-24T18:32:35Z","timestamp":1771957955637,"version":"3.50.1"},"reference-count":53,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2021,10,15]],"date-time":"2021-10-15T00:00:00Z","timestamp":1634256000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2021,10,20]]},"abstract":"<jats:p>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.<\/jats:p>","DOI":"10.1145\/3485519","type":"journal-article","created":{"date-parts":[[2021,10,15]],"date-time":"2021-10-15T19:18:28Z","timestamp":1634325508000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Reconciling optimization with secure compilation"],"prefix":"10.1145","volume":"5","author":[{"given":"Son Tuan","family":"Vu","sequence":"first","affiliation":[{"name":"Sorbonne University, France \/ CNRS, France \/ LIP6, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8866-5343","authenticated-orcid":false,"given":"Albert","family":"Cohen","sequence":"additional","affiliation":[{"name":"Google, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arnaud","family":"De Grandmaison","sequence":"additional","affiliation":[{"name":"ARM, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christophe","family":"Guillon","sequence":"additional","affiliation":[{"name":"STMicroelectronics, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Karine","family":"Heydemann","sequence":"additional","affiliation":[{"name":"Sorbonne University, France \/ CNRS, France \/ LIP6, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2021,10,15]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Languages and Programming (ICALP) (LNCS","author":"Abadi Mart\u00edn","year":"1998","unstructured":"Mart\u00edn Abadi . 1998 . Protection in programming-language translations. In Automata , Languages and Programming (ICALP) (LNCS , Vol. 1443). Springer. Mart\u00edn Abadi. 1998. Protection in programming-language translations. In Automata, Languages and Programming (ICALP) (LNCS, Vol. 1443). Springer."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1102120.1102165"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2240276.2240279"},{"key":"e_1_2_1_4_1","volume-title":"Exploring Robust Property Preservation for Secure Compilation. CoRR, abs\/1807.04603","author":"Abate Carmine","year":"2018","unstructured":"Carmine Abate , Roberto Blanco , Deepak Garg , Catalin Hritcu , Marco Patrignani , and J\u00e9r\u00e9my Thibault . 2018. Exploring Robust Property Preservation for Secure Compilation. CoRR, abs\/1807.04603 ( 2018 ), arxiv:1807.04603. arxiv:1807.04603 Carmine Abate, Roberto Blanco, Deepak Garg, Catalin Hritcu, Marco Patrignani, and J\u00e9r\u00e9my Thibault. 2018. Exploring Robust Property Preservation for Secure Compilation. CoRR, abs\/1807.04603 (2018), arxiv:1807.04603. arxiv:1807.04603"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2019.00025"},{"key":"e_1_2_1_6_1","unstructured":"2003. aiT. https:\/\/www.absint.com\/ait\/index.htm  2003. aiT. https:\/\/www.absint.com\/ait\/index.htm"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1749608.1749612"},{"key":"e_1_2_1_8_1","volume-title":"OTAWA: An Open Toolbox for Adaptive WCET Analysis. In Software Technologies for Embedded and Ubiquitous Systems","author":"Ballabriga Cl\u00e9ment","year":"2010","unstructured":"Cl\u00e9ment Ballabriga , Hugues Cass\u00e9 , 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\u201346. isbn:978-3-642-16256-5 Cl\u00e9ment Ballabriga, Hugues Cass\u00e9, 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\u201346. isbn:978-3-642-16256-5"},{"key":"e_1_2_1_9_1","first-page":"100","article-title":"The Sorcerer\u2019s Apprentice Guide to Fault Attacks","volume":"2004","author":"Bar-El Hagai","year":"2004","unstructured":"Hagai Bar-El , Hamid Choukri , David Naccache , Michael Tunstall , and Claire Whelan . 2004 . The Sorcerer\u2019s Apprentice Guide to Fault Attacks .. IACR Cryptology ePrint Archive , 2004 (2004), 100 . http:\/\/dblp.uni-trier.de\/db\/journals\/iacr\/iacr2004.html##Bar-ElCNTW04 Hagai Bar-El, Hamid Choukri, David Naccache, Michael Tunstall, and Claire Whelan. 2004. The Sorcerer\u2019s Apprentice Guide to Fault Attacks.. IACR Cryptology ePrint Archive, 2004 (2004), 100. http:\/\/dblp.uni-trier.de\/db\/journals\/iacr\/iacr2004.html##Bar-ElCNTW04","journal-title":"IACR Cryptology ePrint Archive"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2858930.2858931"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371075"},{"key":"e_1_2_1_12_1","volume-title":"ACSL: ANSI\/ISO C Specification Language Version 1.4. https:\/\/frama-c.com\/download\/acsl.pdf","author":"Baudin Patrick","year":"2008","unstructured":"Patrick Baudin , Jean C. Filli\u00e2tre , Thierry Hubert , Claude March\u00e9 , Benjamin Monate , Yannick Moy , and Virgile Prevosto . 2008 . ACSL: ANSI\/ISO C Specification Language Version 1.4. https:\/\/frama-c.com\/download\/acsl.pdf Patrick Baudin, Jean C. Filli\u00e2tre, Thierry Hubert, Claude March\u00e9, Benjamin Monate, Yannick Moy, and Virgile Prevosto. 2008. ACSL: ANSI\/ISO C Specification Language Version 1.4. https:\/\/frama-c.com\/download\/acsl.pdf"},{"key":"e_1_2_1_13_1","volume-title":"Sleuth: Automated Verification of Software Power Analysis Countermeasures. In Cryptographic Hardware and Embedded Systems - CHES","author":"Bayrak Ali Galip","year":"2013","unstructured":"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\u00e9bastien Coron (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg. 293\u2013310. isbn:978-3-642-40349-1 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\u00e9bastien Coron (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 293\u2013310. isbn:978-3-642-40349-1"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/ARES.2012.79"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3304080.3304083"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3054924"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250742"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33826-7_16"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/115372.115320"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837618"},{"key":"e_1_2_1_21_1","volume-title":"The Correctness-Security Gap in Compiler Optimization. In 2015 IEEE Security and Privacy Workshops. 73\u201387","author":"D\u2019Silva V.","unstructured":"V. D\u2019Silva , M. Payer , and D. Song . 2015 . The Correctness-Security Gap in Compiler Optimization. In 2015 IEEE Security and Privacy Workshops. 73\u201387 . V. D\u2019Silva, M. Payer, and D. Song. 2015. The Correctness-Security Gap in Compiler Optimization. In 2015 IEEE Security and Privacy Workshops. 73\u201387."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-45477-1_1"},{"key":"e_1_2_1_23_1","unstructured":"DWARF. 2017. DWARF Debugging Information Format Version 5. https:\/\/dwarfstd.org\/doc\/DWARF5.pdf  DWARF. 2017. DWARF Debugging Information Format Version 5. https:\/\/dwarfstd.org\/doc\/DWARF5.pdf"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.micpro.2016.07.003"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_8"},{"key":"e_1_2_1_26_1","unstructured":"Eli Bendersky. 2011. pyelftools - Python library for parsing ELF files and DWARF debugging information. https:\/\/github.com\/eliben\/pyelftools  Eli Bendersky. 2011. pyelftools - Python library for parsing ELF files and DWARF debugging information. https:\/\/github.com\/eliben\/pyelftools"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000279"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/11767480_16"},{"key":"e_1_2_1_29_1","volume-title":"Compiler-Assisted Integrits against Fault injection Attacks. Master\u2019s thesis","author":"Hillebold Christoph","unstructured":"Christoph Hillebold . 2014. Compiler-Assisted Integrits against Fault injection Attacks. Master\u2019s thesis . University of Technology , Graz. http:\/\/chille.at\/articles\/master-thesis Christoph Hillebold. 2014. Compiler-Assisted Integrits against Fault injection Attacks. Master\u2019s thesis. University of Technology, Graz. http:\/\/chille.at\/articles\/master-thesis"},{"key":"e_1_2_1_30_1","volume-title":"Private Circuits: Securing Hardware against Probing Attacks. In Advances in Cryptology - CRYPTO","author":"Ishai Yuval","year":"2003","unstructured":"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\u2013481. isbn:978-3-540-45146-4 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\u2013481. isbn:978-3-540-45146-4"},{"key":"e_1_2_1_31_1","unstructured":"ISO. 2011. C11 Standard. \/bib\/iso\/C11\/n1570.pdf ISO\/IEC 9899:2011.  ISO. 2011. C11 Standard. \/bib\/iso\/C11\/n1570.pdf ISO\/IEC 9899:2011."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11212-1_12"},{"key":"e_1_2_1_33_1","unstructured":"Ilya Levin. 2007. A byte-oriented AES-256 implementation. http:\/\/www.literatecode.com\/aes256  Ilya Levin. 2007. A byte-oriented AES-256 implementation. http:\/\/www.literatecode.com\/aes256"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2659787.2659805"},{"key":"e_1_2_1_35_1","unstructured":"LLVM. 2019. LLVM Language Reference Manual. https:\/\/llvm.org\/docs\/LangRef.html#metadata  LLVM. 2019. LLVM Language Reference Manual. https:\/\/llvm.org\/docs\/LangRef.html#metadata"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/FDTC.2013.9"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2699503"},{"key":"e_1_2_1_38_1","unstructured":"Paul Bakker ARM. 2019. mbedTLS. tls.mbed.org  Paul Bakker ARM. 2019. mbedTLS. tls.mbed.org"},{"key":"e_1_2_1_39_1","unstructured":"Colin Percival. 2014. How to zero a buffer. http:\/\/www.daemonology.net\/blog\/2014-09-04-how-to-zero-a-buffer.html  Colin Percival. 2014. How to zero a buffer. http:\/\/www.daemonology.net\/blog\/2014-09-04-how-to-zero-a-buffer.html"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3141234"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3296975.3186418"},{"key":"e_1_2_1_42_1","volume-title":"CHES","author":"Rivain Matthieu","year":"2010","unstructured":"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\u00e7ois-Xavier Standaert (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 413\u2013427. isbn:978-3-642-15031-9 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\u00e7ois-Xavier Standaert (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 413\u2013427. isbn:978-3-642-15031-9"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.4230\/OASIcs.WCET.2018.8"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2016.17"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP.2018.00009"},{"key":"e_1_2_1_46_1","unstructured":"Daan Sprenkels. 2020. Side-channel resistant values. http:\/\/lists.llvm.org\/pipermail\/llvm-dev\/2019-September\/135079.html  Daan Sprenkels. 2020. Side-channel resistant values. http:\/\/lists.llvm.org\/pipermail\/llvm-dev\/2019-September\/135079.html"},{"issue":"3","key":"e_1_2_1_47_1","first-page":"3","article-title":"Using The Gnu Compiler Collection","volume":"4","author":"Stallman Richard M.","year":"2009","unstructured":"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 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","journal-title":"A Gnu Manual For Gcc Version"},{"key":"e_1_2_1_48_1","unstructured":"The OpenSSL Project. 2003. OpenSSL: The Open Source toolkit for SSL\/TLS. April www.openssl.org  The OpenSSL Project. 2003. OpenSSL: The Open Source toolkit for SSL\/TLS. April www.openssl.org"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3377555.3377897"},{"key":"e_1_2_1_50_1","unstructured":"Marc Witteman. 2018. Secure Application Programming in the Presence of Side Channel Attacks.  Marc Witteman. 2018. Secure Application Programming in the Presence of Side Channel Attacks."},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.5555\/3241189.3241269"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/s13389-017-0152-y"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/s41635-018-0038-1"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3485519","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3485519","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:18:40Z","timestamp":1750191520000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3485519"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,10,15]]},"references-count":53,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2021,10,20]]}},"alternative-id":["10.1145\/3485519"],"URL":"https:\/\/doi.org\/10.1145\/3485519","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,10,15]]},"assertion":[{"value":"2021-10-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}