{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,7]],"date-time":"2026-05-07T02:44:27Z","timestamp":1778121867773,"version":"3.51.4"},"reference-count":61,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["EXC 2092 CASA - 390781972"],"award-info":[{"award-number":["EXC 2092 CASA - 390781972"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["ANR-22-PECY-0006"],"award-info":[{"award-number":["ANR-22-PECY-0006"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,1,7]]},"abstract":"<jats:p>\n                    Compilers often weaken or even discard software-based countermeasures commonly used to protect programs against side-channel attacks; worse, they may also introduce vulnerabilities that attackers can exploit. The solution to this problemis to develop compilers that preserve such countermeasures. Prior work establishes that (a mildly modified version of) the CompCert and Jasmin formally verified compilers preserve constant-time, an information flow policy that ensures that programs are protected against timing side-channel attacks. However, nothing is known about preservation of speculative constant-time, a strengthening of the constant-time policythat ensures that programs are protected against Spectre-v1 attacks. We first show that preservation of speculative constant-time fails in practice by providing examples of secure programs whose compilation is not speculative constant-time using GCC (GCC -O0 and GCC -O1) and Jasmin. Then, we define a proof-of-concept compiler that distills some of the critical passes of the Jasmin compiler and use the C\n                    <jats:sc>oq<\/jats:sc>\n                    proof assistant to prove that it preserves speculative constant-time. Finally, we patch the Jasmin speculative constant-time type checker and demonstrate that all cryptographic implementations written in Jasmin can be fixed with minimal impact.\n                  <\/jats:p>","DOI":"10.1145\/3704880","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"1293-1325","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Preservation of Speculative Constant-Time by Compilation"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0007-7425-570X","authenticated-orcid":false,"given":"Santiago","family":"Arranz Olmos","sequence":"first","affiliation":[{"name":"MPI-SP, Bochum, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3853-1777","authenticated-orcid":false,"given":"Gilles","family":"Barthe","sequence":"additional","affiliation":[{"name":"MPI-SP, Bochum, Germany"},{"name":"IMDEA Software Institute, Madrid, Spain"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9058-2005","authenticated-orcid":false,"given":"Lionel","family":"Blatter","sequence":"additional","affiliation":[{"name":"MPI-SP, Bochum, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6650-9924","authenticated-orcid":false,"given":"Benjamin","family":"Gr\u00e9goire","sequence":"additional","affiliation":[{"name":"Inria, Sophia Antipolis, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3468-352X","authenticated-orcid":false,"given":"Vincent","family":"Laporte","sequence":"additional","affiliation":[{"name":"Inria, Nancy, France"},{"name":"Universit\u00e9 de Lorraine, Nancy, France"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3460860"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2019.00025"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49890-3_24"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.42"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134078"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00028"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-12466-7_1"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP46215.2023.10179355"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP46215.2023.10179418"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3548606.3560689"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372297.3417268"},{"key":"e_1_2_2_12_1","unstructured":"Santiago Arranz Olmos Gilles Barthe Chitchanok Chuengsatiansup Benjamin Gr\u00e9goire Vincent Laporte Tiago Oliveira Peter Schwabe Yuval Yarom and Zhiyuan Zhang. 2024. Protecting cryptographic code against Spectre-RSB. Cryptology ePrint Archive Paper 2024\/1070. https:\/\/eprint.iacr.org\/2024\/1070"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00008"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660267.2660283"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371075"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00046"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2018.00031"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3460120.3484761"},{"key":"e_1_2_2_19_1","unstructured":"Daniel J Bernstein. 2005. Cache-timing attacks on AES."},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_18"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54108-7_15"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594301"},{"key":"e_1_2_2_23_1","volume-title":"RFC: Speculative Load Hardening (a Spectre variant #1 mitigation). https:\/\/lists.llvm.org\/pipermail\/llvm-dev\/2018-March\/122085.html","author":"Carruth Chandler","year":"2018","unstructured":"Chandler Carruth. 2018. RFC: Speculative Load Hardening (a Spectre variant #1 mitigation). https:\/\/lists.llvm.org\/pipermail\/llvm-dev\/2018-March\/122085.html"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP46214.2022.9833707"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385970"},{"key":"e_1_2_2_26_1","unstructured":"Boru Chen Yingchen Wang Pradyumna Shome Christopher W. Fletcher David Kohlbrenner Riccardo Paccagnella and Daniel Genkin. 2024. GoFetch: Breaking Constant-Time Cryptographic Implementations Using Data Memory-Dependent Prefetchers. In USENIX Security."},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2014.26"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/SPW.2015.33"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/S13389-016-0141-6"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3576915.3623112"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134029"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428272"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00011"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP46214.2022.9833713"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04138-9_1"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3576915.3616611"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00002"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-68697-5_9"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254111"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542504"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341687"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2017.13"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3460120.3484534"},{"key":"e_1_2_2_45_1","unstructured":"Colin Percival. 2005. Cache missing for fun and profit."},{"key":"e_1_2_2_46_1","unstructured":"Antoon Purnal. 2024. PQShield plugs timing leaks in Kyber \/ ML-KEM to improve PQC implementation maturity. https:\/\/pqshield.com\/pqshield-plugs-timing-leaks-in-kyber-ml-kem-to-improve-pqc-implementation-maturity\/"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243775"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.46586\/TCHES.V2024.I1.457-500"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP.2018.00009"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/S00145-009-9049-Y"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704887"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434330"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP46214.2022.9833570"},{"key":"e_1_2_2_54_1","volume-title":"31st USENIX Security Symposium, USENIX Security 2022","author":"Wang Yingchen","year":"2022","unstructured":"Yingchen Wang, Riccardo Paccagnella, Elizabeth Tang He, Hovav Shacham, Christopher W. Fletcher, and David Kohlbrenner. 2022. Hertzbleed: Turning Power Side-Channel Attacks Into Remote Timing Attacks on x86. In 31st USENIX Security Symposium, USENIX Security 2022, Boston, MA, USA, August 10-12, 2022, Kevin R. B. Butler and Kurt Thomas (Eds.). USENIX Association, 679\u2013697. https:\/\/www.usenix.org\/conference\/usenixsecurity22\/presentation\/wang-yingchen"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP46215.2023.10179326"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290375"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371119"},{"key":"e_1_2_2_58_1","volume-title":"Silent Bugs Matter: A Study of Compiler-Introduced Security Bugs. In 32nd USENIX Security Symposium, USENIX Security 2023","author":"Xu Jianhao","year":"2023","unstructured":"Jianhao Xu, Kangjie Lu, Zhengjie Du, Zhu Ding, Linke Li, Qiushi Wu, Mathias Payer, and Bing Mao. 2023. Silent Bugs Matter: A Study of Compiler-Introduced Security Bugs. In 32nd USENIX Security Symposium, USENIX Security 2023, Anaheim, CA, USA, August 9-11, 2023, Joseph A. Calandrino and Carmela Troncoso (Eds.). USENIX Association, 3655\u20133672. https:\/\/www.usenix.org\/conference\/usenixsecurity23\/presentation\/xu-jianhao"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/S13389-017-0152-Y"},{"key":"e_1_2_2_60_1","volume-title":"32nd USENIX Security Symposium, USENIX Security 2023","author":"Zhang Zhiyuan","year":"2023","unstructured":"Zhiyuan Zhang, Gilles Barthe, Chitchanok Chuengsatiansup, Peter Schwabe, and Yuval Yarom. 2023. Ultimate SLH: Taking Speculative Load Hardening to the Next Level. In 32nd USENIX Security Symposium, USENIX Security 2023, Anaheim, CA, USA, August 9-11, 2023, Joseph A. Calandrino and Carmela Troncoso (Eds.). USENIX Association, 7125\u20137142. https:\/\/www.usenix.org\/conference\/usenixsecurity23\/presentation\/zhang-zhiyuan-slh"},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/2038642.2038687"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704880","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704880","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:14:01Z","timestamp":1770200041000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704880"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":61,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704880"],"URL":"https:\/\/doi.org\/10.1145\/3704880","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-11","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}