key: cord-0048655-07ap2rdn
authors: Drossopoulou, Sophia; Noble, James; Mackay, Julian; Eisenbach, Susan
title: Holistic Specifications for Robust Programs
date: 2020-03-13
journal: Fundamental Approaches to Software Engineering
DOI: 10.1007/978-3-030-45234-6_21
sha: 6c6e68f35875a88a172cdc445375761e3c9424e9
doc_id: 48655
cord_uid: 07ap2rdn

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 [Formula: see text]hainmail specification language for writing holistic specifications that focus on necessary conditions (as well as sufficient conditions). We give a formal semantics for [Formula: see text]hainmail, and discuss several examples. The core of [Formula: see text]hainmail has been mechanised in the Coq proof assistant.

Software guards our secrets, our money, our intellectual property, our reputation [47] . We entrust personal and corporate information to software which works in an open world, where it interacts with third party software of unknown provenance, possibly buggy and potentially malicious.

This means we need our software to be robust: to behave correctly even if used by erroneous or malicious third parties. We expect that our bank will only make payments from our account if instructed by us, or by somebody we have authorised, that space on a web page given to an advertiser will not be used to obtain access to our bank details [43] , or that a concert hall will not book the same seat more than once.

While language mechanisms such as constants, invariants, object capabilities [40] , and ownership [14] make it possible to write robust programs, they cannot ensure that programs are robust. Ensuring robustness is difficult because it means different things for different systems: perhaps that critical operations should only be invoked with the requisite authority; perhaps that sensitive personal information should not be leaked; or perhaps that a resource belonging to one user should not be consumed by another. To ensure robustness, we need ways to specify what robustness means for a particular program, and ways to demonstrate that the particular program adheres to its specific robustness requirements.

Consider the code snippets from Fig. 1 . Objects of class Safe hold a treasure and a secret, and only the holder of the secret can remove the treasure from the safe. We show the code in two versions; both have the same method take, and the second version has an additional method set. We assume a dynamically typed language (so that our results are applicable to both statically and dynamically typed settings) 4 ; that fields are private in the sense of Java (i.e. only methods of that class may read or write these fields); and that addresses are unforgeable (so there is no way to guess a secret). A classical Hoare triple describing the behaviour of take would be:

(ClassicSpec) method take(scr) PRE: this:Safe POST: scr=this.secretpre −→ this.treasure=null ∧ scr =this.secretpre −→ ∀s:Safe. s.treasure=s.treasurepre (ClassicSpec) expresses that knowledge of the secret is sufficient to remove the treasure, and that take cannot remove the treasure unless the secret is provided. But it cannot preclude that Safe -or some other class, for that matter -contains more methods which might make it possible to remove the treasure without knowledge of the secret. This is the problem with the second version of Safe: it satisfies (ClassicSpec), but is not robust, as it is possible to overwrite the secret of the Safe and then use it to remove the treasure. To express robustness requirements, we introduce holistic specifications, and require that: (HolisticSpec) mandates that for any safe s whose treasure is not null, if some time in the future its treasure were to become null, then at least one external object (i.e. an object whose class is not Safe) in the current configuration has direct access to s's secret. This external object need not have caused the change in s.treasure but it would have (transitively) passed access to the secret which ultimately did cause that change. Both classes in Fig. 1 satisfy (ClassicSpec), but the second version does not satisfy (HolisticSpec).

In this paper we propose Chainmail, a specification language to express holistic specifications. The design of Chainmail was guided by the study of a sequence of examples from the object-capability literature and the smart contracts world: the membrane [17] , the DOM [20, 59] , the Mint/Purse [40] , the Escrow [18] , the DAO [12, 15] and ERC20 [61] . As we worked through the examples, we found a small set of language constructs that let us write holistic specifications across a range of different contexts. Chainmail extends traditional program specification languages [31, 37] the design of the holistic specification language Chainmail, the semantics of Chainmail, a Coq mechanisation of the core of Chainmail.

The rest of the paper is organised as follows: Section 2 gives an example from the literature which we will use to elucidate key points of Chainmail. 3 presents the Chainmail specification language. Section 4 introduces the formal model underlying Chainmail, and then section 5 defines the semantics of Chainmail's assertions. Section 6 discusses our design, 7 considers related work, and section 8 concludes. We relegate key points of exemplar problems and various details to appendices which are available at [1] .

As a motivating example, we consider a simplified banking application taken from the object capabilities literature [41] : Accounts belong to Banks and hold money (balances); with access to two Accounts of the same Bank one can transfer any amount of money from one to the other. This example has the advantage that it requires several objects and classes.

We will not show the code here (see appendix C), but suffice it to say that class Account has methods deposit(src, amt) and makeAccount(amt) (i.e. a method called deposit with two arguments, and a method called makeAccount with one argument). Similarly, Bank has method newAccount(amt). Moreover, deposit requires that the receiver and first argument (this and src) are Accounts and belong to the same bank, that the second argument (amt) is a number, and that src's balance is at least amt. If this condition holds, then amt gets transferred from src to the receiver. The function makeNewAccount returns a fresh Account with the same bank, and transfers amt from the receiver Account to the new Account. Finally, the function newAccount when run by a Bank creates a new Account with corresponding amount of money in it. 5 It is not difficult to give formal specifications of these methods in terms of pre-and post-conditions. However, what if the bank provided a steal method that emptied out every account in the bank into a thief's account? The critical problem is that a bank implementation including a steal method could meet the functional specifications of deposit, makeAccount, and newAccount, and still allow the clients' money to be stolen.

One obvious solution would be to adopt a closed-world interpretation of specifications: we interpret functional specifications as exact in the sense that only implementations that meet the functional specification exactly, with no extra methods or behaviour, are considered as suitable implementations of the functional specification. The problem is that this solution is far too strong: it would for example rule out a bank that during software maintenance was given a new method count that simply counted the number of deposits that had taken place, or a method notify to enable the bank to occasionally send notifications to its customers.

What we need is some way to permit bank implementations that send notifications to customers, but to forbid implementations of steal. The key here is to capture the (implicit) assumptions underlying the design of the banking application. We provide additional specifications that capture those assumptions. The following three informal requirements prevent methods like steal:

1. An account's balance can be changed only if a client calls the deposit method with the account as the receiver or as an argument. 2. An account's balance can be changed only if a client has access to that particular account. 3. The Bank/Account component does not leak access to existing accounts or banks.

Compared with the functional specification we have seen so far, these requirements capture necessary rather than sufficient conditions: Calling the deposit method to gain access to an account is necessary for any change to that account taking place. The function steal is inconsistent with requirement (1), as it reduces the balance of an Account without calling the function deposit. However, requirement (1) is not enough to protect our money. We need (2) to avoid an Account's balance getting modified without access to the particular Account, and (3) to ensure that such accesses are not leaked.

We can express these requirements through Chainmail assertions. Rather than specifying the behaviour of particular methods when they are called, we write assertions that range across the entire behaviour of the Bank/Account module:

In the above and throughout the paper, we use an underscore (_) to indicate an existentially bound variable whose value is of no interest.

Assertion (1) says that if an account's balance changes (changes a.balance ), then there must be some client object o that called the deposit method with a as a receiver or as an argument ( o calls _.deposit( _) ).

Assertion (2) similarly constrains any possible change to an account's balance. If at some future point the balance changes (will changes ... ), and if this future change is observed with the state restricted to the objects from S (i.e. ... in S ), then at least one of these objects (o ∈ S) is external to the Bank/Account system (external o ) and has direct access to that account object ( o access a ). Notice that while the change in the balance happens some time in the future, the external object o has access to a in the current state. Notice also that the object which makes the call to deposit described in (1) , and the object which has access to a in the current state described in (2), need not be the same: it may well be that the latter passes a reference to a to the former (indirectly), which then makes the call to deposit.

It remains to think about how access to an Account may be obtained. This is the remit of assertion (3) , which says that if at some time in the future of the state restricted to S, some object o which is external has access to some account a, and if a exists in the current state, then in the current state some object from S has access to a. Where o and o may, but need not, be the same object. And where o has to exist and have access to a in the current state, but o need not exist in the current state -it may be allocated later. Assertion (3) thus gives essential protection when dealing with foreign, untrusted code. When an Account is given out to untrusted third parties, assertion (3) guarantees that this Account cannot be used to obtain access to further Accounts.

A holistic specification for the bank account, then, would be a sufficient functional specification plus the necessary specifications (1)-(3) from above. This holistic specification permits an implementation of the bank that also provides count and notify methods, even though the specification does not mention either method. Critically, though, the holistic Chainmail specification does not permit an implementation that includes a steal method.

In this Section we give a brief and informal overview of some of the most salient features of Chainmaila full exposition appears in Section 5.

Example Configurations We will illustrate these features using the Bank/Account example from the previous section. We use the runtime configurations σ 1 and σ 2 shown in the left and right diagrams in Figure 2 . In both diagrams the rounded boxes depict objects: green for those from the Bank/Account component, and grey for the "external", "client" objects. The transparent green rectangle shows which objects are contained by the Bank/Account component. The object at 1 is a Bank, those at 2, 3 and 4 are Accounts, and those at 91, 92, 93 and 94 are "client" objects which belong to classes different from those from the Bank/Account module.

Each configuration represents one alternative implementation of the Bank object. Configuration σ 1 may arise from execution using a module M BA1 , where Account objects have a field myBank pointing to their Bank, and an integer field balancethe code can be found in appendix C Fig. 3 . Configuration σ 2 may arise from execution using a module M BA2 , where Accounts have a myBank field, Bank objects have a ledger implemented though a sequence of Nodes, each of which has a field pointing to an Account, a field balance, and a field next -the code can be found in appendix C Figs. 6 and 4. For the rest, assume variable identifiers b 1 , and a 2 -a 4 , and u 91 -u 94 denoting objects 1, 2-4, and 91-94 respectively for both σ 1 and σ 2 . That is,

Classical Assertions talk about the contents of the local variables (i.e. the topmost stack frame), and the fields of the various objects (i.e. the heap). For example, the assertion a 2 .myBank=a 3 .myBank, says that a 2 and a 3 have the same bank. In fact, this assertion is satisfied in both σ 1 and σ 2 , written formally as ..., σ 1 |= a 2 .myBank = a 3 .myBank ..., σ 2 |= a 2 .myBank = a 3 .myBank.

The term x:ClassId says that x is an object of class ClassId. For example ..., σ 1 |= a 2 .myBank : Bank. We support ghost fields [11, 31] , e.g. a 1 .balance is a physical field in σ 1 and a ghost field in σ 2 since in MBA2 an Account does not store its balance (as can be seen in appendix C Fig. 6 ). We also support the usual logical connectives, and so, we can express assertions such as ∀a.

[ a : Account −→ a.myBank : Bank ∧ a.balance ≥ 0 ] .

Permission: Access Our first holistic assertion, x access y , asserts that object x has a direct reference to another object y: either one of x's fields contains a reference to y, or the receiver of the currently executing method is x, and y is one of the arguments or a local variable. For example: ..., σ 1 |= a 2 access b 1 If σ 1 were executing the method body corresponding to the call a 2 .deposit(a 3 ,360), then we would have ..., σ 1 |= a 2 access a 3 , That is, during execution of deposit, the object at a 2 has access to the object at a 3 , and could, if the method body chose to, call a method on a 3 , or store a reference to a 3 in its own fields. Access is not symmetric, nor transitive:

..., σ 1 |= a 3 access a 2 , ..., σ 2 |= a 2 access * a 3 , ..., σ 2 |= a 2 access a 3 .

The assertion x calls m.y( zs) holds in configurations where a method on object x makes a method call y.m(zs) -that is it calls method m with object y as the receiver, and with arguments zs. For example, ..., σ 3 |= x calls a 2 .deposit( a 3 , 360) . means that the receiver in σ 3 is x, and that a 2 .deposit(a 3 , 360) is the next statement to be executed.

Space: In The space assertion A in S establishes validity of A in a configuration restricted to the objects from the set S. For example, if object 94 is included in S 1 but not in S 2 , then we have ..., σ 1 |= (∃o. o access a 4 ) in S 1 ..., σ 1 |= (∃o. o access a 4 ) in S 2 . The set S in the assertion A in S is therefore not the footprint of A; it is more like the fuel [2] given to establish that assertion. Note that ..., σ |= A in S does not imply ..., σ |= A nor does it imply ..., σ |= A in S ∪ S . The other direction of the implication does not hold either.

Time: Next, Will, Prev, Was We support several operators from temporal logic: (next A , will A , prev A , and was A ) to talk about the future or the past in one or more steps. The assertion will A expresses that A will hold in one or more steps. For example, taking σ 4 to be similar to σ 2 , the next statement to be executed to be a 2 .deposit(a 3 , 360), and M BA2 ..., σ 4 |= a 2 .balance = 60, and that M BA2 ..., σ 4 |= a 4 .balance ≥ 360, then M BA2 ..., σ 4 |= will a 2 .balance = 420 . The internal module, M BA2 is needed for looking up the method body of deposit.

Viewpoint: -External The assertion external x expresses that the object at x does not belong to the module under consideration. For example,

The internal module, M BA2 , is needed to judge which objects are internal or external.

Change and Authority: We have used changes ... in our Chainmail assertions in section 2, as in changes a.balance . Assertions that talk about change, or give conditions for change to happen are fundamental for security; the ability to cause change is called authority in [40] . We can encode change using the other features of Chainmail, namely, for any expression e:

]. and similarly for assertions.

Putting these together We now look at some composite assertions which use several features from above. For example, the assertion below says that if the statement to be executed is a 2 .deposit(a 3 , 60), then the balance of a 2 will eventually change:

Now look deeper into space assertions, A in S , which allow us to characterise the set of objects which have authority over certain effects (here A). In particular, the assertion will A in S requires two things: i) that A will hold in the future, and ii) that all the objects which cause the effect which will make A valid are included in S. Knowing who has, and who has not, authority over properties or data is a fundamental concern of robustness [40] . Notice that the authority is a set, rather than a single object: quite often it takes several objects in concert to achieve an effect.

Consider assertions (2) and (3) from the previous section. They both have the form "will A in S −→ P (S)", where P is some property over a set. These assertions say that if ever in the future A becomes valid, and if the objects involved in making A valid are included in S, then S must satisfy P . Such assertions can be used to restrict whether A will become valid. If we have some execution which only involves objects which do not satisfy P , then we know that the execution will not ever make A valid.

In summary, in addition to classical logical connectors and classical assertions over the contents of the heap and the stack, our holistic assertions draw from some concepts from object capabilities ( _ access _ for permission; _ calls _._( _) and changes _ for authority) as well as temporal logic (will A , was A and friends), and the relation of our spatial connective ( A in S ) with ownership and effect systems [60, 14, 13] .

The next two sections discuss the semantics of Chainmail. Section 4 contains an overview of the formal model and section 5 focuses on the most important part of Chainmail: assertions.

We now give an overview of the formal model for Chainmail. In section 4.1 we introduce the shape of the judgments used to give semantics to Chainmail, while in section 4.2 we describe the most salient aspects of an underlying programming language used in Chainmail.

Having outlined the ingredients of our holistic specification language, the next question to ask is: When does a module M satisfy a holistic assertion A? More formally: when does M |= A hold?

Our answer has to reflect the fact that we are dealing with an open world, where M, our module, may be linked with arbitrary untrusted code.

To model the open world, we consider pairs of modules, M M , where M is the module whose code is supposed to satisfy the assertion, and M is another module which exercises the functionality of M. We call our module M the internal module, and M the external module, which represents potential attackers or adversaries.

We The judgement M M , σ |= A means that assertion A is satisfied by M M and σ. As in traditional specification languages [31, 37] , satisfaction is judged in the context of a runtime configuration σ; but in addition, it is judged in the context of the internal and external modules. These are used to find abstract functions defining ghost fields as well as method bodies needed when judging validity of temporal assertions such as will _ .

We distinguish between internal and external modules. This has two uses: First, Chainmail includes the "external o " assertion to require that an object belongs to the external module, as in the Bank Account's assertion (2) and (3) in section 2. Second, we adopt a version of visible states semantics [45, 25, 38] , treating all executions within a module as atomic. We only record runtime configurations which are external to module M, i.e. those where the executing object (i.e. the current receiver) comes from module M . Execution has the form M M , σ ; σ where we ignore all intermediate steps with receivers internal to M. In the next section we shall outline the underlying programming language, and define the judgment M M , σ ; σ and the set Arising(M M ).

The meaning of Chainmail assertions is parametric with an underlying object-oriented programming language, with modules as repositories of code, classes with fields, methods and ghostfields, objects described by classes, a way to link modules into larger ones, and a concept of program execution 6 .

We have developed L oo , a minimal such object-oriented language, which we outline in this section. We describe the novel aspects of L oo , and summarise the more conventional parts, relegating full, and mostly unsurprising, definitions to Appendix A.

Modules are central to L oo , as they are to Chainmail. As modules are repositories of code, we adopt the common formalisation of modules as maps from class identifiers to class definitions, c.f. Appendix, Def. 1. We use the terms module and component in an analogous manner to class and object respectively. L oo is untyped for several reasons. Many popular programming languages are untyped. The external module might be untyped, and so it is more general to consider everything as untyped. Finally, a solution that works for an untyped language will also apply to a typed language, while the converse is not true.

Class definitions consist of field, method and ghost field declarations, c.f. Appendix, Def. 2. Method bodies are sequences of statements, which can be field reads or field assignments, object creation, method calls, and return statements. Fields are private in the sense of C++: they can only be read or written by methods of the current class. This is enforced by the operational semantics, c.f. Fig. 1 . We discuss ghost fields in the next section.

Runtime configurations, σ, contain all the usual information about execution snapshots: the heap, and a stack of frames. Each frame consists of a continuation, contn, describing the remaining code to be executed by the frame, and a map from variables to values. Values are either addresses or sets of addresses; sets are needed to deal with assertions which quantify over sets of objects, such as assertions (1) and (2) from section 2. We define one-module execution through a judgment of the form M, σ ; σ in the Appendix, Fig. 1 .

We define a module linking operator • so that M•M is the union of the two modules, provided that their domains are disjoint, c.f. Appendix, Def. 8. As we said in section 4.1, we distinguish between the internal and external module. We consider execution from the view of the external module, and treat execution of methods from the internal module as atomic. For this, we define two-module execution based on one-module execution as follows: In the definition above, Class(x) σ looks up the class of the object stored at x, c.f. Appendix, Def. 5. For example, for σ 4 as in Section 3 whose next statement to be executed is a 2 .deposit(a 3 , 360), we would have a sequence of configurations σ 41 , ... σ 4n , σ 5 so that the one-module execution gives M BA2 , σ 4 ; σ 41 ; σ 42 ... ; Fig.3 ; where blue stands for σ(this) ∈ M 1 ,and orange for σ(this) ∈ M 2 ). Two-module execution is related to visible states semantics [45] as they both filter configurations, with the difference that in visible states semantics execution is unfiltered and configurations are only filtered when it comes to the consideration of class invariants while two-module execution filters execution. The lemma below says that linking is associative and commutative, and preserves both one-module and two-module execution. We can now answer the question as to which runtime configurations are pertinent when judging a module's adherence to an assertion. Initial configurations are those whose heap have only one object, of class Object, and whose stack have one frame, with arbitrary continuation. Arising configurations are those that can be reached by two-module execution, starting from any initial configuration.

-Initial (ψ, χ) , if ψ consists of a single frame φ with dom(φ) = {this}, and there exists some address α, such that this φ =α, and dom(χ)=α, and

Chainmail assertions (details in appendix B.3) consist of (pure) expressions e, comparisons between expressions, classical assertions about the contents of heap and stack, the usual logical connectives, as well as our holistic concepts. In this section we focus on the novel, holistic, features of Chainmail (permission, control, time, space, and viewpoint), as well as our wish to support some form of recursion while keeping the logic of assertions classical.

Permission expresses that an object has the potential to call methods on another object, and to do so directly, without help from any intermediary object. This is the case when the two objects are aliases, or the first object has a field pointing to the second object, or the first object is the receiver of the currently executing method and the second object is one of the arguments or a local variable. Interpretations of variables and paths, ... σ , are defined in the usual way (appendix Def. 5). x σ and y σ are defined, and • x σ = y σ , or • x.f σ = y σ , for some field f, or • x σ = this σ and y σ = z σ , for some variable z and z appears in σ.contn.

In the last disjunct, where z is a parameter or local variable, we ask that z appears in the code being executed (σ.contn). This requirement ensures that variables which were introduced into the variable map in order to give meaning to existentially quantified assertions, are not considered.

Control expresses which object is the process of making a function call on another object and with what arguments. The relevant information is stored in the continuation (cont) on the top frame. Thus, x calls y.m( z 1 , ...z n ) expresses the call y.m(z 1 , ...z n ) will be executed next, and that the caller is x.

Viewpoint is about whether an object is viewed as belonging to the internal mode; this is determined by the class of the object.

Space is about asserting that some property A holds in a configuration whose objects are restricted to those from a given set S. This way we can express that the objects from the set S have authority over the assertion A. In order to define validity of A in S in a configuration σ, we first define a restriction operation, σ↓ S which restricts the objects from σ to only those from S.

Definition 6 (Restriction of Runtime Configurations). The restriction operator ↓ applied to a runtime configuration σ and a variable S is defined as follows:

-σ↓ S (ψ, χ ), if σ=(ψ, χ), dom(χ ) = S σ , and ∀α ∈ dom(χ ).χ(α) = χ (α).

For example, if we take σ 2 from Fig. 2 in Section 2, and restrict it with some set S 4 such that S 4 σ2 = {91, 1, 2, 3, 4, 11}, then the restriction σ 2 ↓ S4 will look as on the right. Note in the diagram above the dangling pointers at objects 1, 11, and 91 -reminiscent of the separation of heaps into disjoint subheaps, as provided by the * operator in separation logic [53] . The difference is that in separation logic, the separation is provided through the assertions, where A * A holds in any heap which can be split into disjoint χ and χ where χ satisfies A and χ satisfies A . That is, in A * A the split of the heap is determined by the assertions A and A and there is an implicit requirement of disjointness, while in σ↓ S the split is determined by S, and no disjointness is required.

We now define the semantics of A in S .

For any modules M, M , assertions A and variable S, we define:

The set S in the assertion A in S is related to framing from implicit dynamic frames [57] : in an implicit dynamic frames assertion acc x.f * A, the frame x.f prescribes which locations may be used to determine validity of A. The difference is that frames are sets of locations (pairs of address and field), while our S-es are sets of addresses. More importantly, implicit dynamic frames assertions whose frames are not large enough are badly formed, while in our work, such assertions are allowed and may hold or not, e.g. M BA2 M , σ |= ¬ (∃n.a 2 .balance = n) in S 4 .

To deal with time, we are faced with four challenges: a) validity of assertions in the future or the past needs to be judged in the future configuration, but using the bindings from the current one, b) the current configuration needs to store the code being executed, so as to be able to calculate future configurations, c) when considering the future, we do not want to observe configurations which go beyond the frame currently at the top of the stack, d) there is no "undo" operator to deterministically enumerate all the previous configurations.

Consider challenge a) in some more detail: the assertion will x.f = 3 is satisfied in the current configuration σ 1 , if in some future configuration σ 2 , the field f of the object that is pointed at by x in the current configuration (σ 1 ) has the value 3, that is, if

x σ1 .f σ2 = 3, even if in that future configuration x denotes a different object (i.e. if x σ1 = x σ2 ). To address this, we define an auxiliary concept: the operator , where σ 1 σ 2 adapts the second configuration to the top frame's view of the former: it returns a new configuration whose stack comes from σ 2 but is augmented with the view from the top frame from σ 1 and where the continuation has been consistently renamed. This allows us to interpret expressions in σ 2 but with the variables bound according to σ 1 ; e.g. we can obtain that value of x in configuration σ 2 even if x was out of scope in σ 2 .

Definition 8 (Adaptation). For runtime configurations σ 1 , σ 2 .: β 2 ) , and • zs 1 =dom(β 1 ), zs 2 =dom(β 2 ), and • zs is a set of variables with the same cardinality as zs 2 , and all variables in zs are fresh in β 1 and in β 2 .

That is, in the new frame φ 2 from above, we keep the same continuation as from σ 2 but rename all variables with fresh names zs , and combine the variable map β 1 from σ 1 with the variable map β 2 from σ 2 while avoiding names clashes through the renaming [zs → β 2 (zs 2 )]. The consistent renaming of the continuation allows the correct modelling of execution, as needed for the semantics of nested time assertions, as e.g. in will x.f = 3 ∧ will x.f = 5 .

Having addressed challenge a) we turn our attention to the remaining challenges: We address challenge b) by storing the remaining code to be executed in cntn in each frame. We address challenge c) by only taking the top of the frame when considering future executions. Finally, we address challenge d) by considering only configurations which arise from initial configurations, and which lead to the current configuration. and where φ is so that σ=(φ · _, _).

In general, will A in S is different from will A in S . In the former assertion, S must contain the objects involved in reaching the future configuration as well as the objects needed to then establish validity of A in that future configuration. In the latter assertion, S need only contain the objects needed to establish A in that future configuration. For example, revisit Fig. 2 , and take S 1 to consist of objects 1, 2, 4, 93, and 94, and S 2 to consist of objects 1, 2, 4. Assume that σ 5 is like σ 1 , that the next call in σ 5 is a method on u 94 , whose body obtains the address of a 4 (by making a call on 93 to which it has access), and the address of a 2 (to which it has access), and then makes the call a 2 . deposit(a 4 , 360) . Assume also that a 4 's balance is 380. Then M BA1 ..., σ 5 |= will changes a 2 .balance in S 1 M BA1 ..., σ 5 |= will changes a 2 .balance in S 2 M BA1 ..., σ 5 |= will changes a 2 .balance in S 2

We define equivalence of assertions in the usual way: 

Examplars The design of Chainmail was guided by the study of a sequence of exemplars taken from the object-capability literature and the smart contracts world:

In the associated appendix (see Appendix G) we list and present the properties of Chainmail we have formalised in Coq. We have proven that Chainmail obeys much of the properties of classical logic. While we formalise most of the underlying semantics, we make several assumptions in our Coq formalism: (i) the law of the excluded middle, a property that is well known to be unprovable in constructive logics, and (ii) the equality of variable maps and heaps down to renaming. Coq formalisms often require fairly verbose definitions and proofs of properties involving variable substitution and renaming, and assuming equality down to renaming saves much effort.

More details of the formal foundations of Chainmail, and the model, are also in appendices [1] .

Behavioural Specification Languages Hatcliff et al. [26] provide an excellent survey of contemporary specification approaches. With a lineage back to Hoare logic [28] , Meyer's Design by Contract [38] was the first popular attempt to bring verification techniques to object-oriented programs as a "whole cloth" language design in Eiffel. Several more recent specification languages are now making their way into practical and educational use, including JML [31] , Spec [4] , Dafny [32] and Whiley [51] . Our approach builds upon these fundamentals, particularly Leino & Shulte's formulation of two-state invariants [33] , and Summers and Drossopoulou's Considerate Reasoning [58] . In general, these approaches assume a closed system, where modules can be trusted to coöperate. In this paper we aim to work in an open system where modules' invariants must be protected irrespective of the behaviour of the rest of the system.

In an open world, we cannot rely on the kindness of strangers: rather we have to ensure our code is correct regardless of whether it interacts with friends or foes. Attackers "only have to be lucky once" while secure systems "have to be lucky always" [5] . Miller [39, 40] defines the necessary approach as defensive consistency: "An object is defensively consistent when it can defend its own invariants and provide correct service to its well behaved clients, despite arbitrary or malicious misbehaviour by its other clients." Defensively consistent modules are particularly hard to design, to write, to understand, and to verify: but they make it much easier to make guarantees about systems composed of multiple components [46] .

Object Capabilities and Sandboxes. Capabilities as a means to support the development of concurrent and distributed system were developed in the 60's by Dennis and Van Horn [19] , and were adapted to the programming languages setting in the 70's [44] . Object capabilities were first introduced [40] in the early 2000s, and many recent studies manage to verify safety or correctness of object capability programs. Google's Caja [42] applies sandboxes, proxies, and wrappers to limit components' access to ambient authority. Sandboxing has been validated formally: Maffeis et al. [35] develop a model of JavaScript, demonstrate that it obeys two principles of object capability systems and show how untrusted applications can be prevented from interfering with the rest of the system. Recent programming languages [27, 10, 54] including Newspeak [9] , Dart [8] , Grace [7, 30] and Wyvern [36] have adopted the object capability model.

Murray made the first attempt to formalise defensive consistency and correctness [46] . Murray's model was rooted in counterfactual causation [34] : an object is defensively consistent when the addition of untrustworthy clients cannot cause well-behaved clients to be given incorrect service. Murray formalised defensive consistency very abstractly, over models of (concurrent) objectcapability systems in the process algebra CSP [29] , without a specification language for describing effects, such as what it means for an object to provide incorrect service. Both Miller and Murray's definitions are intensional, describing what it means for an object to be defensively consistent.

Drossopoulou and Noble [21, 48] have analysed Miller's Mint and Purse example [40] and discussed the six capability policies as proposed in [40] . In [22] , they sketched a specification language, used it to specify the six policies from [40] , showed that several possible interpretations were possible, and uncovered the need for another four further policies. They also sketched how a trust-sensitive example (the escrow exchange) could be verified in an open world [24] . Their work does not support the concepts of control, time, or space, as in Chainmail, but it offers a primitive expressing trust.

Devriese et al. [20] have deployed powerful theoretical techniques to address similar problems: They show how step-indexing, Kripke worlds, and representing objects as state machines with public and private transitions can be used to reason about object capabilities. Devriese have demonstrated solutions to a range of exemplar problems, including the DOM wrapper (replicated in our section F) and a mashup application. Their distinction between public and private transitions is similar to the distinction between internal and external objects.

More recently, Swasey et al. [59] designed OCPL, a logic for object capability patterns, that supports specifications and proofs for object-oriented systems in an open world. They draw on verification techniques for security and information flow: separating internal implementations ("high values" which must not be exposed to attacking code) from interface objects ("low values" which may be exposed). OCPL supports defensive consistency (they use the term "robust safety" from the security community [6] ) via a proof system that ensures low values can never leak high values to external attackers. This means that low values can be exposed to external code, and the behaviour of the system is described by considering attacks only on low values. They use that logic to prove a number of object-capability patterns, including sealer/unsealer pairs, the caretaker, and a general membrane.

Schaefer et al. [55] have recently added support for information-flow security using refinement to ensure correctness (in this case confidentiality) by construction. By enforcing encapsulation, all these approaches share similarity with techniques such as ownership types [14, 50] , which also protect internal implementation objects from accesses that cross encapsulation boundaries. Banerjee and Naumann demonstrated that by ensuring confinement, ownership systems can enforce representation independence (a property close to "robust safety") some time ago [3] .

Chainmail differs from Swasey, Schaefer's, and Devriese's work in a number of ways: They are primarily concerned with mechanisms that ensure encapsulation (aka confinement) while we abstract away from any mechanism via the external predicate. They use powerful mathematical techniques which the users need to understand in order to write their specifications, while Chainmail users only need to understand first order logic and the holistic operators presented in this paper. Finally, none of these systems offer the kinds of holistic assertions addressing control flow, change, or temporal operations that are at the core of Chainmail's approach.

Scilla [56] is a minimalistic typed functional language for writing smart contracts that compiles to the Ethereum bytecode. Scilla's semantic model is restricted, assuming actor based communication and restricting recursion, thus facilitating static analysis of Scilla contracts and ensuring termination. Scilla is able to demonstrate that a number of popular Ethereum contracts avoid type errors, out-of-gas resource failures, and preservation of virtual currency. Scilla's semantics are defined formally, but have not yet been represented in a mechanised model.

Finally, the recent VerX tool is able to verify a range of specifications for solidity contracts automatically [52] . Similar to Chainmail, VerX has a specification language based on temporal logic. VerX offers three temporal operators (always, once, prev) but only within a past modality, while Chainmail has two temporal operators, both existential, but with both past and future modalities. VerX specifications can also include predicates that model the current invocation on a contract (similar to Chainmail's "calls"), can access variables, and compute sums (only) over collections. Chainmail is strictly more expressive as a specification language, including quantification over objects and sets (so can compute arbitrary reductions on collections) and of course specifications for permission ("access"), space ("in") and viewpoint ("external") which have no analogues in VerX. Unlike Chainmail, VerX includes a practical tool that has been used to verify a hundred properties across case studies of twelve Solidity contracts.

In this paper we have motivated the need for holistic specifications, presented the specification language Chainmail for writing such specifications, and outlined the formal foundations of the language. To focus on the key attributes of a holistic specification language, we have kept Chainmail simple, only requiring an understanding of first order logic. We believe that the holistic features (permission, control, time, space and viewpoint) are intuitive concepts when reasoning informally, and were pleased to have been able to provide their formal semantics in what we argue is a simple manner.

Bank and Account as in Section 2 with two different implementations

Ethereum contract for Decentralised Autonomous Organisation

Restricting access to browser Domain Object Model We present these exemplars as appendices [1]. Our design was also driven by work on other examples such as the membrane

of the Chainmail specification language, along with the underlying L oo language. Our formalism is organised as follows: 1. The L oo Language: a class based, object oriented language with mutable references. 2. Chainmail: The full assertion syntax and semantics

L oo Properties: Secondary properties of the loo language that aid in reasoning about its semantics

Chainmail Properties: The core properties defined on the semantics of Chainmail. References 1. Holistic specifications paper with appendices

State-dependent representation independence

Ownership confinement ensures representation independence for object-oriented programs

The Spec# programming system: An overview

BBC: On This Day: 1984: Tory cabinet in Brighton bomb blast

Refinement types for secure implementations

Grace: the Absence of (Inessential) Difficulty. In: Onwards

The Dart Programming Language

The Newspeak language specification version 0

Capnet: security and least authority in a capability-enabled cloud

Beyond assertions: Advanced specification and verification with JML and esc/java2

Decentralized autonomous organization to automate governance

Ownership, encapsulation and the disjointness of type and effectr

Ownership types for flexible alias protection

Coindesk: Understanding the DAO attack

Membranes in Javascript

Trustworthy proxies: Virtualizing objects with invariants

Programming Semantics for Multiprogrammed Computations

Reasoning about object capabilities with logical relations and effect parametricity

The need for capability policies

Towards capability policy specification and verification

Holisitic Specifications for Robust Programs -Coq Model

Swapsies on the internet: First steps towards reasoning about risk and trust in an open world. In: (PLAS)

Larch: Languages and Tools for Formal Specification

Behavioral interface specification languages

Capabilities for Java: Secure access to resources

An axiomatic basis for computer programming

Communicating Sequential Processes

Object inheritance without classes

Dafny: An automatic program verifier for functional correctness

Using history invariants to verify observers

Object capabilities and isolation of untrusted web applications

A capability-based module system for authority control

Eiffel: The Language

Object-Oriented Software Construction, Second Edition

Distributed electronic rights in JavaScript

Robust Composition: Towards a Unified Approach to Access Control and Concurrency Control

Capability-based Financial Instruments: From Object to Capabilities

Safe active content in sanitized

Mitre Organisation: CWE-830: Inclusion of Web Functionality from an Untrusted Source

Protection in programming languages

Modular invariants for layered object structures

Analysing the Security Properties of Object-Capability Patterns

COVERN: A logic for compositional verification of information flow control

Rationally reconstructing the escrow example

Abstract and concrete data types vs object capabilities

Flexible alias protection

Designing a verifying compiler: Lessons learned from developing

VerX: Safety verification of smart contracts

Separation logic: A logic for shared mutable data structures

Dynamic detection of object capability violations through model checking

Towards confidentiality-by-construction

Safer smart contract programming with Scilla

Implicit Dynamic Frames

Considerate Reasoning and the Composite Pattern

Robust and Compositional Verification of Object Capability Patterns

The Type and Effect Discipline

The Ethereum Wiki: ERC20 Token Standard

), 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

This work is based on a long-standing collaboration with Mark S. Miller