{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,23]],"date-time":"2025-12-23T00:29:55Z","timestamp":1766449795865,"version":"3.28.0"},"reference-count":44,"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.9919645","type":"proceedings-article","created":{"date-parts":[[2022,11,4]],"date-time":"2022-11-04T01:29:20Z","timestamp":1667525360000},"page":"80-95","source":"Crossref","is-referenced-by-count":4,"title":["Proving full-system security properties under multiple attacker models on capability machines"],"prefix":"10.1109","author":[{"given":"Thomas","family":"Van Strydonck","sequence":"first","affiliation":[{"name":"KU Leuven"}]},{"given":"A\u00efna Linn","family":"Georges","sequence":"additional","affiliation":[{"name":"Aarhus University"}]},{"given":"Arma\u00ebl","family":"Gueneau","sequence":"additional","affiliation":[{"name":"Aarhus University"}]},{"given":"Alix","family":"Trieu","sequence":"additional","affiliation":[{"name":"Aarhus University"}]},{"given":"Amin","family":"Timany","sequence":"additional","affiliation":[{"name":"Aarhus University"}]},{"given":"Frank","family":"Piessens","sequence":"additional","affiliation":[{"name":"KU Leuven"}]},{"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[{"name":"Aarhus University"}]},{"given":"Dominique","family":"Devriese","sequence":"additional","affiliation":[{"name":"Vrije Universiteit,KU Leuven,Brussel"}]}],"member":"263","reference":[{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2010.16"},{"key":"ref13","volume":"3","author":"skorstengaard","year":"2019","journal-title":"Stktokens Enforcing well-bracketed control flow and stack encapsulation using linear capabilities"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1109\/DSNW.2011.5958796"},{"key":"ref12","first-page":"5:1","article-title":"Reasoning about a Machine with Local Capabilities: Provably Safe Stack and Return Pointer Management","volume":"42","author":"skorstengaard","year":"2019","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1145\/268998.266668"},{"year":"2019","key":"ref15","article-title":"SAM D5x\/E5x Family Data Sheet"},{"key":"ref36","article-title":"Robust composition: Towards a unified approach to access control and concurrency control","author":"miller","year":"2006","journal-title":"Report of Johns Hopkins University"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1145\/1508293.1508311"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908101"},{"key":"ref30","first-page":"23","article-title":"VCC: A practical system for verifying concurrent C","author":"cohen","year":"0","journal-title":"Theorem Proving in Higher Order Logics Ser Lecture Notes in Computer Science"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1145\/238721.238769"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1145\/3434287"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9446-0"},{"key":"ref10","first-page":"475","article-title":"Reasoning about a machine with local capabilities - provably safe stack and return pointer management","author":"skorstengaard","year":"2018","journal-title":"Programming Languages and Systems - 27th European Symposium on Programming ESOP 2018"},{"key":"ref2","article-title":"The turtles project: Design and implementation of nested virtualization","author":"ben-yehuda","year":"2010","journal-title":"OSDI"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1145\/2592798.2592812"},{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1145\/2505123"},{"journal-title":"The Geometry of Innocent Flesh on the Bone Return-into-libc without Function Calls (on the x86)","year":"2007","author":"shacham","key":"ref17"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD.2018.00023"},{"article-title":"Proving full-system security properties under multiple attacker models on capability machines: Coq mechanization","year":"2021","author":"van strydonck","key":"ref16"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926417"},{"article-title":"The Iris documentation and Coq development","year":"2021","author":"team","key":"ref18"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2015.38"},{"key":"ref23","volume":"4","author":"sammler","year":"2019","journal-title":"The high-level benefits of low-level sandboxing"},{"key":"ref26","first-page":"86","article-title":"Intel SGX explained","volume":"2016","author":"costan","year":"2016","journal-title":"IACR Cryptology ePrint Archive"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676972"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28891-3_21"},{"key":"ref20","first-page":"108","article-title":"Higher-order concurrent abstract predicates","author":"svendsen","year":"2012","journal-title":"Modular specification and verification for higher-order languages with state"},{"key":"ref41","first-page":"35","article-title":"SLAM2: static driver verification with under 4% false alarms","author":"ball","year":"2010","journal-title":"International Conference on Formal Methods In Computer-Aided Design"},{"journal-title":"Arm Architecture Reference Manual Supplement Morello for A-profile Architecture","year":"2020","author":"limited","key":"ref44"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1109\/85.601735"},{"journal-title":"Position paper Defending direct memory access with CHERI capabilities","year":"2020","author":"markettos","key":"ref43"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"ref28","first-page":"207","article-title":"se14: formal verification of an OS kernel","author":"klein","year":"2009","journal-title":"Symposium on Operating Systems Principles 2009"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1145\/3079763"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1145\/1743546.1743574"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1145\/3133913"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP.2016.22"},{"key":"ref9","article-title":"Linear capabilities for fully abstract compilation of separation-logic-verified code","volume":"ic","author":"van strydonck","year":"0","journal-title":"Proc ACM Program Lang"},{"journal-title":"Capability-Based Computer Systems","year":"1984","author":"levy","key":"ref4"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2015.55"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2015.9"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1145\/195473.195579"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2016.11"}],"event":{"name":"2022 IEEE 35th Computer Security Foundations Symposium (CSF)","start":{"date-parts":[[2022,8,7]]},"location":"Haifa, Israel","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\/09919645.pdf?arnumber=9919645","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,8]],"date-time":"2023-11-08T23:19:35Z","timestamp":1699485575000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9919645\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8]]},"references-count":44,"URL":"https:\/\/doi.org\/10.1109\/csf54842.2022.9919645","relation":{},"subject":[],"published":{"date-parts":[[2022,8]]}}}