{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:31:55Z","timestamp":1767929515589,"version":"3.49.0"},"reference-count":52,"publisher":"IEEE","license":[{"start":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T00:00:00Z","timestamp":1659312000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-009"},{"start":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T00:00:00Z","timestamp":1659312000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-001"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022,8]]},"DOI":"10.1109\/csf54842.2022.9919680","type":"proceedings-article","created":{"date-parts":[[2022,11,3]],"date-time":"2022-11-03T21:29:20Z","timestamp":1667510960000},"page":"64-79","source":"Crossref","is-referenced-by-count":5,"title":["SecurePtrs: Proving Secure Compilation with Data-Flow Back-Translation and Turn-Taking Simulation"],"prefix":"10.1109","author":[{"given":"Akram","family":"El-Korashy","sequence":"first","affiliation":[{"name":"Max Planck Institute for Software Systems (MPI-SWS)"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roberto","family":"Blanco","sequence":"additional","affiliation":[{"name":"Max Planck Institute for Security and Privacy (MPI-SP)"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J\u00e9r\u00e9my","family":"Thibault","sequence":"additional","affiliation":[{"name":"Max Planck Institute for Security and Privacy (MPI-SP)"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adrien","family":"Durier","sequence":"additional","affiliation":[{"name":"Max Planck Institute for Security and Privacy (MPI-SP)"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Deepak","family":"Garg","sequence":"additional","affiliation":[{"name":"Max Planck Institute for Software Systems (MPI-SWS)"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"C\u0103t\u0103lin","family":"Hri\u0163cu","sequence":"additional","affiliation":[{"name":"Max Planck Institute for Security and Privacy (MPI-SP)"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2015.55"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1109\/CSF49147.2020.00026"},{"key":"ref15","article-title":"Modular, fully-abstract compilation by approximate back-translation","volume":"13","author":"devriese","year":"2017","journal-title":"LMCS"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837618"},{"key":"ref52","article-title":"Using hammock graphs to structure programs","author":"zhang","year":"2004","journal-title":"IEEE Trans Softw Eng"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1145\/3264820.3264822"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/CSF51468.2021.00020"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1109\/CSF51468.2021.00036"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1145\/2786763.2694383"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-54430-5_93"},{"key":"ref18","article-title":"Authenticity by typing for security protocols 1","volume":"11","author":"gordon","year":"2003","journal-title":"JCS"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1145\/2678373.2665740"},{"key":"ref50","author":"watson","year":"2019","journal-title":"Capability Hardware Enhanced RISC Instructions CHERI Instruction-Set Architecture (Version 7)"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1145\/3133913"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1145\/3341688"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2015.9"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2019.00024"},{"key":"ref42","article-title":"CompCertM: CompCert with C-assembly linking and lightweight modular verification","author":"song","year":"2019","journal-title":"PACMPL 4 (POPL)"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1145\/3290332"},{"key":"ref44","first-page":"241","author":"strackx","year":"2013","journal-title":"Protected Mode Software Architecture"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676985"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1109\/MM.2016.84"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2018.00031"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_2"},{"key":"ref9","article-title":"Formal verification of a constant-time preserving C compiler","volume":"4","author":"barthe","year":"2019","journal-title":"PACMPL"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_1"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2019.00025"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1145\/2034574.2034830"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411227"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796821000162"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1145\/2699503"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1145\/3280984"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1145\/3140587.3062347"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1145\/3341689"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784764"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-39322-9_1"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1145\/3436809"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951941"},{"key":"ref2","author":"abate","year":"2019","journal-title":"When good components go bad Formally secure compilation despite dynamic compromise"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0055109"},{"key":"ref39","article-title":"Verifying That a Compiler Preserves Concurrent Value-Dependent Information-Flow Security","author":"sison","year":"2019","journal-title":"ITP"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1145\/3371100"},{"key":"ref24","first-page":"667","author":"laird","year":"2007","journal-title":"A fully abstract trace semantics for general references"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48320-9_27"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9099-0"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2015.38"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837642"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1145\/361932.361937"},{"key":"ref27","article-title":"Proving compiler correctness in a mechanized logic","author":"milner","year":"1972","journal-title":"Machine Intelligence"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2008.ECP.24"}],"event":{"name":"2022 IEEE 35th Computer Security Foundations Symposium (CSF)","location":"Haifa, Israel","start":{"date-parts":[[2022,8,7]]},"end":{"date-parts":[[2022,8,10]]}},"container-title":["2022 IEEE 35th Computer Security Foundations Symposium (CSF)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/9919409\/9919636\/09919680.pdf?arnumber=9919680","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,8]],"date-time":"2023-11-08T18:07:07Z","timestamp":1699466827000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9919680\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8]]},"references-count":52,"URL":"https:\/\/doi.org\/10.1109\/csf54842.2022.9919680","relation":{},"subject":[],"published":{"date-parts":[[2022,8]]}}}