Abstract
Functional specifications describe what program components can do: the sufficient conditions to invoke components’ operations. They allow us to reason about the use of components in a closed world setting, where components interact with known client code, and where the client code must establish the appropriate pre-conditions before calling into a component.
Sufficient conditions are not enough to reason about the use of components in an open world setting, where components interact with external code, possibly of unknown provenance, and where components may evolve over time. In this open world setting, we must also consider the necessary conditions, i. e. what are the conditions without which an effect will not happen.
In this paper we propose the \({\mathcal {C}}\)hainmail specification language for writing holistic specifications that focus on necessary conditions (as well as sufficient conditions). We give a formal semantics for \({\mathcal {C}}\)hainmail, and discuss several examples. The core of \({\mathcal {C}}\)hainmail has been mechanised in the Coq proof assistant.
Chapter PDF
Similar content being viewed by others
References
Holistic specifications paper with appendices. https://arxiv.org/abs/2002.08334, accessed: 2020–02-21
Ahmed, A., Dreyer, D., Rossberg, A.: State-dependent representation independence. In: POPL (2009)
Banerjee, A., Naumann, D.A.: Ownership confinement ensures representation independence for object-oriented programs. J. ACM 52(6), 894–960 (Nov 2005)
Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: CASSIS. pp. 49–69. LNCS, Springer (2005)
BBC: On This Day: 1984: Tory cabinet in Brighton bomb blast (2015), [Online; accessed 15-October-2015]
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–8:45 (Feb 2011)
Black, A., Bruce, K., Homer, M., Noble, J.: Grace: the Absence of (Inessential) Difficulty. In: Onwards (2012)
Bracha, G.: The Dart Programming Language (Dec 2015)
Bracha, G.: The Newspeak language specification version 0.1 (Feb 2017), newspeaklanguage.org/
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–27, 2017. pp. 128–141 (2017)
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–4, 2005, Revised Lectures. pp. 342–363 (2005), https://doi.org/10.1007/11804192_16
Christoph Jentsch: Decentralized autonomous organization to automate governance (Mar 2016), https://download.slock.it/public/DAO/WhitePaper.pdf
Clarke, D., Drossopoulou, S.: Ownership, encapsulation and the disjointness of type and effectr. In: OOPSLA. ACM (2002)
Clarke, D.G., Potter, J.M., James Noble: Ownership types for flexible alias protection. In: OOPSLA. ACM (1998)
Coindesk: Understanding the DAO attack (2016), www.coindesk.com/understanding-dao-hack-journalists/
Community, S.: Solidity, https://solidity.readthedocs.io/en/develop/
van Cutsem, T.: Membranes in Javascript (2012), available from prog.vub.ac.be/tvcutsem/invokedynamic/js-membranes
Cutsem, T.V., S, M.: Trustworthy proxies: Virtualizing objects with invariants. In: ECOOP (2013)
Dennis, J.B., Horn, E.C.V.: Programming Semantics for Multiprogrammed Computations. Comm. ACM 9(3) (1966)
Devriese, D., Birkedal, L., Piessens, F.: Reasoning about object capabilities with logical relations and effect parametricity. In: IEEE EuroS&P. pp. 147–162 (2016). http://doi.org/10.1109/EuroSP.2016.22
Drossopoulou, S., Noble, J.: The need for capability policies. In: (FTfJP) (2013)
Drossopoulou, S., Noble, J.: Towards capability policy specification and verification (May 2014), ecs.victoria.ac.nz/Main/TechnicalReportSeries
Drossopoulou, S., Noble, J., Mackay, J., Eisenbach, S.: Holisitic Specifications for Robust Programs - Coq Model (2020). https://doi.org/10.5281/zenodo.3677621
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)
Guttag, J.V., Horning, J.J.: Larch: Languages and Tools for Formal Specification. Springer (1993)
Hatcliff, J., Leavens, G.T., Leino, K.R.M., Müller, P., Parkinson, M.J.: Behavioral interface specification languages. ACM Comput. Surv. 44(3), 16 (2012)
Hayes, I.J., Wu, X., Meinicke, L.A.: Capabilities for Java: Secure access to resources. In: APLAS. pp. 67–84 (2017)
Hoare, C.A.R.: An axiomatic basis for computer programming. Comm. ACM 12, 576–580 (1969)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall (1985)
Jones, T., Homer, M., James Noble, Bruce, K.B.: Object inheritance without classes. In: ECOOP. pp. 13:1–13:26 (2016)
Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D.R., Müller, P., Kiniry, J., Chalin, P.: JML Reference Manual (February 2007), iowa State Univ. www.jmlspecs.org
Leino, K.R.: Dafny: An automatic program verifier for functional correctness. In: LPAR16. Springer (April 2010)
Leino, K.R.M., Schulte, W.: Using history invariants to verify observers. In: ESOP (2007)
Lewis, D.: Causation. Journal of Philosophy 70(17) (1973)
Maffeis, S., Mitchell, J., Taly, A.: Object capabilities and isolation of untrusted web applications. In: Proc of IEEE Security and Privacy (2010)
Melicher, D., Shi, Y., Potanin, A., Aldrich, J.: A capability-based module system for authority control. In: ECOOP. pp. 20:1–20:27 (2017)
Meyer, B.: Eiffel: The Language. Prentice Hall (1992)
Meyer, B.: Object-Oriented Software Construction, Second Edition. Prentice Hall, second edn. (1997)
Miller, M.S., Cutsem, T.V., Tulloh, B.: Distributed electronic rights in JavaScript. In: ESOP (2013)
Miller, M.S.: Robust Composition: Towards a Unified Approach to Access Control and Concurrency Control. Ph.D. thesis, Baltimore, Maryland (2006)
Miller, M.S., Morningstar, C., Frantz, B.: Capability-based Financial Instruments: From Object to Capabilities. In: Financial Cryptography. Springer (2000)
Miller, M.S., Samuel, M., Laurie, B., Awad, I., Stay, M.: Safe active content in sanitized JavaScript (2008), code.google.com/p/google-caja/
Mitre Organisation: CWE-830: Inclusion of Web Functionality from an Untrusted Source (2019), https://cwe.mitre.org/data/definitions/830.html
Morris Jr., J.H.: Protection in programming languages. CACM 16(1) (1973)
Müller, P., Poetzsch-Heffter, A., Leavens, G.T.: Modular invariants for layered object structures. Science of Computer Programming 62, 253–286 (2006)
Murray, T.: Analysing the Security Properties of Object-Capability Patterns. Ph.D. thesis, University of Oxford (2010)
Murray, T., Sison, R., Engelhardt, K.: Covern: A logic for compositional verification of information flow control. In: EuroS&P (2018)
Noble, J., Drossopoulou, S.: Rationally reconstructing the escrow example. In: FTfJP (2014)
Noble, J., Potanin, A., Murray, T., Miller, M.S.: Abstract and concrete data types vs object capabilities. In: Müller, P., Schaefer, I. (eds.) Principled Software Development (2018)
Noble, J., Potter, J., Vitek, J.: Flexible alias protection. In: ECOOP (Jul 1998)
Pearce, D., Groves, L.: Designing a verifying compiler: Lessons learned from developing Whiley. Sci. Comput. Prog. (2015)
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)
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS. pp. 55–74. IEEE Computer Society (2002)
Rhodes, D., Disney, T., Flanagan, C.: Dynamic detection of object capability violations through model checking. In: DLS. pp. 103–112 (2014)
Schaefer, I., Runge, T., Knüppel, 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–9, 2018, Proceedings, Part I. pp. 502–515 (2018)
Sergey, I., Nagaraj, V., Johannsen, J., Kumar, A., Trunov, A., Chan, K.: Safer smart contract programming with Scilla. In: OOPSLA (2019)
Smans, J., Jacobs, B., Piessens, F.: Implicit Dynamic Frames. ToPLAS (2012)
Summers, A.J., Drossopoulou, S.: Considerate Reasoning and the Composite Pattern. In: VMCAI (2010)
Swasey, D., Garg, D., Dreyer, D.: Robust and Compositional Verification of Object Capability Patterns. In: OOPSLA (2017)
Talpin, J.P., Jouvelot, P.: The Type and Effect Discipline. In: LICS. pp. 162–173 (1992)
The Ethereum Wiki: ERC20 Token Standard (Dec 2018), https://theethereum.wiki/w/index.php/ERC20_Token_Standard
Acknowledgments
This work is based on a long-standing collaboration with Mark S. Miller and Toby Murray. We have received invaluable feedback from Alex Summers, Bart Jacobs, Chris Hawblitzel, Michael Jackson, Lucius G. Meredith, Mike Stay, Shuh Peng Loh, Emil Klasan, members of WG 2.3, and the FASE 2020 reviewers. The work has been supported by the Royal Society of New Zealand (Te Apārangi) Marsden Fund (Te Pūtea Rangahau a Marsden) grants VUW-1318 and VUW-1815, and research gifts from Agoric , the Ethereum Foundation, and Facebook.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2020 The Author(s)
About this paper
Cite this paper
Drossopoulou, S., Noble, J., Mackay, J., Eisenbach, S. (2020). Holistic Specifications for Robust Programs. In: Wehrheim, H., Cabot, J. (eds) Fundamental Approaches to Software Engineering. FASE 2020. Lecture Notes in Computer Science(), vol 12076. Springer, Cham. https://doi.org/10.1007/978-3-030-45234-6_21
Download citation
DOI: https://doi.org/10.1007/978-3-030-45234-6_21
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-45233-9
Online ISBN: 978-3-030-45234-6
eBook Packages: Computer ScienceComputer Science (R0)