{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T16:39:23Z","timestamp":1783010363890,"version":"3.54.6"},"reference-count":46,"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\/"}],"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                    We address the problem of preserving non-interference across compiler transformations\n                    <jats:italic toggle=\"yes\">under speculative semantics<\/jats:italic>\n                    . We develop a proof method that ensures the preservation uniformly across all source programs. The basis of our proof method is a new form of simulation relation. It operates over directives that model the attacker\u2019s control over the micro-architectural state, and it accounts for the fact that the compiler transformation may change the influence of the micro-architectural state on the execution (and hence the directives). Using our proof method, we show the correctness of dead code elimination. When we tried to prove register allocation correct, we identified a previously unknown weakness that introduces violations to non-interference. We have confirmed the weakness for a mainstream compiler on code from the\n                    <jats:monospace>libsodium<\/jats:monospace>\n                    cryptographic library. To reclaim security once more, we develop a novel static analysis that operates on a product of source program and register-allocated program. Using the analysis, we present an automated fix to existing register allocation implementations. We prove the correctness of the fixed register allocations with our proof method.\n                  <\/jats:p>","DOI":"10.1145\/3704887","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"1506-1535","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0009-4781-8583","authenticated-orcid":false,"given":"S\u00f6ren","family":"van der Wall","sequence":"first","affiliation":[{"name":"TU Braunschweig, Braunschweig, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8495-671X","authenticated-orcid":false,"given":"Roland","family":"Meyer","sequence":"additional","affiliation":[{"name":"TU Braunschweig, Braunschweig, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/019\/0242403"},{"key":"e_1_3_2_3_1","first-page":"481","article-title":"\u201cAn Algebraic Definition of Simulation between Programs.\u201d","author":"Milner Robin","year":"1971","unstructured":"Robin Milner. 1971. \u201cAn Algebraic Definition of Simulation between Programs.\u201d IFCAI. William Kaufmann, 481\u2013489.","journal-title":"IFCAI"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/512927.512945"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/0096-0551(81)90048-5"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.1982.10014"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/277650.277714"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292561"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/330249.330250"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2002.806121"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.comnet.2005.01.010"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/11734727_14"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2009-0393"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.42"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660267.2660283"},{"key":"e_1_3_2_17_1","first-page":"719","article-title":"\u201cFLUSH+RELOAD: A High Resolution, Low Noise, L3 Cache Side-Channel Attack.\u201d","author":"Yarom Yuval","year":"2014","unstructured":"Yuval Yarom and Katrina Falkner. 2014. \u201cFLUSH+RELOAD: A High Resolution, Low Noise, L3 Cache Side-Channel Attack.\u201d USENIX, 719\u2013732.","journal-title":"USENIX"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2015.43"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908100"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2018.00031"},{"key":"e_1_3_2_21_1","unstructured":"Jann Horn. 2018. Speculative Execution Variant 4: Speculative Store Bypass. Retrieved July 11 2024 from https:\/\/bugs.chromium.org\/p\/project-zero\/issues\/detail?id=1528."},{"key":"e_1_3_2_22_1","article-title":"\u201cSpectre Returns! Speculation Attacks Using the Return Stack Buffer.\u201d","author":"Koruyeh Esmaeil Mohammadian","year":"2018","unstructured":"Esmaeil Mohammadian Koruyeh, Khaled N. Khasawneh, Chengyu Song, and Nael Abu-Ghazaleh. 2018. \u201cSpectre Returns! Speculation Attacks Using the Return Stack Buffer.\u201d USENIX.","journal-title":"USENIX"},{"key":"e_1_3_2_23_1","first-page":"973","article-title":"\u201cMeltdown: Reading Kernel Memory from User Space.\u201d","author":"Lipp Moritz","year":"2018","unstructured":"Moritz Lipp, Michael Schwarz, Daniel Gruss, Thomas Prescher, Werner Haas, Anders Fogh, Jann Horn, Stefan Mangard, Paul Kocher, Daniel Genkin, Yuval Yarom, and Mike Hamburg. 2018. \u201cMeltdown: Reading Kernel Memory from User Space.\u201d USENIX, 973\u2013990.","journal-title":"USENIX"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP.2018.00009"},{"key":"e_1_3_2_25_1","unstructured":"Paul Turner. 2018. Retpoline: A Software Construct for Preventing Branch-Target-Injection. Retrieved Oct. 24 2024 from https:\/\/support.google.com\/faqs\/answer\/7625886."},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371075"},{"key":"e_1_3_2_27_1","first-page":"249","article-title":"\u201cA Systematic Evaluation of Transient Execution Attacks and Defenses.\u201d","author":"Canella Claudio","year":"2019","unstructured":"Claudio Canella, Jo Van Bulck, Michael Schwarz, Moritz Lipp, Benjaminvon Berg, Philipp Ortner, Frank Piessens, Dmitry Evtyushkin, and Daniel Gruss. 2019. \u201cA Systematic Evaluation of Transient Execution Attacks and Defenses.\u201d USENIX, 249\u2013266.","journal-title":"USENIX"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00002"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385970"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372297.3417246"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00011"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00008"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF51468.2021.00020"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00046"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3460120.3484761"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2021.24286"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00036"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3460120.3484534"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434330"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485519"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP46214.2022.9833707"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-80515-9_22"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622857"},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP46215.2023.10179418"},{"key":"e_1_3_2_45_1","first-page":"7125","article-title":"\u201cUltimate SLH: Taking Speculative Load Hardening to the Next Level.\u201d","author":"Zhang Zhiyuan","year":"2023","unstructured":"Zhiyuan Zhang, Gilles Barthe, Chitchanok Chuengsatiansup, Peter Schwabe, and Yuval Yarom. 2023. \u201cUltimate SLH: Taking Speculative Load Hardening to the Next Level.\u201d USENIX, 7125\u20137142.","journal-title":"USENIX"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704880"},{"key":"e_1_3_2_47_1","unstructured":"Chandler Carruth. 2024. Speculative Load Hardening - LLVM. Retrieved July 12 2024 from https:\/\/llvm.org\/docs\/SpeculativeLoadHardening.html."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704887","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704887","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:14:47Z","timestamp":1770200087000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704887"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":46,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704887"],"URL":"https:\/\/doi.org\/10.1145\/3704887","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"}}]}}