{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T02:17:04Z","timestamp":1772158624665,"version":"3.50.1"},"reference-count":36,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2017,10,12]],"date-time":"2017-10-12T00:00:00Z","timestamp":1507766400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/summer-heart-0930.chufeiyun1688.workers.dev:443\/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":[[2017,10,12]]},"abstract":"<jats:p>\n            In scenarios such as web programming, where code is linked together from multiple sources,\n            <jats:italic>object capability patterns<\/jats:italic>\n            (OCPs) provide an essential safeguard, enabling programmers to protect the private state of their objects from corruption by unknown and untrusted code. However, the benefits of OCPs in terms of program verification have never been properly formalized. In this paper, building on the recently developed Iris framework for concurrent separation logic, we develop OCPL, the first program logic for compositionally specifying and verifying OCPs in a language with closures, mutable state, and concurrency. The key idea of OCPL is to account for the interface between verified and untrusted code by adopting a well-known idea from the literature on security protocol verification, namely\n            <jats:italic>robust safety<\/jats:italic>\n            . Programs that export only properly wrapped values to their environment can be proven robustly safe, meaning that their untrusted environment cannot violate their internal invariants. We use OCPL to give the first general, compositional, and machine-checked specs for several commonly-used OCPs\u2014including the\n            <jats:italic>dynamic sealing<\/jats:italic>\n            ,\n            <jats:italic>membrane<\/jats:italic>\n            , and\n            <jats:italic>caretaker<\/jats:italic>\n            patterns\u2014which we then use to verify robust safety for representative client code. All our results are fully mechanized in the Coq proof assistant.\n          <\/jats:p>","DOI":"10.1145\/3133913","type":"journal-article","created":{"date-parts":[[2017,10,13]],"date-time":"2017-10-13T15:15:45Z","timestamp":1507907745000},"page":"1-26","update-policy":"https:\/\/summer-heart-0930.chufeiyun1688.workers.dev:443\/https\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":41,"title":["Robust and compositional verification of object capability patterns"],"prefix":"10.1145","volume":"1","author":[{"given":"David","family":"Swasey","sequence":"first","affiliation":[{"name":"MPI-SWS, Germany"}]},{"given":"Deepak","family":"Garg","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}]},{"given":"Derek","family":"Dreyer","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}]}],"member":"320","published-online":{"date-parts":[[2017,10,12]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/324133.324266"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190235"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1101821.1101824"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/11531142_17"},{"key":"e_1_2_1_5_1","unstructured":"Adam Barth. 2011. The Web origin concept. RFC 6454. https:\/\/summer-heart-0930.chufeiyun1688.workers.dev:443\/https\/www.rfc- editor.org\/rfc\/rfc6454.txt  Adam Barth. 2011. The Web origin concept. RFC 6454. https:\/\/summer-heart-0930.chufeiyun1688.workers.dev:443\/https\/www.rfc- editor.org\/rfc\/rfc6454.txt"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1890028.1890031"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926401"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36946-9_3"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/286936.286947"},{"key":"e_1_2_1_10_1","volume-title":"Making JavaScript safe for advertising. (2008). Retrieved","author":"Crockford Douglas","year":"2017","unstructured":"Douglas Crockford . 2008. Making JavaScript safe for advertising. (2008). Retrieved April 2017 from https:\/\/summer-heart-0930.chufeiyun1688.workers.dev:443\/http\/www.adsafe.org\/ Douglas Crockford. 2008. Making JavaScript safe for advertising. (2008). Retrieved April 2017 from https:\/\/summer-heart-0930.chufeiyun1688.workers.dev:443\/http\/www.adsafe.org\/"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP.2016.22"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14107-2_24"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2786558.2786564"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90014-7"},{"key":"e_1_2_1_16_1","unstructured":"Google Inc. 2015. Caja membrane implementation. (Feb. 2015). https:\/\/summer-heart-0930.chufeiyun1688.workers.dev:443\/https\/github.com\/google\/caja\/blob\/master\/src\/com\/google\/ caja\/plugin\/taming- membrane.js  Google Inc. 2015. Caja membrane implementation. (Feb. 2015). https:\/\/summer-heart-0930.chufeiyun1688.workers.dev:443\/https\/github.com\/google\/caja\/blob\/master\/src\/com\/google\/ caja\/plugin\/taming- membrane.js"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2001.930143"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_2_1_19_1","doi-asserted-by":"crossref","unstructured":"Ralf Jung Robbert Krebbers Jacques-Henri Jourdan Ale\u0161 Bizjak Lars Birkedal and Derek Dreyer. 2017. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. (2017). Submitted for publication.  Ralf Jung Robbert Krebbers Jacques-Henri Jourdan Ale\u0161 Bizjak Lars Birkedal and Derek Dreyer. 2017. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. (2017). Submitted for publication.","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_2_1_23_1","volume-title":"Proceedings of the Network and Distributed System Security Symposium (NDSS \u201910)","author":"Mettler Adrian","year":"2010","unstructured":"Adrian Mettler , David Wagner , and Tyler Close . 2010 . Joe-E: A security-oriented subset of Java . In Proceedings of the Network and Distributed System Security Symposium (NDSS \u201910) . Adrian Mettler, David Wagner, and Tyler Close. 2010. Joe-E: A security-oriented subset of Java. In Proceedings of the Network and Distributed System Security Symposium (NDSS \u201910)."},{"key":"e_1_2_1_24_1","unstructured":"Mark Samuel Miller. 2006. Robust Composition: Towards a Unified Approach to Access Control and Concurrency Control. Ph.D. Dissertation. Johns Hopkins University.  Mark Samuel Miller. 2006. Robust Composition: Towards a Unified Approach to Access Control and Concurrency Control. Ph.D. Dissertation. Johns Hopkins University."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_1"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/647504.728481"},{"key":"e_1_2_1_27_1","volume-title":"Caja: Safe active content in sanitized JavaScript. (June","author":"Miller Mark S.","year":"2008","unstructured":"Mark S. Miller , Mike Samuel , Ben Laurie , Ihab Awad , and Mike Stay . 2008 . Caja: Safe active content in sanitized JavaScript. (June 2008). Mark S. Miller, Mike Samuel, Ben Laurie, Ihab Awad, and Mike Stay. 2008. Caja: Safe active content in sanitized JavaScript. (June 2008)."},{"key":"e_1_2_1_28_1","first-page":"224","article-title":"Paradigm regained: Abstraction mechanisms for access control. In Advances in Computing Science \u2013 ASIAN 2003 Programming Languages and Distributed Computation, 8th Asian Computing Science Conference (ASIAN \u201903)","volume":"2896","author":"Miller Mark S.","year":"2003","unstructured":"Mark S. Miller and Jonathan S. Shapiro . 2003 . Paradigm regained: Abstraction mechanisms for access control. In Advances in Computing Science \u2013 ASIAN 2003 Programming Languages and Distributed Computation, 8th Asian Computing Science Conference (ASIAN \u201903) . Springer LNCS 2896 , 224 \u2013 242 . Mark S. Miller and Jonathan S. Shapiro. 2003. Paradigm regained: Abstraction mechanisms for access control. In Advances in Computing Science \u2013 ASIAN 2003 Programming Languages and Distributed Computation, 8th Asian Computing Science Conference (ASIAN \u201903). Springer LNCS 2896, 224\u2013242.","journal-title":"Springer LNCS"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/361932.361937"},{"key":"e_1_2_1_30_1","volume-title":"Script security. (Aug","year":"2016","unstructured":"Mozilla. 2016. Script security. (Aug . 2016 ). https:\/\/summer-heart-0930.chufeiyun1688.workers.dev:443\/https\/developer.mozilla.org\/en- US\/docs\/Mozilla\/Gecko\/Script_security Overview of the Firefox membrane. Mozilla. 2016. Script security. (Aug. 2016). https:\/\/summer-heart-0930.chufeiyun1688.workers.dev:443\/https\/developer.mozilla.org\/en- US\/docs\/Mozilla\/Gecko\/Script_security Overview of the Firefox membrane."},{"key":"e_1_2_1_32_1","volume-title":"Long version of this paper (with appendices) and Coq development. (Sept","author":"OCPL","year":"2017","unstructured":"OCPL 2017. Long version of this paper (with appendices) and Coq development. (Sept . 2017 ). Available at the Iris project website at https:\/\/summer-heart-0930.chufeiyun1688.workers.dev:443\/http\/iris- project.org . OCPL 2017. Long version of this paper (with appendices) and Coq development. (Sept. 2017). Available at the Iris project website at https:\/\/summer-heart-0930.chufeiyun1688.workers.dev:443\/http\/iris- project.org ."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21461-5_19"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-140504"},{"key":"e_1_2_1_36_1","volume-title":"Proceedings of the Second International Conference on Multiparadigm Programming in Mozart\/Oz (MOZ \u201904)","author":"Spiessens Fred","year":"2004","unstructured":"Fred Spiessens and Peter Van Roy . 2004 . The Oz-E project: Design guidelines for a secure multiparadigm programming language . In Proceedings of the Second International Conference on Multiparadigm Programming in Mozart\/Oz (MOZ \u201904) . 21\u201340. Fred Spiessens and Peter Van Roy. 2004. The Oz-E project: Design guidelines for a secure multiparadigm programming language. In Proceedings of the Second International Conference on Multiparadigm Programming in Mozart\/Oz (MOZ \u201904). 21\u201340."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/11580850_14"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964015"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39038-8_7"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/summer-heart-0930.chufeiyun1688.workers.dev:443\/https\/dl.acm.org\/doi\/10.1145\/3133913","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/summer-heart-0930.chufeiyun1688.workers.dev:443\/https\/dl.acm.org\/doi\/pdf\/10.1145\/3133913","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:13:25Z","timestamp":1750212805000},"score":1,"resource":{"primary":{"URL":"https:\/\/summer-heart-0930.chufeiyun1688.workers.dev:443\/https\/dl.acm.org\/doi\/10.1145\/3133913"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,10,12]]},"references-count":36,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2017,10,12]]}},"alternative-id":["10.1145\/3133913"],"URL":"https:\/\/summer-heart-0930.chufeiyun1688.workers.dev:443\/https\/doi.org\/10.1145\/3133913","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,10,12]]},"assertion":[{"value":"2017-10-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}