Towards specifications of robustness - the things that programs do _not_ do

Programs are considered to be robust, if they behave “well” in all possible usage scenarios, whether intended or not. To help develop robust programs several programming language features and programming patterns have been proposed: constants, private members, encapsulation, capabilities, ownership, proxies, membranes etc. All these are powerful mechanisms which support the development of robust code.

However, these mechanisms do not address the question as to what specific guarantees we want the particular robust code to make. How do we express, eg, that a DOM-tree protected by a wrapper will not be modified beyond the part allowed by the wrapper, or that money will not disappear from a multiowner-account unless one of the account holders withdrew their money? Traditional program specifications, based on pre- and post- conditions do not address robustness either.

In this talk we will claim that robustness is about guaranteeing that certain thing will not happen – as opposed to functional specifications which are about what will happen. We will introduce "holistic specifications", an extension of traditional program specifications that support the expression of robustness properties through a logic with spatial and temporal features. We will show how holistic specifications can be used to specify robustness concerns in a number of popular program patterns from object-capabilities and smart contracts: the membrane, Mint-and-Purse, DOM-wrappers, the DAO, and ERC-20. We will show how to reason about the preservation of non-trivial properties concerning our data when it comes into contact with unknown, or adversarial code.

OBJECTIVES

To discuss what _is_ robustness, and how to specify robustness aspects of programs.