{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T20:51:18Z","timestamp":1760043078670,"version":"3.40.3"},"publisher-location":"Cham","reference-count":61,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030452339"},{"type":"electronic","value":"9783030452346"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-45234-6_21","type":"book-chapter","created":{"date-parts":[[2020,4,20]],"date-time":"2020-04-20T14:04:23Z","timestamp":1587391463000},"page":"420-440","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Holistic Specifications for Robust Programs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1993-1142","authenticated-orcid":false,"given":"Sophia","family":"Drossopoulou","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9036-5692","authenticated-orcid":false,"given":"James","family":"Noble","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3098-3901","authenticated-orcid":false,"given":"Julian","family":"Mackay","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9072-6689","authenticated-orcid":false,"given":"Susan","family":"Eisenbach","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,4,17]]},"reference":[{"key":"21_CR1","unstructured":"Holistic specifications paper with appendices. https:\/\/arxiv.org\/abs\/2002.08334 , accessed: 2020\u201302-21"},{"key":"21_CR2","doi-asserted-by":"crossref","unstructured":"Ahmed, A., Dreyer, D., Rossberg, A.: State-dependent representation independence. In: POPL (2009)","DOI":"10.1145\/1480881.1480925"},{"key":"21_CR3","doi-asserted-by":"crossref","unstructured":"Banerjee, A., Naumann, D.A.: Ownership confinement ensures representation independence for object-oriented programs. J. ACM 52(6), 894\u2013960 (Nov 2005)","DOI":"10.1145\/1101821.1101824"},{"key":"21_CR4","doi-asserted-by":"crossref","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: CASSIS. pp. 49\u201369. LNCS, Springer (2005)","DOI":"10.1007\/978-3-540-30569-9_3"},{"key":"21_CR5","unstructured":"BBC: On This Day: 1984: Tory cabinet in Brighton bomb blast (2015), [Online; accessed 15-October-2015]"},{"key":"21_CR6","doi-asserted-by":"crossref","unstructured":"Bengtson, J., Bhargavan, K., Fournet, C., Gordon, A.D., Maffeis, S.: Refinement types for secure implementations. ACM Trans. Program. Lang. Syst. 33(2), 8:1\u20138:45 (Feb 2011)","DOI":"10.1145\/1890028.1890031"},{"key":"21_CR7","doi-asserted-by":"crossref","unstructured":"Black, A., Bruce, K., Homer, M., Noble, J.: Grace: the Absence of (Inessential) Difficulty. In: Onwards (2012)","DOI":"10.1145\/2384592.2384601"},{"key":"21_CR8","unstructured":"Bracha, G.: The Dart Programming Language (Dec 2015)"},{"key":"21_CR9","unstructured":"Bracha, G.: The Newspeak language specification version 0.1 (Feb 2017), newspeaklanguage.org\/"},{"key":"21_CR10","unstructured":"Burtsev, A., Johnson, D., Kunz, J., Eide, E., van der Merwe, J.E.: Capnet: security and least authority in a capability-enabled cloud. In: Proceedings of the 2017 Symposium on Cloud Computing, SoCC 2017, Santa Clara, CA, USA, September 24\u201327, 2017. pp. 128\u2013141 (2017)"},{"key":"21_CR11","doi-asserted-by":"crossref","unstructured":"Chalin, P., Kiniry, J.R., Leavens, G.T., Poll, E.: Beyond assertions: Advanced specification and verification with JML and esc\/java2. In: Formal Methods for Components and Objects, 4th International Symposium, FMCO 2005, Amsterdam, The Netherlands, November 1\u20134, 2005, Revised Lectures. pp. 342\u2013363 (2005), https:\/\/doi.org\/10.1007\/11804192_16","DOI":"10.1007\/11804192_16"},{"key":"21_CR12","unstructured":"Christoph Jentsch: Decentralized autonomous organization to automate governance (Mar 2016), https:\/\/download.slock.it\/public\/DAO\/WhitePaper.pdf"},{"key":"21_CR13","doi-asserted-by":"crossref","unstructured":"Clarke, D., Drossopoulou, S.: Ownership, encapsulation and the disjointness of type and effectr. In: OOPSLA. ACM (2002)","DOI":"10.1145\/582419.582447"},{"key":"21_CR14","doi-asserted-by":"crossref","unstructured":"Clarke, D.G., Potter, J.M., James Noble: Ownership types for flexible alias protection. In: OOPSLA. ACM (1998)","DOI":"10.1145\/286936.286947"},{"key":"21_CR15","unstructured":"Coindesk: Understanding the DAO attack (2016), www.coindesk.com\/understanding-dao-hack-journalists\/"},{"key":"21_CR16","unstructured":"Community, S.: Solidity, https:\/\/solidity.readthedocs.io\/en\/develop\/"},{"key":"21_CR17","unstructured":"van Cutsem, T.: Membranes in Javascript (2012), available from prog.vub.ac.be\/tvcutsem\/invokedynamic\/js-membranes"},{"key":"21_CR18","unstructured":"Cutsem, T.V., S, M.: Trustworthy proxies: Virtualizing objects with invariants. In: ECOOP (2013)"},{"key":"21_CR19","doi-asserted-by":"crossref","unstructured":"Dennis, J.B., Horn, E.C.V.: Programming Semantics for Multiprogrammed Computations. Comm. ACM 9(3) (1966)","DOI":"10.1145\/365230.365252"},{"key":"21_CR20","doi-asserted-by":"crossref","unstructured":"Devriese, D., Birkedal, L., Piessens, F.: Reasoning about object capabilities with logical relations and effect parametricity. In: IEEE EuroS&P. pp. 147\u2013162 (2016). http:\/\/doi.org\/10.1109\/EuroSP.2016.22","DOI":"10.1109\/EuroSP.2016.22"},{"key":"21_CR21","doi-asserted-by":"crossref","unstructured":"Drossopoulou, S., Noble, J.: The need for capability policies. In: (FTfJP) (2013)","DOI":"10.1145\/2489804.2489811"},{"key":"21_CR22","unstructured":"Drossopoulou, S., Noble, J.: Towards capability policy specification and verification (May 2014), ecs.victoria.ac.nz\/Main\/TechnicalReportSeries"},{"key":"21_CR23","doi-asserted-by":"publisher","unstructured":"Drossopoulou, S., Noble, J., Mackay, J., Eisenbach, S.: Holisitic Specifications for Robust Programs - Coq Model (2020). https:\/\/doi.org\/10.5281\/zenodo.3677621","DOI":"10.5281\/zenodo.3677621"},{"key":"21_CR24","doi-asserted-by":"crossref","unstructured":"Drossopoulou, S., Noble, J., Miller, M.: Swapsies on the internet: First steps towards reasoning about risk and trust in an open world. In: (PLAS) (2015)","DOI":"10.1145\/2786558.2786564"},{"key":"21_CR25","doi-asserted-by":"crossref","unstructured":"Guttag, J.V., Horning, J.J.: Larch: Languages and Tools for Formal Specification. Springer (1993)","DOI":"10.1007\/978-1-4612-2704-5"},{"key":"21_CR26","doi-asserted-by":"crossref","unstructured":"Hatcliff, J., Leavens, G.T., Leino, K.R.M., M\u00fcller, P., Parkinson, M.J.: Behavioral interface specification languages. ACM Comput. Surv. 44(3), 16 (2012)","DOI":"10.1145\/2187671.2187678"},{"key":"21_CR27","doi-asserted-by":"crossref","unstructured":"Hayes, I.J., Wu, X., Meinicke, L.A.: Capabilities for Java: Secure access to resources. In: APLAS. pp. 67\u201384 (2017)","DOI":"10.1007\/978-3-319-71237-6_4"},{"key":"21_CR28","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Comm. ACM 12, 576\u2013580 (1969)","journal-title":"Comm. ACM"},{"key":"21_CR29","doi-asserted-by":"crossref","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall (1985)","DOI":"10.1007\/978-3-642-82921-5_4"},{"key":"21_CR30","unstructured":"Jones, T., Homer, M., James Noble, Bruce, K.B.: Object inheritance without classes. In: ECOOP. pp. 13:1\u201313:26 (2016)"},{"key":"21_CR31","unstructured":"Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D.R., M\u00fcller, P., Kiniry, J., Chalin, P.: JML Reference Manual (February 2007), iowa State Univ. www.jmlspecs.org"},{"key":"21_CR32","doi-asserted-by":"crossref","unstructured":"Leino, K.R.: Dafny: An automatic program verifier for functional correctness. In: LPAR16. Springer (April 2010)","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"21_CR33","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M., Schulte, W.: Using history invariants to verify observers. In: ESOP (2007)","DOI":"10.1007\/978-3-540-71316-6_7"},{"key":"21_CR34","doi-asserted-by":"crossref","unstructured":"Lewis, D.: Causation. Journal of Philosophy 70(17) (1973)","DOI":"10.2307\/2025310"},{"key":"21_CR35","doi-asserted-by":"crossref","unstructured":"Maffeis, S., Mitchell, J., Taly, A.: Object capabilities and isolation of untrusted web applications. In: Proc of IEEE Security and Privacy (2010)","DOI":"10.1109\/SP.2010.16"},{"key":"21_CR36","unstructured":"Melicher, D., Shi, Y., Potanin, A., Aldrich, J.: A capability-based module system for authority control. In: ECOOP. pp. 20:1\u201320:27 (2017)"},{"key":"21_CR37","unstructured":"Meyer, B.: Eiffel: The Language. Prentice Hall (1992)"},{"key":"21_CR38","unstructured":"Meyer, B.: Object-Oriented Software Construction, Second Edition. Prentice Hall, second edn. (1997)"},{"key":"21_CR39","doi-asserted-by":"crossref","unstructured":"Miller, M.S., Cutsem, T.V., Tulloh, B.: Distributed electronic rights in JavaScript. In: ESOP (2013)","DOI":"10.1007\/978-3-642-37036-6_1"},{"key":"21_CR40","unstructured":"Miller, M.S.: Robust Composition: Towards a Unified Approach to Access Control and Concurrency Control. Ph.D. thesis, Baltimore, Maryland (2006)"},{"key":"21_CR41","doi-asserted-by":"crossref","unstructured":"Miller, M.S., Morningstar, C., Frantz, B.: Capability-based Financial Instruments: From Object to Capabilities. In: Financial Cryptography. Springer (2000)","DOI":"10.1007\/3-540-45472-1_24"},{"key":"21_CR42","unstructured":"Miller, M.S., Samuel, M., Laurie, B., Awad, I., Stay, M.: Safe active content in sanitized JavaScript (2008), code.google.com\/p\/google-caja\/"},{"key":"21_CR43","unstructured":"Mitre Organisation: CWE-830: Inclusion of Web Functionality from an Untrusted Source (2019), https:\/\/cwe.mitre.org\/data\/definitions\/830.html"},{"key":"21_CR44","doi-asserted-by":"crossref","unstructured":"Morris Jr., J.H.: Protection in programming languages. CACM 16(1) (1973)","DOI":"10.1145\/361932.361937"},{"key":"21_CR45","doi-asserted-by":"crossref","unstructured":"M\u00fcller, P., Poetzsch-Heffter, A., Leavens, G.T.: Modular invariants for layered object structures. Science of Computer Programming 62, 253\u2013286 (2006)","DOI":"10.1016\/j.scico.2006.03.001"},{"key":"21_CR46","doi-asserted-by":"crossref","unstructured":"Murray, T.: Analysing the Security Properties of Object-Capability Patterns. Ph.D. thesis, University of Oxford (2010)","DOI":"10.1007\/978-3-642-12459-4_7"},{"key":"21_CR47","doi-asserted-by":"crossref","unstructured":"Murray, T., Sison, R., Engelhardt, K.: Covern: A logic for compositional verification of information flow control. In: EuroS&P (2018)","DOI":"10.1109\/EuroSP.2018.00010"},{"key":"21_CR48","doi-asserted-by":"crossref","unstructured":"Noble, J., Drossopoulou, S.: Rationally reconstructing the escrow example. In: FTfJP (2014)","DOI":"10.1145\/2635631.2635850"},{"key":"21_CR49","doi-asserted-by":"crossref","unstructured":"Noble, J., Potanin, A., Murray, T., Miller, M.S.: Abstract and concrete data types vs object capabilities. In: M\u00fcller, P., Schaefer, I. (eds.) Principled Software Development (2018)","DOI":"10.1007\/978-3-319-98047-8_14"},{"key":"21_CR50","doi-asserted-by":"crossref","unstructured":"Noble, J., Potter, J., Vitek, J.: Flexible alias protection. In: ECOOP (Jul 1998)","DOI":"10.1007\/BFb0054091"},{"key":"21_CR51","doi-asserted-by":"crossref","unstructured":"Pearce, D., Groves, L.: Designing a verifying compiler: Lessons learned from developing Whiley. Sci. Comput. Prog. (2015)","DOI":"10.1016\/j.scico.2015.09.006"},{"key":"21_CR52","doi-asserted-by":"crossref","unstructured":"Permenev, A., Dimitrov, D., Tsankov, P., Drachsler-Cohen, D., Vechev, M.: VerX: Safety verification of smart contracts. In: IEEE Symp. on Security and Privacy (2020)","DOI":"10.1109\/SP40000.2020.00024"},{"key":"21_CR53","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS. pp. 55\u201374. IEEE Computer Society (2002)"},{"key":"21_CR54","doi-asserted-by":"crossref","unstructured":"Rhodes, D., Disney, T., Flanagan, C.: Dynamic detection of object capability violations through model checking. In: DLS. pp. 103\u2013112 (2014)","DOI":"10.1145\/2775052.2661099"},{"key":"21_CR55","unstructured":"Schaefer, I., Runge, T., Kn\u00fcppel, A., Cleophas, L., Kourie, D.G., Watson, B.W.: Towards confidentiality-by-construction. In: Leveraging Applications of Formal Methods, Verification and Validation. Modeling - 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5\u20139, 2018, Proceedings, Part I. pp. 502\u2013515 (2018)"},{"key":"21_CR56","doi-asserted-by":"crossref","unstructured":"Sergey, I., Nagaraj, V., Johannsen, J., Kumar, A., Trunov, A., Chan, K.: Safer smart contract programming with Scilla. In: OOPSLA (2019)","DOI":"10.1145\/3360611"},{"key":"21_CR57","doi-asserted-by":"crossref","unstructured":"Smans, J., Jacobs, B., Piessens, F.: Implicit Dynamic Frames. ToPLAS (2012)","DOI":"10.1145\/2160910.2160911"},{"key":"21_CR58","doi-asserted-by":"crossref","unstructured":"Summers, A.J., Drossopoulou, S.: Considerate Reasoning and the Composite Pattern. In: VMCAI (2010)","DOI":"10.1007\/978-3-642-11319-2_24"},{"key":"21_CR59","doi-asserted-by":"crossref","unstructured":"Swasey, D., Garg, D., Dreyer, D.: Robust and Compositional Verification of Object Capability Patterns. In: OOPSLA (2017)","DOI":"10.1145\/3133913"},{"key":"21_CR60","unstructured":"Talpin, J.P., Jouvelot, P.: The Type and Effect Discipline. In: LICS. pp. 162\u2013173 (1992)"},{"key":"21_CR61","unstructured":"The Ethereum Wiki: ERC20 Token Standard (Dec 2018), https:\/\/theethereum.wiki\/w\/index.php\/ERC20_Token_Standard"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-45234-6_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,10,21]],"date-time":"2022-10-21T20:36:17Z","timestamp":1666384577000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-45234-6_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030452339","9783030452346"],"references-count":61,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-45234-6_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"17 April 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FASE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Fundamental Approaches to Software Engineering","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Dublin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ireland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 April 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 April 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fase2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2020\/fase","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"81","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"23","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"28% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference could not take place due to the COVID-19 pandemic. There was an online event on July 2, 2020.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}