{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,30]],"date-time":"2026-09-30T03:23:38Z","timestamp":1790738618832,"version":"4.1.0"},"reference-count":59,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T00:00:00Z","timestamp":1667174400000},"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":[[2022,10,31]]},"abstract":"<jats:p>Robust modules guarantee to do only what they are supposed to do \u2013 even in the presence of untrusted malicious clients, and considering not just the direct behaviour of individual methods, but also the emergent behaviour from calls to more than one method. Necessity is a language for specifying robustness, based on novel necessity operators capturing temporal implication, and a proof logic that derives explicit robustness specifications from functional specifications. Soundness and an exemplar proof are mechanised in Coq.<\/jats:p>","DOI":"10.1145\/3563317","type":"journal-article","created":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T20:23:35Z","timestamp":1667247815000},"page":"811-840","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["<i>Necessity<\/i>\n            specifications for robustness"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3098-3901","authenticated-orcid":false,"given":"Julian","family":"Mackay","sequence":"first","affiliation":[{"name":"Victoria University of Wellington, New Zealand"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9072-6689","authenticated-orcid":false,"given":"Susan","family":"Eisenbach","sequence":"additional","affiliation":[{"name":"Imperial College London, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9036-5692","authenticated-orcid":false,"given":"James","family":"Noble","sequence":"additional","affiliation":[{"name":"Creative Research &amp; Programming, New Zealand"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1993-1142","authenticated-orcid":false,"given":"Sophia","family":"Drossopoulou","sequence":"additional","affiliation":[{"name":"Meta, UK \/ Imperial College London, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,10,31]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428277"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3491216"},{"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","doi-asserted-by":"publisher","DOI":"10.1145\/3473586"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485523"},{"key":"e_1_2_1_7_1","volume-title":"The Stanford Encyclopedia of Philosophy (Spring 2022 ed.), Edward N","author":"Bra\u00fcner Torben","unstructured":"Torben Bra\u00fcner . 2022. Hybrid Logic . In The Stanford Encyclopedia of Philosophy (Spring 2022 ed.), Edward N . Zalta (Ed.). Torben Bra\u00fcner. 2022. Hybrid Logic. In The Stanford Encyclopedia of Philosophy (Spring 2022 ed.), Edward N. Zalta (Ed.)."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_13"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2011.13"},{"key":"e_1_2_1_10_1","unstructured":"Adam Chlipala. 2019. Certified Programming with Dependent Types. http:\/\/adam.chlipala.net\/cpdt\/ \t\t\t\t  Adam Chlipala. 2019. Certified Programming with Dependent Types. http:\/\/adam.chlipala.net\/cpdt\/"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/583854.582447"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/286936.286947"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45337-7_4"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3297858.3304042"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24690-6_12"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP.2016.22"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2014.9"},{"key":"e_1_2_1_18_1","unstructured":"Sophia Drossopoulou and James Noble. 2014. Towards Capability Policy Specification and Verification. \u00a7mall ecs.victoria.ac.nz\/Main\/TechnicalReportSeries \t\t\t\t  Sophia Drossopoulou and James Noble. 2014. Towards Capability Policy Specification and Verification. \u00a7mall ecs.victoria.ac.nz\/Main\/TechnicalReportSeries"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.3677621"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45234-6_21"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2786558.2786564"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2007.7"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2001.930143"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158136"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2187671.2187678"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_27_1","volume-title":"Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Pearson.","author":"Lamport Leslie","year":"2002","unstructured":"Leslie Lamport . 2002 . Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Pearson. Leslie Lamport. 2002. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Pearson."},{"key":"e_1_2_1_28_1","unstructured":"G. T. Leavens E. Poll C. Clifton Y. Cheon C. Ruby D. R. Cok P. M\u00fcller J. Kiniry and P. Chalin. 2007. JML Reference Manual. February Iowa State Univ. www.jmlspecs.org \t\t\t\t  G. T. Leavens E. Poll C. Clifton Y. Cheon C. Ruby D. R. Cok P. M\u00fcller J. Kiniry and P. Chalin. 2007. JML Reference Manual. February Iowa State Univ. www.jmlspecs.org"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2013.6606754"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24851-4_22"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71316-6_7"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.2307\/2025310"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7087932"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7087913"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2010.16"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.161279"},{"key":"e_1_2_1_38_1","volume-title":"Robust Composition: Towards a Unified Approach to Access Control and Concurrency Control. Ph. D. Dissertation.","author":"Miller Mark Samuel","year":"2006","unstructured":"Mark Samuel Miller . 2006 . Robust Composition: Towards a Unified Approach to Access Control and Concurrency Control. Ph. D. Dissertation. Baltimore, Maryland . Mark Samuel Miller. 2006. Robust Composition: Towards a Unified Approach to Access Control and Concurrency Control. Ph. D. Dissertation. Baltimore, Maryland."},{"key":"e_1_2_1_39_1","unstructured":"Mark Samuel Miller. 2011. Secure Distributed Programming with Object-capabilities in JavaScript. Oct. Talk at Vrije Universiteit Brussel mobicrant-talks.eventbrite.com \t\t\t\t  Mark Samuel Miller. 2011. Secure Distributed Programming with Object-capabilities in JavaScript. Oct. Talk at Vrije Universiteit Brussel mobicrant-talks.eventbrite.com"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_1"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45472-1_24"},{"key":"e_1_2_1_42_1","unstructured":"Mark Samuel Miller Mike Samuel Ben Laurie Ihab Awad and Mike Stay. 2008. Safe active content in sanitized JavaScript. code.google.com\/p\/google-caja\/ \t\t\t\t  Mark Samuel Miller Mike Samuel Ben Laurie Ihab Awad and Mike Stay. 2008. Safe active content in sanitized JavaScript. code.google.com\/p\/google-caja\/"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3022671.2984021"},{"key":"e_1_2_1_44_1","volume-title":"Analysing the Security Properties of Object-Capability Patterns. Ph. D. Dissertation","author":"Murray Toby","unstructured":"Toby Murray . 2010. Analysing the Security Properties of Object-Capability Patterns. Ph. D. Dissertation . University of Oxford. Toby Murray. 2010. Analysing the Security Properties of Object-Capability Patterns. Ph. D. Dissertation. University of Oxford."},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35308-6_12"},{"key":"e_1_2_1_46_1","unstructured":"James Noble Robert Biddle Ewan Tempero Alex Potanin and Dave Clarke. 2003. Towards a Model of Encapsulation. In IWACO. \t\t\t\t  James Noble Robert Biddle Ewan Tempero Alex Potanin and Dave Clarke. 2003. Towards a Model of Encapsulation. In IWACO."},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054091"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371078"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3436809"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2015.09.006"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00024"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_14"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371100"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03418-4_30"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11319-2_24"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133913"},{"key":"e_1_2_1_57_1","volume-title":"Arma\u00ebl Gu\u00e9neau, Alix Trieu, Amin Timany, Frank Piessens, Lars Birkedal, and Dominique Devriese.","author":"Strydonck Thomas Van","year":"2022","unstructured":"Thomas Van Strydonck , A\u2208a Linn Georges , Arma\u00ebl Gu\u00e9neau, Alix Trieu, Amin Timany, Frank Piessens, Lars Birkedal, and Dominique Devriese. 2022 . Proving full-system security properties under multiple attacker models on capability machines. Thomas Van Strydonck, A\u2208a Linn Georges, Arma\u00ebl Gu\u00e9neau, Alix Trieu, Amin Timany, Frank Piessens, Lars Birkedal, and Dominique Devriese. 2022. Proving full-system security properties under multiple attacker models on capability machines."},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/320385.320392"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45309-1_4"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563317","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3563317","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:38:10Z","timestamp":1750178290000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563317"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10,31]]},"references-count":59,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2022,10,31]]}},"alternative-id":["10.1145\/3563317"],"URL":"https:\/\/doi.org\/10.1145\/3563317","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,10,31]]},"assertion":[{"value":"2022-10-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}