{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:42:29Z","timestamp":1780994549803,"version":"3.54.1"},"reference-count":60,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T00:00:00Z","timestamp":1576800000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100010663","name":"H2020 European Research Council","doi-asserted-by":"publisher","award":["772568"],"award-info":[{"award-number":["772568"]}],"id":[{"id":"10.13039\/100010663","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100007297","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N00014-12-1-0914, N00014-15-1-2750, N00014-19-1-2292"],"award-info":[{"award-number":["N00014-12-1-0914, N00014-15-1-2750, N00014-19-1-2292"]}],"id":[{"id":"10.13039\/100007297","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100008394","name":"Natur og Univers, Det Frie Forskningsr\u00e5d","doi-asserted-by":"crossref","award":["6108-00363"],"award-info":[{"award-number":["6108-00363"]}],"id":[{"id":"10.13039\/100008394","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2020,1]]},"abstract":"<jats:p>Timing side-channels are arguably one of the main sources of vulnerabilities in cryptographic implementations. One effective mitigation against timing side-channels is to write programs that do not perform secret-dependent branches and memory accesses. This mitigation, known as \"cryptographic constant-time\", is adopted by several popular cryptographic libraries.<\/jats:p>\n          <jats:p>This paper focuses on compilation of cryptographic constant-time programs, and more specifically on the following question: is the code generated by a realistic compiler for a constant-time source program itself provably constant-time? Surprisingly, we answer the question positively for a mildly modified version of the CompCert compiler, a formally verified and moderately optimizing compiler for C. Concretely, we modify the CompCert compiler to eliminate sources of potential leakage. Then, we instrument the operational semantics of CompCert intermediate languages so as to be able to capture cryptographic constant-time. Finally, we prove that the modified CompCert compiler preserves constant-time. Our mechanization maximizes reuse of the CompCert correctness proof, through the use of new proof techniques for proving preservation of constant-time. These techniques achieve complementary trade-offs between generality and tractability of proof effort, and are of independent interest.<\/jats:p>","DOI":"10.1145\/3371075","type":"journal-article","created":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T19:45:25Z","timestamp":1576871125000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":49,"title":["Formal verification of a constant-time preserving C compiler"],"prefix":"10.1145","volume":"4","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[{"name":"MPI for Security and Privacy, Germany \/ IMDEA Software Institute, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sandrine","family":"Blazy","sequence":"additional","affiliation":[{"name":"University of Rennes, France \/ Inria, France \/ CNRS, France \/ IRISA, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Benjamin","family":"Gr\u00e9goire","sequence":"additional","affiliation":[{"name":"Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"R\u00e9mi","family":"Hutin","sequence":"additional","affiliation":[{"name":"University of Rennes, France \/ Inria, France \/ CNRS, France \/ IRISA, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Vincent","family":"Laporte","sequence":"additional","affiliation":[{"name":"Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"David","family":"Pichardie","sequence":"additional","affiliation":[{"name":"University of Rennes, France \/ Inria, France \/ CNRS, France \/ IRISA, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alix","family":"Trieu","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,12,20]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"Computer Security Foundations","author":"Abate Carmine","year":"2019","unstructured":"Carmine Abate , Roberto Blanco , Deepak Garg , Catalin Hritcu , Marco Patrignani , and J\u00e9r\u00e9my Thibault . 2018. Exploring Robust Property Preservation for Secure Compilation . In Computer Security Foundations 2019 . http:\/\/arxiv.org\/abs\/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. In Computer Security Foundations 2019. http:\/\/arxiv.org\/abs\/1807.04603"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49890-3_24"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.42"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134078"},{"key":"e_1_2_2_5_1","volume-title":"Verifying Constant-Time Implementations. In 25th USENIX Security Symposium, USENIX Security 16","author":"Almeida Jos\u00e9 Bacelar","year":"2016","unstructured":"Jos\u00e9 Bacelar Almeida , Manuel Barbosa , Gilles Barthe , Fran\u00e7ois Dupressoir , and Michael Emmi . 2016 . Verifying Constant-Time Implementations. In 25th USENIX Security Symposium, USENIX Security 16 . Jos\u00e9 Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Fran\u00e7ois Dupressoir, and Michael Emmi. 2016. Verifying Constant-Time Implementations. In 25th USENIX Security Symposium, USENIX Security 16."},{"key":"e_1_2_2_6_1","volume-title":"The Last Mile: High-Assurance and High-Speed Cryptographic Implementations. CoRR abs\/1904.04606","author":"Almeida Jos\u00e9 Bacelar","year":"2019","unstructured":"Jos\u00e9 Bacelar Almeida , Manuel Barbosa , Gilles Barthe , Benjamin Gr\u00e9goire , Adrien Koutsos , Vincent Laporte , Tiago Oliveira , and Pierre-Yves Strub . 2019. The Last Mile: High-Assurance and High-Speed Cryptographic Implementations. CoRR abs\/1904.04606 ( 2019 ). arXiv: 1904.04606 http:\/\/arxiv.org\/abs\/1904.04606 Jos\u00e9 Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Gr\u00e9goire, Adrien Koutsos, Vincent Laporte, Tiago Oliveira, and Pierre-Yves Strub. 2019. The Last Mile: High-Assurance and High-Speed Cryptographic Implementations. CoRR abs\/1904.04606 (2019). arXiv: 1904.04606 http:\/\/arxiv.org\/abs\/1904.04606"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2015.44"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243766"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19718-5_1"},{"key":"e_1_2_2_10_1","volume-title":"Program Logics - for Certified Compilers","author":"Appel Andrew W.","unstructured":"Andrew W. Appel . 2014. Program Logics - for Certified Compilers . Cambridge University Press . http: \/\/www.cambridge.org\/de\/academic\/subjects\/computer- science\/programming- languages- and- applied- logic\/programlogics- certified- compilers?format=HB Andrew W. Appel. 2014. Program Logics - for Certified Compilers. Cambridge University Press. http: \/\/www.cambridge.org\/de\/academic\/subjects\/computer- science\/programming- languages- and- applied- logic\/programlogics- certified- compilers?format=HB"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2701415"},{"key":"e_1_2_2_12_1","unstructured":"ARM. 2016. mbed TLS. https:\/\/tls.mbed.org\/  ARM. 2016. mbed TLS. https:\/\/tls.mbed.org\/"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660267.2660283"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2018.00031"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2006.13"},{"key":"e_1_2_2_16_1","volume-title":"Verified Correctness and Security of OpenSSL HMAC. In 24th USENIX Security Symposium, USENIX Security 15","author":"Beringer Lennart","year":"2015","unstructured":"Lennart Beringer , Adam Petcher , Katherine Q. Ye , and Andrew W. Appel . 2015 . Verified Correctness and Security of OpenSSL HMAC. In 24th USENIX Security Symposium, USENIX Security 15 , Washington, D.C., USA , August 12-14, 2015 ., Jaeyeon Jung and Thorsten Holz (Eds.). USENIX Association, 207\u2013221. https:\/\/www.usenix.org\/conference\/usenixsecurity15\/technicalsessions\/presentation\/beringer Lennart Beringer, Adam Petcher, Katherine Q. Ye, and Andrew W. Appel. 2015. Verified Correctness and Security of OpenSSL HMAC. In 24th USENIX Security Symposium, USENIX Security 15, Washington, D.C., USA, August 12-14, 2015., Jaeyeon Jung and Thorsten Holz (Eds.). USENIX Association, 207\u2013221. https:\/\/www.usenix.org\/conference\/usenixsecurity15\/technicalsessions\/presentation\/beringer"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/11745853_14"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33481-8_9"},{"key":"e_1_2_2_19_1","volume-title":"Information-Flow Preservation in Compiler Optimisations","author":"Besson Fr\u00e9d\u00e9ric","unstructured":"Fr\u00e9d\u00e9ric Besson , Alexandre Dang , and Thomas Jensen . 2019. Information-Flow Preservation in Compiler Optimisations . In CSF. IEEE. Fr\u00e9d\u00e9ric Besson, Alexandre Dang, and Thomas Jensen. 2019. Information-Flow Preservation in Compiler Optimisations. In CSF. IEEE."},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/11813040_31"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-181136"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314605"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806643"},{"key":"e_1_2_2_24_1","unstructured":"Inria 2019. The Coq proof assistant reference manual. Inria. http:\/\/coq.inria.fr Version 8.9.1.  Inria 2019. The Coq proof assistant reference manual. Inria. http:\/\/coq.inria.fr Version 8.9.1."},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676966"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192377"},{"key":"e_1_2_2_27_1","volume-title":"ERTS2 2018 - 9th European Congress Embedded Real-Time Software and Systems. 3AF, SEE","author":"K\u00e4stner Daniel","unstructured":"Daniel K\u00e4stner , J\u00f6rg Barrho , Ulrich W\u00fcnsche , Marc Schlickling , Bernhard Schommer , Michael Schmidt , Christian Ferdinand , Xavier Leroy , and Sandrine Blazy . 2018. CompCert: Practical Experience on Integrating and Qualifying a Formally Verified Optimizing Compiler . In ERTS2 2018 - 9th European Congress Embedded Real-Time Software and Systems. 3AF, SEE , SIE , Toulouse, France , 1\u20139. https:\/\/hal.inria.fr\/hal- 01643290 Daniel K\u00e4stner, J\u00f6rg Barrho, Ulrich W\u00fcnsche, Marc Schlickling, Bernhard Schommer, Michael Schmidt, Christian Ferdinand, Xavier Leroy, and Sandrine Blazy. 2018. CompCert: Practical Experience on Integrating and Qualifying a Formally Verified Optimizing Compiler. In ERTS2 2018 - 9th European Congress Embedded Real-Time Software and Systems. 3AF, SEE, SIE, Toulouse, France, 1\u20139. https:\/\/hal.inria.fr\/hal- 01643290"},{"key":"e_1_2_2_28_1","volume-title":"When Constant-Time Source Yields VariableTime Binary: Exploiting Curve25519-donna Built with MSVC","author":"Kaufmann Thierry","year":"2015","unstructured":"Thierry Kaufmann , Herv\u00e9 Pelletier , Serge Vaudenay , and Karine Villegas . 2016. When Constant-Time Source Yields VariableTime Binary: Exploiting Curve25519-donna Built with MSVC 2015 . In 15 th International Conference on Cryptology and Network Security (CANS) . 573\u2013582. Thierry Kaufmann, Herv\u00e9 Pelletier, Serge Vaudenay, and Karine Villegas. 2016. When Constant-Time Source Yields VariableTime Binary: Exploiting Curve25519-donna Built with MSVC 2015. In 15 th International Conference on Cryptology and Network Security (CANS). 573\u2013582."},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"e_1_2_2_30_1","unstructured":"Adam Langley. 2010. ctgrind. https:\/\/github.com\/agl\/ctgrind  Adam Langley. 2010. ctgrind. https:\/\/github.com\/agl\/ctgrind"},{"key":"e_1_2_2_31_1","unstructured":"Adam Langley. 2015. curve25519-donna. https:\/\/code.google.com\/archive\/p\/curve25519- donna  Adam Langley. 2015. curve25519-donna. https:\/\/code.google.com\/archive\/p\/curve25519- donna"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_2_2_33_1","volume-title":"Formal verification of a realistic compiler. Commun. ACM","author":"Leroy Xavier","year":"2009","unstructured":"Xavier Leroy . 2009a. Formal verification of a realistic compiler. Commun. ACM ( 2009 ). Xavier Leroy. 2009a. Formal verification of a realistic compiler. Commun. ACM (2009)."},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_2_2_35_1","volume-title":"Program Logics for Certified Compilers, Andrew W","author":"Leroy Xavier","unstructured":"Xavier Leroy , Andrew W. Appel , Sandrine Blazy , and Gordon Stewart . 2014. The CompCert memory model . In Program Logics for Certified Compilers, Andrew W . Appel (Ed.). Cambridge University Press , 237\u2013271. https:\/\/hal.inria.fr\/hal- 00905435 Xavier Leroy, Andrew W. Appel, Sandrine Blazy, and Gordon Stewart. 2014. The CompCert memory model. In Program Logics for Certified Compilers, Andrew W. Appel (Ed.). Cambridge University Press, 237\u2013271. https:\/\/hal.inria.fr\/hal- 00905435"},{"key":"e_1_2_2_36_1","volume-title":"CompCert - A Formally Verified Optimizing Compiler. In ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress. SEE","author":"Leroy Xavier","year":"2016","unstructured":"Xavier Leroy , Sandrine Blazy , Daniel K\u00e4stner , Bernhard Schommer , Markus Pister , and Christian Ferdinand . 2016 . CompCert - A Formally Verified Optimizing Compiler. In ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress. SEE , Toulouse, France. https:\/\/hal.inria.fr\/hal- 01238879 Xavier Leroy, Sandrine Blazy, Daniel K\u00e4stner, Bernhard Schommer, Markus Pister, and Christian Ferdinand. 2016. CompCert - A Formally Verified Optimizing Compiler. In ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress. SEE, Toulouse, France. https:\/\/hal.inria.fr\/hal- 01238879"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2013.11"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314622"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/11734727_14"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2016.36"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2017.53"},{"key":"e_1_2_2_42_1","unstructured":"OpenSSL. 2019. OpenSSL. https:\/\/www.openssl.org\/  OpenSSL. 2019. OpenSSL. https:\/\/www.openssl.org\/"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110262"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3280984"},{"key":"e_1_2_2_45_1","volume-title":"Type-Driven Repair for Information Flow Security. CoRR abs\/1607.03445","author":"Polikarpova Nadia","year":"2016","unstructured":"Nadia Polikarpova , Jean Yang , Shachar Itzhaky , and Armando Solar-Lezama . 2016. Type-Driven Repair for Information Flow Security. CoRR abs\/1607.03445 ( 2016 ). arXiv: 1607.03445 http:\/\/arxiv.org\/abs\/1607.03445 Nadia Polikarpova, Jean Yang, Shachar Itzhaky, and Armando Solar-Lezama. 2016. Type-Driven Repair for Information Flow Security. CoRR abs\/1607.03445 (2016). arXiv: 1607.03445 http:\/\/arxiv.org\/abs\/1607.03445"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110261"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2892208.2892230"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243775"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2487241.2487248"},{"key":"e_1_2_2_50_1","volume-title":"International Conference on Interactive Theorem Proving (Lecture Notes in Computer Science). Springer-Verlag.","author":"Sison Robert","year":"2019","unstructured":"Robert Sison and Toby Murray . 2019 . Verifying that a compiler preserves concurrent value-dependent information-flow security . In International Conference on Interactive Theorem Proving (Lecture Notes in Computer Science). Springer-Verlag. Robert Sison and Toby Murray. 2019. Verifying that a compiler preserves concurrent value-dependent information-flow security. In International Conference on Interactive Theorem Proving (Lecture Notes in Computer Science). Springer-Verlag."},{"key":"e_1_2_2_51_1","unstructured":"SUPERCOP. 2019. SUPERCOP. https:\/\/bench.cr.yp.to\/supercop.html  SUPERCOP. 2019. SUPERCOP. https:\/\/bench.cr.yp.to\/supercop.html"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951924"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2016.35"},{"key":"e_1_2_2_54_1","volume-title":"IODINE: Verifying Constant-Time Execution of Hardware. In USENIX Security Symposium. USENIX.","author":"von Gleissenthall Klaus","year":"2019","unstructured":"Klaus von Gleissenthall , Rami G\u00f6khan K\u0131c\u0131 , Deian Stefan , and Ranjit Jhala . 2019 . IODINE: Verifying Constant-Time Execution of Hardware. In USENIX Security Symposium. USENIX. Klaus von Gleissenthall, Rami G\u00f6khan K\u0131c\u0131, Deian Stefan, and Ranjit Jhala. 2019. IODINE: Verifying Constant-Time Execution of Hardware. In USENIX Security Symposium. USENIX."},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58108-1_16"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3213846.3213851"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3133974"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103709"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462164"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134043"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371075","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371075","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371075","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:05:42Z","timestamp":1750273542000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371075"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12,20]]},"references-count":60,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2020,1]]}},"alternative-id":["10.1145\/3371075"],"URL":"https:\/\/doi.org\/10.1145\/3371075","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,12,20]]},"assertion":[{"value":"2019-12-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}