{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T18:17:14Z","timestamp":1781893034611,"version":"3.54.5"},"reference-count":37,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2019,7,26]],"date-time":"2019-07-26T00:00:00Z","timestamp":1564099200000},"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":[[2019,7,26]]},"abstract":"<jats:p>Separation logic is a powerful program logic for the static modular verification of imperative programs. However, dynamic checking of separation logic contracts on the boundaries between verified and untrusted modules is hard, because it requires one to enforce (among other things) that outcalls from a verified to an untrusted module do not access memory resources currently owned by the verified module.<\/jats:p>\n          <jats:p>This paper proposes an approach to dynamic contract checking by relying on support for capabilities, a well-studied form of unforgeable memory pointers that enables fine-grained, efficient memory access control. More specifically, we rely on a form of capabilities called linear capabilities for which the hardware enforces that they cannot be copied.<\/jats:p>\n          <jats:p>We formalize our approach as a fully abstract compiler from a statically verified source language to an unverified target language with support for linear capabilities. The key insight behind our compiler is that memory resources described by spatial separation logic predicates can be represented at run time by linear capabilities. The compiler is separation-logic-proof-directed: it uses the separation logic proof of the source program to determine how memory accesses in the source program should be compiled to linear capability accesses in the target program.<\/jats:p>\n          <jats:p>The full abstraction property of the compiler essentially guarantees that compiled verified modules can interact with untrusted target language modules as if they were compiled from verified code as well.<\/jats:p>","DOI":"10.1145\/3341688","type":"journal-article","created":{"date-parts":[[2019,7,29]],"date-time":"2019-07-29T20:55:51Z","timestamp":1564433751000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["Linear capabilities for fully abstract compilation of separation-logic-verified code"],"prefix":"10.1145","volume":"3","author":[{"given":"Thomas","family":"Van Strydonck","sequence":"first","affiliation":[{"name":"KU Leuven, Belgium"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Frank","family":"Piessens","sequence":"additional","affiliation":[{"name":"KU Leuven, Belgium"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dominique","family":"Devriese","sequence":"additional","affiliation":[{"name":"Vrije Universiteit Brussel, Belgium"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,7,26]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"Secure Internet programming","author":"Abadi Mart\u00edn","unstructured":"Mart\u00edn Abadi . 1999. Protection in programming-language translations . In Secure Internet programming . Springer-Verlag , 19\u201334. Mart\u00edn Abadi. 1999. Protection in programming-language translations. In Secure Internet programming. Springer-Verlag, 19\u201334."},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2240276.2240279"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676972"},{"key":"e_1_2_2_4_1","volume-title":"Verification, Model Checking, and Abstract Interpretation (Lecture Notes in Computer Science)","author":"Bader Johannes","unstructured":"Johannes Bader , Jonathan Aldrich , and \u00c9ric Tanter . 2018. Gradual Program Verification . In Verification, Model Checking, and Abstract Interpretation (Lecture Notes in Computer Science) . Springer International Publishing . Johannes Bader, Jonathan Aldrich, and \u00c9ric Tanter. 2018. Gradual Program Verification. In Verification, Model Checking, and Abstract Interpretation (Lecture Notes in Computer Science). Springer International Publishing."},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/1770351.1770381"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_6"},{"key":"e_1_2_2_7_1","volume-title":"Computer Aided Verification","author":"Berdine Josh","unstructured":"Josh Berdine , Byron Cook , and Samin Ishtiaq . 2011. SLAyer: Memory safety for systems-level code . In Computer Aided Verification . Springer , 178\u2013183. Josh Berdine, Byron Cook, and Samin Ishtiaq. 2011. SLAyer: Memory safety for systems-level code. In Computer Aided Verification. Springer, 178\u2013183."},{"key":"e_1_2_2_8_1","volume-title":"Moving Fast with Software Verification. 15","author":"Calcagno Cristiano","year":"2015","unstructured":"Cristiano Calcagno , Dino Distefano , J\u00e9r\u00e9my Dubreil , Dominik Gabi , Pieter Hooimeijer , Martino Luca , Peter W. O\u2019Hearn , Irene Papakonstantinou , Jim Purbrick , and Dulma Rodriguez . 2015. Moving Fast with Software Verification. 15 ( 2015 ), 3\u201311. Cristiano Calcagno, Dino Distefano, J\u00e9r\u00e9my Dubreil, Dominik Gabi, Pieter Hooimeijer, Martino Luca, Peter W. O\u2019Hearn, Irene Papakonstantinou, Jim Purbrick, and Dulma Rodriguez. 2015. Moving Fast with Software Verification. 15 (2015), 3\u201311."},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2694344.2694367"},{"key":"e_1_2_2_10_1","unstructured":"Adam Chlipala. 2017. Formal Reasoning About Programs.  Adam Chlipala. 2017. Formal Reasoning About Programs."},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2578855.2535839"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2015.55"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837618"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951930"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_19"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429114"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837670"},{"key":"e_1_2_2_19_1","unstructured":"Deepak Garg Catalin Hritcu Marco Patrignani Marco Stronati and David Swasey. 2017. Robust Hyperproperty Preservation for Secure Compilation (Extended Abstract). (2017). arXiv: 1710.07309 http:\/\/arxiv.org\/abs\/1710.07309  Deepak Garg Catalin Hritcu Marco Patrignani Marco Stronati and David Swasey. 2017. Robust Hyperproperty Preservation for Secure Compilation (Extended Abstract). (2017). arXiv: 1710.07309 http:\/\/arxiv.org\/abs\/1710.07309"},{"key":"e_1_2_2_20_1","volume-title":"Garbage Collection in C Programs","author":"Insolvibile Gianluca","year":"2003","unstructured":"Gianluca Insolvibile . 2003. Garbage Collection in C Programs . 2003 , 113 (2003), 7\u2013. http:\/\/dl.acm.org\/citation.cfm?id= 882036.882043 Gianluca Insolvibile. 2003. Garbage Collection in C Programs. 2003, 113 (2003), 7\u2013. http:\/\/dl.acm.org\/citation.cfm?id= 882036.882043"},{"key":"e_1_2_2_21_1","unstructured":"Bart Jacobs and Frank Piessens. 2008. The VeriFast program verifier. (2008). https:\/\/lirias.kuleuven.be\/handle\/123456789\/ 197789  Bart Jacobs and Frank Piessens. 2008. The VeriFast program verifier. (2008). https:\/\/lirias.kuleuven.be\/handle\/123456789\/ 197789"},{"key":"e_1_2_2_22_1","series-title":"Lecture Notes in Computer Science","volume-title":"Programming Languages and Systems","author":"Jacobs Bart","unstructured":"Bart Jacobs , Jan Smans , and Frank Piessens . 2010. A quick tour of the VeriFast program verifier . In Programming Languages and Systems . Lecture Notes in Computer Science , Vol. 6461 . Springer Berlin Heidelberg , 304\u2013311. Bart Jacobs, Jan Smans, and Frank Piessens. 2010. A quick tour of the VeriFast program verifier. In Programming Languages and Systems. Lecture Notes in Computer Science, Vol. 6461. Springer Berlin Heidelberg, 304\u2013311."},{"key":"e_1_2_2_23_1","volume-title":"Capability-Based Computer Systems","author":"Levy Henry M.","unstructured":"Henry M. Levy . 1984. Capability-Based Computer Systems . Digital Press . https:\/\/homes.cs.washington.edu\/~levy\/capabook\/ Henry M. Levy. 1984. Capability-Based Computer Systems. Digital Press. https:\/\/homes.cs.washington.edu\/~levy\/capabook\/"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951941"},{"key":"e_1_2_2_25_1","volume-title":"9th International Conference. 203\u2013217","author":"Nguyen Huu Hai","year":"2008","unstructured":"Huu Hai Nguyen , Viktor Kuncak , and Wei-Ngan Chin . 2008 . Runtime Checking for Separation Logic. In Verification, Model Checking, and Abstract Interpretation , 9th International Conference. 203\u2013217 . Huu Hai Nguyen, Viktor Kuncak, and Wei-Ngan Chin. 2008. Runtime Checking for Separation Logic. In Verification, Model Checking, and Abstract Interpretation, 9th International Conference. 203\u2013217."},{"key":"e_1_2_2_26_1","volume-title":"USENIX Security Symposium. 479\u2013494","author":"Noorman Job","year":"2013","unstructured":"Job Noorman , Pieter Agten , Wilfried Daniels , Raoul Strackx , Anthony Van Herrewege , Christophe Huygens , Bart Preneel , Ingrid Verbauwhede , and Frank Piessens . 2013 . Sancus: Low-cost Trustworthy Extensible Networked Devices with a Zero-software Trusted Computing Base .. In USENIX Security Symposium. 479\u2013494 . Job Noorman, Pieter Agten, Wilfried Daniels, Raoul Strackx, Anthony Van Herrewege, Christophe Huygens, Bart Preneel, Ingrid Verbauwhede, and Frank Piessens. 2013. Sancus: Low-cost Trustworthy Extensible Networked Devices with a Zero-software Trusted Computing Base.. In USENIX Security Symposium. 479\u2013494."},{"key":"e_1_2_2_27_1","unstructured":"Peter W. O\u2019Hearn. 2012. A Primer on Separation Logic (and Automatic Program Verification and Analysis). In Software Safety and Security - Tools for Analysis and Verification. 286\u2013318.  Peter W. O\u2019Hearn. 2012. A Primer on Separation Logic (and Automatic Program Verification and Analysis). In Software Safety and Security - Tools for Analysis and Verification. 286\u2013318."},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2699503"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3280984"},{"key":"e_1_2_2_30_1","volume-title":"Secure Compilation and Hyperproperty Preservation. In Computer Security Foundations Symposium. IEEE, 392\u2013404","author":"Patrignani M.","unstructured":"M. Patrignani and D. Garg . 2017 . Secure Compilation and Hyperproperty Preservation. In Computer Security Foundations Symposium. IEEE, 392\u2013404 . M. Patrignani and D. Garg. 2017. Secure Compilation and Hyperproperty Preservation. In Computer Security Foundations Symposium. IEEE, 392\u2013404."},{"key":"e_1_2_2_31_1","volume-title":"Efficient, Provably Secure Compilation. (April","author":"Patrignani Marco","year":"2018","unstructured":"Marco Patrignani and Deepak Garg . 2018. Robustly Safe Compilation or , Efficient, Provably Secure Compilation. (April 2018 ). https:\/\/arxiv.org\/abs\/1804.00489v3 Marco Patrignani and Deepak Garg. 2018. Robustly Safe Compilation or, Efficient, Provably Secure Compilation. (April 2018). https:\/\/arxiv.org\/abs\/1804.00489v3"},{"key":"e_1_2_2_32_1","volume-title":"Logic in Computer Science","author":"Reynolds John C.","unstructured":"John C. Reynolds . 2002. Separation logic: A logic for shared mutable data structures . In Logic in Computer Science . IEEE , 55\u201374. John C. Reynolds. 2002. Separation logic: A logic for shared mutable data structures. In Logic in Computer Science. IEEE, 55\u201374."},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290332"},{"key":"e_1_2_2_34_1","volume-title":"Security and Privacy in Communication Networks (Lecture Notes)","author":"Strackx Raoul","unstructured":"Raoul Strackx , Frank Piessens , and Bart Preneel . 2010. Efficient Isolation of Trusted Subsystems in Embedded Systems . In Security and Privacy in Communication Networks (Lecture Notes) . Springer , Berlin, Heidelberg , 344\u2013361. Raoul Strackx, Frank Piessens, and Bart Preneel. 2010. Efficient Isolation of Trusted Subsystems in Embedded Systems. In Security and Privacy in Communication Networks (Lecture Notes). Springer, Berlin, Heidelberg, 344\u2013361."},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133913"},{"key":"e_1_2_2_36_1","volume-title":"Automatically Generating Secure Wrappers for SGX Enclaves from Separation Logic Specifications","author":"van Ginkel Neline","unstructured":"Neline van Ginkel , Raoul Strackx , and Frank Piessens . 2017. Automatically Generating Secure Wrappers for SGX Enclaves from Separation Logic Specifications . In Programming Languages and Systems, Bor-Yuh Evan Chang (Ed.). Springer International Publishing , Cham , 105\u2013123. Neline van Ginkel, Raoul Strackx, and Frank Piessens. 2017. Automatically Generating Secure Wrappers for SGX Enclaves from Separation Logic Specifications. In Programming Languages and Systems, Bor-Yuh Evan Chang (Ed.). Springer International Publishing, Cham, 105\u2013123."},{"key":"e_1_2_2_37_1","volume-title":"Logical Methods in Computer Science 11, 3","author":"Vogels Fr\u00e9d\u00e9ric","year":"2015","unstructured":"Fr\u00e9d\u00e9ric Vogels , Bart Jacobs , and Frank Piessens . 2015. Featherweight VeriFast . Logical Methods in Computer Science 11, 3 ( 2015 ). Fr\u00e9d\u00e9ric Vogels, Bart Jacobs, and Frank Piessens. 2015. Featherweight VeriFast. Logical Methods in Computer Science 11, 3 (2015)."},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2015.9"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341688","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3341688","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:41:29Z","timestamp":1750200089000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341688"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,7,26]]},"references-count":37,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2019,7,26]]}},"alternative-id":["10.1145\/3341688"],"URL":"https:\/\/doi.org\/10.1145\/3341688","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,7,26]]},"assertion":[{"value":"2019-07-26","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}