{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,28]],"date-time":"2026-08-28T16:52:29Z","timestamp":1787935949136,"version":"build-2784847793"},"reference-count":59,"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\/501100004837","name":"Spanish Ministry of Science and Innovation","doi-asserted-by":"crossref","award":["TED2021-132464B-I00 PRODIGY, RYC2021-032614-I, PID2022-142290OB-I00 ESPADA"],"award-info":[{"award-number":["TED2021-132464B-I00 PRODIGY, RYC2021-032614-I, PID2022-142290OB-I00 ESPADA"]}],"id":[{"id":"10.13039\/501100004837","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100003407","name":"Italian Ministry of Education","doi-asserted-by":"crossref","award":["Rita Levi Montalcini grant (call of 2019)"],"award-info":[{"award-number":["Rita Levi Montalcini grant (call of 2019)"]}],"id":[{"id":"10.13039\/501100003407","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":[[2025,1,7]]},"abstract":"<jats:p>\n                    Mainstream compilers implement different countermeasures to prevent specific classes of speculative execution attacks. Unfortunately, these countermeasures either lack formal guarantees or come with proofs restricted to speculative semantics capturing only a subset of the speculation mechanisms supported by modern CPUs, thereby limiting their practical applicability. Ideally, these security proofs should target a speculative semantics capturing the effects of\n                    <jats:italic toggle=\"yes\">all<\/jats:italic>\n                    speculation mechanisms implemented in modern CPUs. However, this is impractical and requires new secure compilation proofs to support additional speculation mechanisms.\n                  <\/jats:p>\n                  <jats:p>\n                    In this paper, we address this problem by proposing a novel secure compilation framework that allows\n                    <jats:italic toggle=\"yes\">lifting<\/jats:italic>\n                    the security guarantees provided by Spectre countermeasures from weaker speculative semantics (ignoring some speculation mechanisms) to stronger ones (accounting for the omitted mechanisms)\n                    <jats:italic toggle=\"yes\">without<\/jats:italic>\n                    requiring new secure compilation proofs. Using our lifting framework, we performed the most comprehensive security analysis of Spectre countermeasures implemented in mainstream compilers to date. Our analysis spans 9 different countermeasures against 5 classes of Spectre attacks, which we proved secure against a speculative semantics accounting for 5 different speculation mechanisms. Our analysis highlights that fence-based and retpoline-based countermeasures can be securely lifted to the strongest speculative semantics under study. In contrast, countermeasures based on speculative load hardening cannot be securely lifted to semantics supporting indirect jump speculation.\n                  <\/jats:p>","DOI":"10.1145\/3704867","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"893-922","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Do You Even Lift? Strengthening Compiler Security Guarantees against Spectre Attacks"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0006-6342-4646","authenticated-orcid":false,"given":"Xaver","family":"Fabian","sequence":"first","affiliation":[{"name":"CISPA Helmholtz Center for Information Security, Saarbr\u00fccken, Germany"},{"name":"University of Trento, Trento, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3411-9678","authenticated-orcid":false,"given":"Marco","family":"Patrignani","sequence":"additional","affiliation":[{"name":"University of Trento, Trento, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5767-555X","authenticated-orcid":false,"given":"Marco","family":"Guarnieri","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute, Madrid, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7130-9211","authenticated-orcid":false,"given":"Michael","family":"Backes","sequence":"additional","affiliation":[{"name":"CISPA Helmholtz Center for Information Security, Saarbr\u00fccken, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/324133.324266"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2019.00025"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134078"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00028"},{"key":"e_1_3_2_6_2","unstructured":"AMD. 2020. Whitepaper Straight-line Speculation. https:\/\/www.amd.com\/system\/files\/documents\/technical-guidance-for-mitigating-branch-type-confusion.pdf."},{"key":"e_1_3_2_7_2","unstructured":"AMD. 2021. Security analysis of AMD predictive store forwarding. https:\/\/www.amd.com\/system\/files\/documents\/security-analysis-predictive-store-forwarding.pdf. Accessed: 2024-03-11."},{"key":"e_1_3_2_8_2","unstructured":"ARM. 2020. Whitepaper Straight-line Speculation. https:\/\/developer.arm.com\/documentation\/102825\/0100\/."},{"key":"e_1_3_2_9_2","unstructured":"ARM. 2021. Arm Armv9-A A64 Instruction Set Architecture. https:\/\/developer.arm.com\/documentation\/100076\/0100\/A64-Instruction-Set-Reference\/A64-General-Instructions\/BTI?"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89722-6_4"},{"key":"e_1_3_2_11_2","unstructured":"Enrico Barberis Pietro Frigo Marius Muench Herbert Bos and Cristiano Giuffrida. 2022. Branch History Injection: On the Effectiveness of Hardware Mitigations Against Cross-Privilege Spectre-v2 Attacks. In Proceedings of the 31st USENIX Security Symposium (USENIX Security \u201922). USENIX Association. https:\/\/www.usenix.org\/conference\/usenixsecurity22\/presentation\/barberis"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/3658644.3670319"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00046"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/3319535.3363194"},{"key":"e_1_3_2_15_2","volume-title":"Proceedings of the 28th USENIX Security Symposium (USENIX Security \u201919)","author":"Canella Claudio","year":"2019","unstructured":"Claudio Canella, Jo Van Bulck, Michael Schwarz, Moritz Lipp, Benjamin von Berg, Philipp Ortner, Frank Piessens, Dmitry Evtyushkin, and Daniel Gruss. 2019. A Systematic Evaluation of Transient Execution Attacks and Defenses. In Proceedings of the 28th USENIX Security Symposium (USENIX Security \u201919). USENIX Association. https:\/\/www.usenix.org\/conference\/usenixsecurity19\/presentation\/canella"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/3386263.3407584"},{"key":"e_1_3_2_17_2","unstructured":"Chandler Carruth. 2018. Speculative Load Hardening. https:\/\/llvm.org\/docs\/SpeculativeLoadHardening.html"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385970"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP46214.2022.9833707"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2019.00027"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-54997-8_21"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2021.24286"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00047"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1109\/CSF54842.2022.9919680"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/3548606.3560555"},{"key":"e_1_3_2_26_2","unstructured":"Xaver Fabian Marco Guarnieri Marco Patrignani and Michael Backes. 2024. https:\/\/github.com\/XFabian\/secure_comp_lifting"},{"key":"e_1_3_2_27_2","doi-asserted-by":"crossref","unstructured":"Xaver Fabian Marco Patrignani Marco Guarnieri and Michael Backes. 2024. Do You Even Lift? Strengthening Compiler Security Guarantees Against Spectre Attacks. arXiv:2405.10089 [cs.PL] https:\/\/arxiv.org\/abs\/2405.10089","DOI":"10.1145\/3704867"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/1275497.1275500"},{"key":"e_1_3_2_29_2","article-title":"Authenticity by Typing for Security Protocols","volume":"11","author":"Gordon Andrew D.","year":"2003","unstructured":"Andrew D. Gordon and Alan Jeffrey. 2003. Authenticity by Typing for Security Protocols. J. Comput. Secur. 11 (2003). http:\/\/dl.acm.org\/citation.cfm?id=959088.959090","journal-title":"J. Comput. Secur."},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/3372297.3417246"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00036"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00011"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/3377811.3380428"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062363"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/3634737.3637662"},{"key":"e_1_3_2_36_2","unstructured":"J. Horn. 2018. Speculative execution variant 4: Speculative store bypass. https:\/\/bugs.chromium.org\/p\/project-zero\/issues\/detail?id=1528. Accessed: 2021-04-11."},{"key":"e_1_3_2_37_2","unstructured":"Intel. 2018. Retpoline: A Branch Target Injection Mitigation. https:\/\/www.intel.com\/content\/dam\/develop\/external\/us\/en\/documents\/retpoline-a-branch-target-injection-mitigation.pdf"},{"key":"e_1_3_2_38_2","unstructured":"Intel. 2018. Speculative Store Bypass. https:\/\/www.intel.com\/content\/www\/us\/en\/developer\/articles\/technical\/software-security-guidance\/advisory-guidance\/speculative-store-bypass.html"},{"key":"e_1_3_2_39_2","unstructured":"Intel. 2018. Using Intel Compilers to Mitigate Speculative Execution Side-Channel Issues. https:\/\/software.intel.com\/en-us\/articles\/using-intel-compilers-to-mitigate-speculative-execution-side-channel-issues"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00002"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-68697-5_9"},{"key":"e_1_3_2_42_2","volume-title":"Proceedings of the 12th USENIX Workshop on Offensive Technologies (WOOT \u201918)","author":"Koruyeh Esmaeil Mohammadian","year":"2018","unstructured":"Esmaeil Mohammadian Koruyeh, Khaled N. Khasawneh, Chengyu Song, and Nael Abu-Ghazaleh. 2018. Spectre Returns! Speculation Attacks Using the Return Stack Buffer. In Proceedings of the 12th USENIX Workshop on Offensive Technologies (WOOT \u201918). USENIX Association. https:\/\/www.usenix.org\/conference\/woot18\/presentation\/koruyeh"},{"key":"e_1_3_2_43_2","unstructured":"Matthis Kruse and Marco Patrignani. 2022. Composing Secure Compilers."},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243761"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP54263.2024.00048"},{"key":"e_1_3_2_46_2","volume-title":"Proceedings of the 30th USENIX Security Symposium (USENIX Security \u201921)","author":"Narayan Shravan","year":"2021","unstructured":"Shravan Narayan, Craig Disselkoen, Daniel Moghimi, Sunjay Cauligi, Evan Johnson, Zhao Gang, Anjo Vahldiek-Oberwagner, Ravi Sahita, Hovav Shacham, Dean Tullsen, and Deian Stefan. 2021. Swivel: Hardening Web Assembly against Spectre. In Proceedings of the 30th USENIX Security Symposium (USENIX Security \u201921). USENIX Association. https:\/\/www.usenix.org\/conference\/usenixsecurity21\/presentation\/narayan"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP46215.2023.10179391"},{"key":"e_1_3_2_48_2","unstructured":"Marco Patrignani. 2020. Why should anyone use colours? or syntax highlighting beyond code snippets. arXiv preprint arXiv:2001.11334 (2020)."},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1109\/CSF57540.2023.00045"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1145\/3460120.3484534"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP46214.2022.9833774"},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371100"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.1145\/3337167.3337175"},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP46215.2023.10179418"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP46215.2023.10179355"},{"key":"e_1_3_2_56_2","doi-asserted-by":"publisher","DOI":"10.1145\/3133913"},{"key":"e_1_3_2_57_2","doi-asserted-by":"publisher","DOI":"10.1145\/3434330"},{"key":"e_1_3_2_58_2","doi-asserted-by":"publisher","DOI":"10.1145\/3613424.3614275"},{"key":"e_1_3_2_59_2","doi-asserted-by":"publisher","DOI":"10.1145\/3373376.3378526"},{"key":"e_1_3_2_60_2","volume-title":"Proceedings of the 32nd USENIX Conference on Security Symposium (USENIX Security \u201923)","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 Proceedings of the 32nd USENIX Conference on Security Symposium (USENIX Security \u201923). USENIX Association. https:\/\/www.usenix.org\/conference\/usenixsecurity23\/presentation\/zhang-zhiyuan-slh"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704867","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704867","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:17:36Z","timestamp":1770200256000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704867"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":59,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704867"],"URL":"https:\/\/doi.org\/10.1145\/3704867","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"}}]}}