Specifications for Robustness

Julian Mackay

Victoria University of Wellington

New Zealand

Sophia Drossopoulou

Meta, and Imperial College London

United Kingdom

James Noble

Creative Resaerch & Programming
5 Fernlea Ave, Darkest Karori

New Zealand

Susan Eisenbach

Imperial College London

United Kingdom

Robust modules guarantee to do only what they are supposed to
do – 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.
is a language for specifying robustness, based on novel necessity
operators capturing temporal implication, and a
proof logic that derives explicit robustness specifications from
. Soundness
and an exemplar proof
are mechanised in Coq.

<concept_desc>Software and its engineering General programming languages</concept_desc>
<concept_desc>Social and professional topics History of programming languages</concept_desc>

[500]Software and its engineering General programming languages

§ INTRODUCTION: NECESSARY CONDITIONS AND ROBUSTNESS

Software needs to be both correct (programs do what they
are supposed to) and robust (programs only do what they are supposed to).
We use the term robust as a generalisation of robust safety <cit.>  whereby a module or process or ADT is robustly safe if its execution preserves some safety guarantees even when run together with unknown,   unverified, potentially malicious client code.
The particular safety guarantees vary across the literature.
We are interested in program-specific safety guarantees which describe  necessary conditions
for some effect to take place.
In this work we propose how to specify such necessary conditions, and how to prove that modules adhere to such specifications.

We motivate the need for  necessary conditions for effects through an example:

Correctness is traditionally specified

through Hoare69 triples: a  precondition, a code snippet, and a
For example,  part of the of a transfer method for a bank module is that the source account's balance decreases:

$\{\,$pwd=src.pwd $\,\wedge\,$ src.bal=b$\,\}$ src.transfer(dst,pwd) $\{$ src.bal=b-100$\,\wedge\,\dots \}$  Calling transfer on  an account with the correct password will transfer the money.

Assuming termination, the precondition is a sufficient condition for the code snippet to behave correctly:

the precondition (providing the right
password) guarantees that
the code (call the transfer function)
will always achieve the postcondition (the money is transferred).

describes  the correct use of the  particular function, but is not concerned with the module's robustness.
For example, can I pass an account to foreign untrusted code, in the expectation of receiving a payment,
but without fear that a malicious client might use the account to steal my money <cit.>?
A first  attempt to specify robustness could be:

$\triangleq$   An account's balance does not decrease unless transfer was called
with the correct password.

guarantees that it is not possible to  take money out of the account

without calling transfer and without providing the password.
Calling transfer   with the  correct password is
a necessary condition for (the effect of) reducing the account's  balance.

is  crucial, but  not   enough:
it does not take  account of the module's emergent behaviour,
that is, does not cater for the potential interplay of several methods offered by the module.
What if the module provided further methods which leaked the password?

While no single procedure call is capable of breaking the intent of , a sequence of calls might.
What we really need is

$\triangleq$   The balance of an account does not ever decrease in the future unless some external
object  now has access to the account's current password.

With , I can confidently pass my account to  any, potentially untrusted context, where my password is not known;

the payment I was expecting may or may not be made,

but I know

that my money will not be stolen <cit.>.
Note that does not mention
the names of any functions in the module, and
thus can be expressed without reference to any particular API —
indeed can constrain any API with an account, an account
balance, and a password.

Earlier work addressing robustness includes object capabilities  <cit.>,
information control flow <cit.>,
correspondence assertions <cit.>,
sandboxing  <cit.>,
robust linear temporal logic   <cit.> – to name a few.
Most of these
propose generic  guarantees (e.g. no dependencies from high values to low values),
or preservation of module invariants,
while we work with  problem-specific  guarantees concerned with necessary conditions
for specific effects  (e.g. no decrease in balance without access to password).
VerX <cit.> and  Chainmail <cit.> also work on problem-specific guarantees.
Both these approaches are able to express necessary conditions
like using
temporal logic operators and implication,
and Chainmail is able to express ,
however neither have a proof logic
[removed:able] to prove adherence to such specifications.

In this paper we introduce , the first approach that is able to  both express and prove
(through an inference system)
robustness specifications such as  .
Developing a specification language with a proof logic that is able to prove properties such as
and must tread a fine line: the language must be rich enough to express complex specifications; temporal operators are needed along with object capability style operators
that describe permission and provenance, while also being simple enough that proof rules might be devised.

The first main contribution
is three novel operators that merge
temporal operators and implication
and most importantly are both expressive enough to capture the
examples we have found in the literature and provable through an inference system.

One such necessity operator is

\strut \hspace{1.7in} \onlyIf {A_{curr}} {A_{fut}} {A_{nec}}

This form says that
a  transition from a current state satisfying assertion $A_{curr}$ to a future
state satisfying $A_{fut}$  is possible only if  the   necessary
$A_{nec}$ holds in the current state.
Using this operator,
we can formulate  as
[language = Chainmail, mathescape=true, frame=lines]
$\text{\SrobustB}$  $\triangleq$   from   a:Account $\wedge$ a.balance==bal    to   a.balance < bal
onlyIf  $\exists$ o.[$\external{\texttt{o}}$ $\wedge$ $\access{\texttt{o}}{\texttt{a.pwd}}$]

Namely, a transition from a  current state where an account's balance is bal, to a  future state where
it has decreased, may only occur if  in the current state some external, unknown client object
has access to that account's password.
More    in <ref>.

Unlike  Chainmail's temporal operators,
the necessity operators
are  not first class, and may not appear in the assertions  (${A_{curr}}$).
This simplification enabled us to develop our proof logic.
Thus, we have reached a  sweet spot between expressiveness and

The second main contribution is  a logic that  enables us to prove that code
obeys specifications.
Our insight was  that specifications are logically equivalent to the
intersection of an infinite number of Hoare triples, i.e.,
$\onlyIf{A_1} {A_2} {A_3}$ is
logically equivalent

$\forall \prg{stmts}. \{ A_1 \wedge \neg A_3\} \prg{stmts} \{ \neg A_2 \}$.
Note that in the above, the assertions $A_1$, $A_2$ and $A_3$ are fixed, while the code (stmts) is universally quantified.
This leaves the challenge that, usually, Hoare logics do not support such infinite quantification over the code.

We addressed that  challenge through three further insights:
(1) specifications of emergent behaviour can be built up from specifications of
single-step executions, which (2) can be built from encapsulation and finite intersections
of specifications of function calls, which
(3) in turn can be obtained from traditional .

§.§ Contributions and Paper Organization

The contributions of this work are:

* A language to express specifications (<ref>), including three novel operators (<ref>) that combine implication and temporal operators.

* A logic for proving a module's adherence to its
specifications (<ref>), and a proof of soundness of the logic, (<ref>),
both mechanised in Coq []<cit.>.

* A proof in our logic
that our bank module obeys
(<ref>),     mechanised in Coq.
And a proof that
a richer bank module which uses ghostfields and confined classes  obeys  (<ref>),
also mechanised in Coq.

*  Examples taken from the literature  (<ref> and <ref>) specified in .

We place into the context of
related work (<ref>) and consider our overall conclusions

The Coq proofs of
(2) and (3) above appear in the
supplementary material, along with appendices containing expanded
definitions and further examples.
In the next section, (<ref>),  we outline our approach using a
bank   as  a motivating example.

A strength of our work
is that it is
parametric with respect to assertion
satisfaction and functional specifications – these questions are well covered in the literature,
and offer several off-the-shelf solutions.

The current work is based on
a simple, imperative, typed, object oriented
language with unforgeable addresses and private fields; nevertheless,
we believe
that   our approach
is applicable to several programming paradigms, and
that   unforgeability and privacy
can be replaced
by lower level mechanisms such as capability machines <cit.>.
In line  with other work in the literature, we do not –yet– support
“callbacks” out from internal objects (whose code gas been checked) to  external objects (ie unknown objects
whose code has not been checked).

§ OUTLINE OF OUR APPROACH

In this Section we outline our approach:
we  revisit  our running example, the Bank Account (<ref>),
introduce the three necessity operators (<ref>),  give
the specs (<ref>),
outline how we model the open world (<ref>),
give the main ideas of our proof system (<ref>)
and   outline
how we use it to reason
about adherence to specifications  (<ref>).

§.§ Bank Account – three modules

Module consists of an empty
Password class where each instance models a unique password, and an  Account class with a password, and a balance, an init method to
initialize the password, and
transfer method.
Note that we assume that all  fields are  “class-private”,
i.e., methods may read and write fields of any instance of the same class,
and  that passwords are unforgeable and not enumerable (as
in Java, albeit without reflection.

[mathescape=true, language=Chainmail, frame=lines]
module $\ModA$
class Account
field balance:int
field pwd: Password
method transfer(dest:Account, pwd':Password) -> void
if this.pwd==pwd'
method init(pwd':Password) -> void
if this.pwd==null
class Password

We can capture the intended semantics of   transfer
through  a  with pre- and post- conditions and MODIFIES clauses as e.g., in .
The implementation of  transfer in module  $\ModA$ meets
this specification.

[mathescape=true, frame=lines, language=Chainmail]
$\Sclassic$  $\triangleq$
method transfer(dest:Account, pwd':Password) -> void
this.pwd$=$pwd' $\wedge$ this$\neq$dest  $\longrightarrow$
this.balance$_{post} =$this.balance$_{pre}$-100 $\wedge$ dest.balance$_{post} =$dest.balance$_{pre}$+100
this.pwd$\neq$pwd' $\vee$ this$=$dest  $\longrightarrow$
this.balance$_{post} =$this.balance$_{pre}$ $\wedge$ dest.balance$_{post} =$dest.balance$_{pre}$
MODIFIES:  this.balance, dest.balance

Now consider the following alternative implementations:
allows any client to reset an account's password at any time;
requires the existing password in order to change it.

[mathescape=true, language=chainmail, frame=lines]
module $\ModB$
class Account
field balance:int
field pwd: Password
method transfer(..) ...
... as earlier ...
method init(...) ...
... as earlier ...
method set(pwd': Password)

class Password

[mathescape=true, language=chainmail, frame=lines]
module $\ModC$
class Account
field balance:int
field pwd: Password
method transfer(..)
... as earlier ...

method set(pwd',pwd”: Password)
if (this.pwd==pwd')
class Password

Although the transfer method is the same in
all three alternatives, and each one satisfies ,
code  such as

$\ \strut \hspace{.2in} $ an_account.set(42); an_account.transfer(rogue_account,42)

is enough to drain  an_account in without knowing the password.

This example also demonstrates the importance of field privacy: $\ModA$ and $\ModC$ would not be any
more robust than $\ModB$ if the underlying programming language did not restrict access to fields. Without
such a restriction,
any external object would have been able to directly manipulate the fields balance and pwd.

§.§ The three necessity operators

We need  a specification that rules out while permitting and
.  For this, we will be using  one of the  three necessity operators mentioned in  <ref>. These operators are:

$ \strut \hspace{1.7in} \onlyIf {A_{curr}} {A_{fut}} {A_{nec}} $

$ \strut \hspace{1.7in}   \onlyIfSingle {A_{curr}} {A_{fut}} {A_{nec}} $

$ \strut \hspace{1.7in}   \onlyThrough {A_{curr}} {A_{fut}} {A_{intrm}} $

The first operator was already introduced in <ref>: it says that
a  transition from a current state satisfying assertion $A_{curr}$ to a future
state satisfying $A_{fut}$  is possible only if  the   necessary
$A_{nec}$ holds in the current state.

The  second operator says    that
a  one-step transition from a current state satisfying assertion $A_{curr}$ to a future
state satisfying $A_{fut}$
is possible only if
$A_{nec}$ holds in the current state.
The   third operator   says that a change from
$A_{curr}$ to  $A_{fut}$  may happen only if
$A_{intrm}$ holds in some intermediate state.

Our assertions $A$, also allow for the use of capability operators, such as
1) having access to an object ($\access{\prg{o}}{\prg{o'}}$) which means that $\prg{o}$ has a reference to $\prg{o'}$,
or 2) calling a method with on receiver with certain arguments,
($\calls{\prg{o}}{\prg{o'}}{\prg{m}}{\prg{args}} $), or 3) an object being external,
where  $\external{\prg{o}}$ means that o belongs to a class that is not defined in the current module,
and thus its behaviour is unrestricted.
These are the capability operators that we have
adopted from Chainmail.

§.§ Bank Account – the right specification

We now return to our quest for a specification that rules out while permitting and
. The catch is that the vulnerability present in is the result
of  emergent behaviour from the interactions of the set
and transfer methods — even though also has a
set method, it does not exhibit the unwanted interaction.
This is exactly where a necessary condition can help:
we want to avoid transferring money
(or more generally, reducing an account's balance)
without the existing account password.  Phrasing the same condition
the other way around
rules out the theft: that money can only be
transferred when the account's password is known.

In syntax, and recalling <ref>, and <ref>,

[language = Chainmail, mathescape=true, frame=lines]
$\text{\SrobustA}$  $\triangleq$   from   a:Account $\wedge$ a.balance==bal    next    a.balance < bal
onlyIf $\exists$ o,a'. [$\external{\prg{o}}$ $\wedge$ $\calls{\prg{o}}{\prg{a}}{\prg{transfer}}{\prg{a'},\prg{a.pwd}} $]

$\text{\SrobustB}$  $\triangleq$   from   a:Account $\wedge$ a.balance==bal    to    a.balance < bal
onlyIf $\exists$ o.[$\external{\prg{o}}$ $\wedge$ $\access{\prg{o}}{\prg{a.pwd}}$]

does not fit the bill: all three modules   satisfy  it.

But  does fit the bill: and satisfy , while does not.

A critical point of
is that it is
expressed in terms of observable effects (the account's balance is
reduced: a.balance < bal) and the shape of the heap
(external access to the password:
$\external{\prg{o}}\ \wedge\ \access{\prg{o}}{\prg{a.pwd}}$)
rather than in terms of individual methods such as
set and transfer.
This gives our specifications the
vital advantage that they can be used to constrain
[typo]implementations of a bank account with a balance and a
password, irrespective of the API it
offers, the services it exports, or the dependencies on other parts of
the system.

This example also demonstrates that
adherence to   specifications is not monotonic:
adding a method to a module does not necessarily preserve adherence to
a specification,
and while separate methods may adhere to a  specification, their combination does
not necessarily do so.
For example, satisfies , while does not.
This is why we say that specifications capture a module's emergent behaviour.

§.§.§ How  useful is  ?

One might think that was not useful: normally, there will exist somewhere in the heap
at least one external object
with access to the password –  if no such object existed, then nobody would be able to use the money of
the account.
And if such an object did exist, then the premise of would not hold, and thus
the guarantee given by might seem vacuous.

This is not so:
in scopes   from which such external objects with access to the password
are not (transitively) reachable,
guarantees that the balance of the account will not decrease.

We illustrate this through the following  code snippet:

[mathescape=true, language=chainmail, frame=lines]
module $\ModParam{1}$
method cautious(untrusted:Object)
a = new Account
p = new Password

The method cautious has as  argument an external object untrusted, of unknown provenance.
It creates a new Account and initializes its password.
In the scope of  this method,  external objects with access to the password are reachable:
thus,  during execution of  line 7, or   line 9 the balance may decrease.

Assume that class Account is from a module which satisfies .
Assume also that the code in line 7 does not leak the password to untrusted. Then no external object
reachable from the scope of execution of make_payment at line 8 has access to the password.
even though we are calling   an untrusted object, guarantees that untrusted
will not be able to take any money out of  a.

A  proof sketch of the  safety provided by appears in Appendix <ref>.

Note that in this example, we have (at least) three modules: the internal module
which defines class Account adhering to  , the
external module $\ModParam{1}$, and the external module which contains the class definition for untrusted.
Our methodology allows the external module, $\ModParam{1}$ to reason about its own code, and thus
pass a to code from the second external module, without fear of losing money.
In further work we want to make such arguments more generally applicable, and
extend Hoare logics to encompass such proof steps.

§.§ Internal and external modules, objects, and calls

Our work concentrates on guarantees made in an open setting; that is, a given module
$M$ must be programmed so that
execution of $M$ together with any module $M'$ will uphold these guarantees. In the tradition of
visible states semantics, we are  only interested in upholding the guarantees while
$M'$, the   module, is executing. A module can
temporarily break its own invariants,
so long as the broken invariants are never visible externally.

We therefore distinguish between
objects — instances of classes defined in $M$ —
and  objects defined in any other module.
We also distinguish between
calls  (from either an internal or an external object)  made
to objects and  calls made
to objects.
Looking at the code snippet from <ref>, the call to set on line 6 is an
internal call, while the call to make_payment is an external call – from the external
object  this  to the external object untrusted.

Because we only require guarantees while
the  module  is executing,
we develop an external states semantics, where
any internal calls are executed in one, large, step.
With external steps semantics,  the executing object (this) is always   external.
In line  with other work in the literature <cit.>, we currently forbid
calls from internal to  external objects
– further details on call-backs in <ref>.

For the purposes of the current work we are only interested in one internal, and one external module.
But the interested reader might ask: what if there is more than one external module?
The answer is that from the internal module's viewpoint, all external modules are considered as one;
for this we provide a module linking operator with  the expected semantics – more details in Def. <ref> and <ref>.
But from the external module's viewpoint, there may be more than one external module: for example, in <ref>,
module $\ModParam{1}$ is external to the module   implementing class Account, and the module
implementing the class of untrusted is external to

§.§ Reasoning about

We will now outline the key ingredients of  our logic with which we prove
that modules obey specifications.
We will use the auxiliary concept that
an assertion $A$ is encapsulated by
a module $M$, if  $A$  can only be invalidated through
a call to a method from $M$ – more   in <ref>.

The logic is based on the insight that the specification

$\hspace{1in}$  $\onlyIf{A_1} {A_2} {A_3}$

is  logically equivalent to

$\hspace{1in}$  $\forall \prg{stmts}. \{ A_1 \wedge \neg A_3\} \prg{stmts} \{ \neg A_2 \}$

– that is,
with an infinite conjunction  of Hoare triples, where the three assertions are fixed, but the code,
stmts, is universally quantified.
This leaves the challenge that [changed "no Hoare logics support"]usually, Hoare logics do
not support such infinite conjunctions over code.
Three [dropped breakthroughs]ideas helped us address   that challenge:

From Hoare triples to per-call specs
The Hoare triple
$ \{ A_1 \wedge \neg A_3 \} \ \prg{x.m(ys)}\  \{ \neg A_2 \}$ is logically equivalent
to the specification
$ \onlyIfSingle {(A_1 \wedge  \calls{\_}{\prg{x}}{\prg{m}}{\prg{ys}} )} {A_2} {A_3}$.

From per-call specs to per-step specs
If an assertion $A_2$  is encapsulated by a module – and thus the only way from a
state that satisfies $A_2$ to a state that does not, is through a call to a method in that module – then
finite conjunction
that all methods of that module $ \onlyIfSingle {(\, A_1 \wedge A_2 \wedge {\calls{\_}{\prg{x}}{\prg{m}}{\prg{ys}}}\, )} {\neg  A_2} {A_3}$
is logically equivalent
$ \onlyIfSingle {A_1 \wedge A_2} {\neg A_2} {A_3}$.

Proof logic  for emergent behaviour
combines several specifications to reason about the
emergent behaviour, e.g.,
$ \onlyThrough  {A_1} {A_2} {A_3}$  and $ \onlyIf  {A_1} {A_3} {A_4}$ implies
$ \onlyIf  {A_1} {A_2} {A_4}$.

Thus, our system consists of four parts (five including ):
(Part 1) assertion encapsulation, (Part 2) per-method specifications,
(Part 3) per-step specifications, and (Part 4) specifications of emergent behaviour.
The structure of the system, and the dependency of each part on preceding parts is given in Fig. <ref>.
are used to prove []per-method specifications, which coupled with
assertion encapsulation is used to prove per-step specifications, which is used to
prove specifications of emergent behaviour.

Parts of Logic and their Dependencies.
Note that gray parts with a dashed border indicate
parts that are not part of , and on which is parametric.

Our logic  is parametric with respect to  the way we ascertain whether an assertion
is encapsulated and the way we obtain .
As a result we can leverage  results from many different approaches.
Further, our proofs of do not inspect method
bodies: we rely on simple annotations to infer encapsulation, and
on pre and post-conditions  to infer per-method conditions.

§.§ Outline of the proof that  obeys

For illustration, we  outline  a proof that  adheres to .
note that for illustration purposes, in this paper we show how assertion encapsulation can be proven
based on simple annotations inspired by confinement types
<cit.>; we could just as easily rely  on other language mechanisms,  e.g., ownership types,
or even develop custom  logics.

Part 1: Assertion Encapsulation.

We begin by proving that encapsulates:

(A) The balance

(B) The password

(C) External accessibility to an account's password –
that is, the property that no external object has access to the password may only
be invalidated by calls to .

Part 2: Per-Method Specifications

We prove that the call of any  method from (set and transfer)

(D) If the balance decreases, then
transfer was called with the correct password

(E) If the password changes, then the method called was
set with the correct password

(F) It will not provide external accessibility to the password.

Part 3: Per-step Specifications

We then raise our results of Parts 1 and 2 to reason about arbitrary single-step executions:

By (A) and (D) only transfer and external access to the password may decrease the balance.

By (B) and (E) only set and external access to the password may change the password.

By (C) and (F) no step may grant external accessibility to an account's password.

Part 4: Specifications of Emergent Behaviour

We then raise our necessary conditions of Part 3 to reason about arbitrary executions:

A decrease in balance over any number of steps implies that some single intermediate step
reduced the account's balance.

By (F) we know that step must be a call to transfer with the correct password.

When transfer was called, either

The password used was the current password, and thus by (H) we know that
the current password must be externally known, satisfying , or

The password had been changed, and thus by (G) some intermediate step must have been
a call to set with the current password. Thus, by (H) we know that
the current password must be externally known, satisfying .

§ THE MEANING OF NECESSITY

In this section we define the  specification language.
We first define an underlying programming language, (<ref>).
We then define an assertion language, , which can talk about the
contents of the state, as well as about provenance, permission and
control (<ref>).  Finally, we define the syntax and
semantics of our full language for writing specifications (<ref>).

is a [removed: formal model of a] small, imperative, sequential,
class based, typed, object-oriented language, whose
fields are private to the class where they are defined.
is straightforward:

Appendix <ref> contains
the full definitions.

is based on <cit.>, with some small variations, as well as
the addition of
a simple type system – more in <ref>.

A state $\sigma$ consists of a
heap $\chi$, and a  stack $\psi$ which is a sequence of frames.
A frame $\phi$ consists of
local variable map, and a continuation, a sequence of statements to be executed.
A statement may assign to variables, create new objects and push them to the heap,
perform field reads and writes on objects,  or
call methods on those objects.

Modules are mappings
from class names to class definitions.

is in the context of  a module $M$ and   a state $\sigma$,

defined via unsurprising small-step semantics of the form
$M, \sigma \leadsto \sigma'$.
The   top frame's continuation contains the statement to be
executed next.

As discussed in <ref>,
open world specifications need to be able to provide
guarantees which hold
during execution of an internal,
known, trusted module $M$ when linked together with any
unknown, untrusted, module $M'$. These guarantees need only hold
when the external module is executing; we are not concerned if they are
temporarily broken by the internal module. Therefore, we are only interested in states where the
executing object (this) is an external object.
To express our focus on external states, we define the  external states semantics, of the form
$\reduction{M'}{M}{\sigma}{\sigma'}$, where $M'$ is the external
module, and $M$ is the internal module, and where we
collapse all internal steps into one single step.

modules $M$,  $M'$, and
states $\sigma$, $\sigma'$,
we say that $\ \ \ \ \ \ \ \ \reduction{M'}{M}{\sigma}{\sigma'}\ \ \ \ \ \ \ \ $ if and only if there exist
$n\in\mathbb{N}$, and states $\sigma_0$,...$\sigma_n$, such that

* $\sigma$=$\sigma_1$, and  $\sigma'$=$\sigma_n$,

* $M' \circ M, \sigma_i \leadsto \sigma_{i+1}$     for all $i\in [0..n)$,

* $\class{\sigma}{\scd{\prg{this}}}, \class{\sigma'}{\scd{\prg{this}}}\in M'$,

* $\class{\sigma_i}{\scd{\prg{this}}} \in M$   for all $i\in (1..n)$.

The function $\class{\sigma}{\_}$ is overloaded:
applied to a variable,
$\class{\sigma}{x}$  looks up the variable $x$ in the top frame of $\sigma$, and returns the
class of the corresponding object in the  heap of $\sigma$;

applied to an address, $\class{\sigma}{\alpha}$  returns
the class of   the object referred by address $\alpha$ in the heap of $\sigma$.
The module linking operator $\circ$, applied to two modules, $M'\circ M$,
combines the two modules into one module in the obvious way, provided their
domains are disjoint.
Full details in  Appendix <ref>.

External States Semantics
(Def. <ref>),

(A) $\exec{{\color{hotpink}M'} \circ {\color{lightseagreen}M}}{\sigma_1}{\ldots}\leadsto \sigma_9$    and
(B) $\reduction{{\color{hotpink}M'}}{{\color{lightseagreen}M}}{\sigma_2}{\ldots}\leadsto \sigma_9$,

where $\class{{\color{lightseagreen}\sigma_1}}{\scd{\prg{this}}}$,$\class{{\color{lightseagreen}\sigma_3}}{\scd{\prg{this}}}$,$\class{{\color{lightseagreen}\sigma_4}}{\scd{\prg{this}}}$,$\class{{\color{lightseagreen}\sigma_7}}{\scd{\prg{this}}}$,$\class{{\color{lightseagreen}\sigma_8}}{\scd{\prg{this}}}\in {\color{lightseagreen}M}$,

and where $\class{{\color{hotpink}\sigma_2}}{\scd{\prg{this}}},\class{{\color{hotpink}\sigma_5}}{\scd{\prg{this}}}
\class{{\color{hotpink}\sigma_6}}{\scd{\prg{this}}},\class{{\color{hotpink}\sigma_9}}{\scd{\prg{this}}}\in {\color{hotpink}M'}$.

Fig. <ref> inspired by FASE provides a simple graphical description of
our external states semantics: (A) is the “normal” execution after
linking two modules into one:  $M' \circ M, ... \leadsto ...$ whereas (B) is the
external states execution when $M'$ is external,   $\reduction{M'}{M}{...}{...}$.
Note that whether a module is external or internal depends on
perspective – nothing in a module itself renders it internal or external. For example, in
$\reduction{M_1}{M_2}{...}{...}$ the external module is $M_1$,
while in  $\reduction{M_2}{M_1}{...}{...}$  the external module is $M_2$.

We  use the notation   $\reductions{M'}{M}{\sigma}{\sigma'}$
to denote zero or more  steps starting at state $\sigma$ and ending at state $\sigma'$, in the context of internal module
$M$ and external module $M'$.

We are []not concerned with internal states or states that can never arise.
A state $\sigma$ is arising,  written $\arising{M'}{M}{\sigma}$, if it  may arise by external states execution
starting at some initial configuration:

For   modules $M$ and  $M'$, a
state $\sigma$ is
called an arising state, formally    $\arising{M'}{M}{\sigma}$,
if and only if there exists some $\sigma_0$ such that $\initial{\sigma_0}$ and

An Initial state's heap
contains a single object of class Object, and
its  stack   consists of a single frame, whose local variable map is a
mapping from this to the single object, and whose continuation is  any statement.
(See Definitions <ref> and <ref>).

While our work is based on
a simple, imperative, typed, object oriented
language with unforgeable addresses and private fields, we believe
it is applicable to several programming paradigms, and
that   unforgeability and privacy
can be replaced
by lower level mechanisms such as capability machines <cit.>.

is [removed: a subset of the Chainmail assertions language, ]
a basic assertion language extended with
object-capability assertions.

§.§.§ Syntax of

The syntax of is given in
Definition <ref>.
An assertion may be an expression,   a query of the defining class of
an object, the usual connectives and quantifiers, along
with three non-standard assertion forms:
(1) Permission and (2) Provenance, inspired by the capabilities literature, and
(3) Control which allows tighter  characterisation of the cause of effects –
useful for the specification of large APIs.

* Permission ($\access{x}{y}$):
$x$ has access to $y$.

* Provenance ($\internal{x}$ and $\external{y}$):   $x$ is an internal [](i.e. trusted) object, and $y$ is an external [](i.e. untrusted) object.

* Control ($\calls{x}{y}{m}{\overline{z}}$):
$x$ calls method $m$ on object $y$ with arguments $\overline{z}$.

Assertions ($A$) in
are defined as follows:

\[
\begin{syntax}
\syntaxElement{A}{}
\syntaxline
{e : C}
{\neg A}
{A\ \wedge\ A}
{A\ \vee\ A}
\endsyntaxline
\syntaxline
%		\endsyntaxline
%		}
%		{
%		\syntaxline
\endsyntaxline
\endSyntaxElement\\
\end{syntax}
\]

§.§.§ Semantics of

The semantics of is given in Definition <ref>.
We   use the evaluation relation, $\eval{M}{\sigma}{e}{v}$,
which says that the expression $e$ evaluates
to value $v$ in the context of state $\sigma$ and module $M$.
Note that expressions in may be recursively defined, and thus evaluation
need not [removed: always]
terminate. Nevertheless, the logic of $A$ remains classical because recursion is restricted
to expressions, and not generally to assertions.
We have taken this approach from FASE, which also contains a mechanized Coq proof that assertions are classical <cit.>.

The semantics of $\hookrightarrow$ []is unsurprising (see Fig.<ref>).

$\interpret{\phi}{x} = v$  means that $x$ maps to
value $v$ in the local variable map of frame $\phi$, $\interpret{\sigma}{x} = v$ means that $x$
maps to $v$ in the top most frame of $\sigma$'s stack, and $\interpret{\sigma}{x.f} = v$
has the obvious meaning. The terms $\sigma.\prg{stack}$,

$\sigma.\prg{heap}$     mean the stack,

the continuation at the
top frame of $\sigma$,
and the heap of $\sigma$.
The term $\alpha\!\in\!\sigma.\prg{heap}$ means that $\alpha$ is in the domain of the heap of $\sigma$, and $x$ fresh in $\sigma$ means that
$x$ isn't in the variable map of the top frame of $\sigma$,
while the substitution  $\sigma[x \mapsto \alpha]$ is applied to the top frame of $\sigma$.
[added extra space] $C\in M$ means that class $C$ is in the domain of module $M$.

We define satisfaction of an assertion $A$ by a
state $\sigma$ with
module $M$ as:

$\satisfiesA{M}{\sigma}{e}$    iff     $\eval{M}{\sigma}{e}{\true}$

$\satisfiesA{M}{\sigma}{e : C}$    iff     $\eval{M}{\sigma}{e}{\alpha}$ and $\class{\sigma}{\alpha} = C$

* $\satisfiesA{M}{\sigma}{\neg A}$    iff     ${M},{\sigma}\nvDash{A}$

* $\satisfiesA{M}{\sigma}{A_1\ \wedge\ A_2}$    iff     $\satisfiesA{M}{\sigma}{A_1}$ and

* $\satisfiesA{M}{\sigma}{A_1\ \vee\ A_2}$    iff     $\satisfiesA{M}{\sigma}{A_1}$ or

$\satisfiesA{M}{\sigma}{\all{x}{A}}$    iff
$\satisfiesA{M}{\sigma[x \mapsto \alpha]}{A}$,
for some $x$ fresh in $\sigma$, and for all $\alpha\!\in\!\sigma.\prg{heap}$.

$\satisfiesA{M}{\sigma}{\ex{x}{A}}$    iff
$\satisfiesA{M}{\sigma[x \mapsto \alpha]}{A}$,
for some $x$ fresh in $\sigma$, and for some $ \alpha\!\in\!\sigma.\prg{heap}$.

$\satisfiesA{M}{\sigma}{\access{x}{y}}$    iff

$\interpret{\sigma}{x.f}={\interpret{\sigma}{y}}$ for some $f$,

$\interpret{\sigma}{x}=\interpret{\phi}{\prg{this}}$, $\interpret{\sigma}{y}=\interpret{\phi}{z}$, and $z\ \in\ \phi.\prg{contn}$   for some variable $z$, and some frame $\phi$ in $\sigma.
\prg{stack}$.

$\satisfiesA{M}{\sigma}{\internal{x}}$    iff
$\textit{classOf}(\sigma,x) \in M$

$\satisfiesA{M}{\sigma}{\external{x}}$    iff
$\textit{classOf}(\sigma,x) \not\in M$

$\satisfiesA{M}{\sigma}{\calls{x}{y}{m}{z_1, \ldots, z_n}}$    iff

* $\sigma.\prg{contn} = (w := y'.m(z'_1,\ldots,z'_n)\scd{; s})$,  for some
variable $w$, and some statement $s$,

* $\satisfiesA{M}{\sigma}{x = \prg{this}}$
$\satisfiesA{M}{\sigma}{y = y'}$,

* $\satisfiesA{M}{\sigma}{z_i = z'_i}$   for all $1\!\leq i\!\leq n$

Quantification (defined in <ref> and <ref>) is done over all objects on the heap.
We do not include quantification over primitive types such as integers as is too simple. The
Coq mechanisation does include primitive types.

The assertion ${\access{x}{y}}$ (defined in  <ref>)
requires  that $x$ has access to $y$
either through a field of $x$ (case <ref>),
or through some call in the stack, where $x$ is the receiver and $y$ is one of the
arguments (case <ref>).
Note that access is not deep, and only refers to objects that
an object has direct access to via a field or within the context of a current scope.

The restricted form of access used in specifically captures a crucial property of robust programs in the open world: access to an object does not imply access to that object's internal data. For example, an object may have access to an account a, but a safe implementation of the account would never allow that object to leverage that access to gain direct access to a.pwd.

The assertion
${\calls{x}{y}{m}{z_1, \ldots, z_n}}$  (defined in <ref>)
describes the current innermost active call. It
requires that the current receiver (this) is $x$, and that it calls the method $m$ on $y$ with
arguments $z_1$, ... $z_n$ – It does not mean  that somewhere in the
call stack there exists a call from $x$ to $y.m(...)$.
Note that in most cases, satisfaction of an assertion not only depends on the state $\sigma$, but
also depends on the module in the case of expressions (<ref>), class membership
(<ref>), and internal or external provenance (<ref> and <ref>).

We now define what it means for a module to satisfy an assertion:
$M$ satisfies  $A$ if any state arising from external steps execution of that
module with any other external module  satisfies $A$.

For a module $M$ and assertion $A$, we say that   $\satisfies{M}{A}$   if and only if
for all modules $M'$, and all $\sigma$, if $\arising{M'}{M}{\sigma}$, then $\satisfiesA{M}{\sigma}{A}$.

In the current work we assume the existence of a proof system that judges
$\proves{M}{A}$, to prove  satisfaction of assertions.
We will not define such a judgement, but will rely on its existence later on for Theorem <ref>.
We define soundness of such a judgement in the usual way:

A judgement of the form $\proves{M}{A}$ is sound, if for all
modules $M$ and assertions $A$,  if $\proves{M}{A}$ then $\satisfies{M}{A}$.

§.§.§ Inside

We define
a final shorthand
predicate $\wrapped{\prg{o}}$ which states
that only objects have access to o.
The object o may be either or .

$\wrapped{o}\ \triangleq\ \all{x}{\access{x}{o}\ \Rightarrow\ \internal{x}} $

is a very useful concept. For example, the balance of an account whose
password is will not decrease in the next step.
Often, API implementations contain objects whose capabilities, while  crucial for the implementation, if exposed,
would break the intended guarantees of the API. Such objects need to remain - see
such an example in Section <ref>.

§.§ operators

§.§.§ Syntax of Specifications

The specification language extends with our three novel
[] operators:

[$\onlyIfSingle{A_1}{A_2}{A}$]: If an arising
state satisfies $A_1$, and a single execution step reaches  a state satisfying $A_2$,
then the original
state must have also satisfied $A$.

[$\onlyIf{A_1}{A_2}{A}$]: If an arising
state satisfies $A_1$ and a number of execution steps reach a state   satisfying $A_2$,
then the original
state must have also satisfied $A$.

[$\onlyThrough{A_1}{A_2}{A}$]: If an arising
state satisfies $A_1$, and a number of execution steps reach a state
satisfying $A_2$,  then  execution must have passed through some intermediate state satisfying $A$.

The syntax of  specifications is given below

Syntax of Specifications

\[
\begin{syntax}
\syntaxElement{S}{}
\syntaxline
% \endsyntaxline
% }
% \syntaxline
\endsyntaxline
\endSyntaxElement\\
\end{syntax}
\]

As an example, we consider the following three  specifications:

[language = Chainmail, mathescape=true, frame=lines]
$\text{\SRobustNextAcc}$   $\triangleq$  from a:Account $\wedge$ a.balance==bal  next a.balance < bal
onlyIf $\exists$ o.[$\external{\texttt{o}}$ $\wedge$ $\access{\prg{o}}{\prg{a.pwd}}$]
$\text{\SRobustIfAcc}$   $\triangleq$  from a:Account $\wedge$ a.balance==bal  to a.balance < bal
onlyIf $\exists$ o.[$\external{\texttt{o}}$ $\wedge$ $\access{\prg{o}}{\prg{a.pwd}}$]
$\text{\SRobustThroughAcc}$   $\triangleq$  from a:Account $\wedge$ a.balance==bal  next a.balance < bal
onlyThrough $\exists$ o.[$\external{\texttt{o}}$ $\wedge$ $\access{\prg{o}}{\prg{a.pwd}}$]

requires that an account's balance may decrease in one step (go from a state where the balance is bal
to a state where it is less than bal) only if the password is accessible to an external object (in the original state an external object had access to the password).
requires that an account's balance may decrease in any number of steps    only if the password is accessible to an external object.
requires that an account's balance may decrease in any number of steps    only if in some intermediate state the password was accessible to an external object –  the   intermediate state  where the password is accessible to the external object might be the starting
state, the final state, or any state in between.

§.§.§ Semantics of Specifications

We now  define what it means for  a module  $M$ to satisfy specification  $S$, written as $M \vDash S$. The
Definition <ref> below is straightforward, apart from
the use of the $\adapt  {\sigma'}{\sigma}$  (best read as “$\sigma'$ seen
from $\sigma$”)

to deal with the fact that execution might  change the bindings in local variables.
We explain this in detail in   <ref>, but for now, the reader may ignore the applications of that operator and
read $\sigma' \triangleleft \sigma$ as $\sigma'$,
and also read ${\sigma_k \triangleleft \sigma_1}$ as  $\sigma_k$.
We illustrate the meaning of the three operators in
Fig. <ref>.

Illustrating the three operators

We define $\satisfies{M}{{S}}$ by cases over the four possible syntactic forms.
For any assertions   $A_1$, $A_2$, and $A$:

$\bullet$  $\satisfies{M}{{A}}$    iff   for all $M'$, $\sigma$, if $\arising{M'}{M}{\sigma}$, then $\satisfiesA{M}{\sigma}{A}$. (see Def. <ref>)

$\bullet$  $\satisfies{M}{\onlyIf {A_1}{A_2}{A}}$   iff   for all $M'$, $\sigma$, $\sigma'$, such that $\arising{M'}{M}{\sigma}$:

$\;\;\;\;$- $\satisfiesA{M}{\sigma}{A_1}$      }33mm[$\;\;\;\Rightarrow\;\;\;$  $\satisfiesA{M}{\sigma}{A}$]

$\;\;\;\;$- $\satisfiesA{M}{\sigma' \triangleleft \sigma}{A_2}$

$\;\;\;\;$- $\reductions{M'}{M}{\sigma}{\sigma'}$

$\bullet$   $\satisfies{M}{\onlyIfSingle {A_1}{A_2}{A}}$  iff    for all $M'$, $\sigma$,   $\sigma'$, such that $\arising{M'}{M}{\sigma}$:

$\;\;\;\;$- $\satisfiesA{M}{\sigma}{A_1}$      }33mm[$\;\;\;\Rightarrow\;\;\;$  $\satisfiesA{M}{\sigma}{A}$]

$\;\;\;\;$- $\satisfiesA{M}{\sigma' \triangleleft \sigma}{A_2}$

$\;\;\;\;$- $\reduction{M'}{M}{\sigma}{\sigma'}$

$\bullet$   $\satisfies{M}{\onlyThrough {A_1}{A_2}{A}}$   iff   for all $M'$, $\sigma_1$,  $\sigma_2$,  .... $\sigma_n$, such that $\arising{M'}{M}{\sigma_1}$:

$\;\;\;\;$- $\satisfiesA{M}{\sigma_1}{A_1}$      }33mm[$\;\;\;\Rightarrow\;\;\;$  $\exists k. \ 1\leq k \leq n \ \wedge \ \satisfiesA{M}{\sigma_k \triangleleft \sigma_1}{A}$]

$\;\;\;\;$- $\satisfiesA{M}{\sigma_n\triangleleft \sigma\sd{_1}}{A_2}$

$\;\;\;\;$- $\forall i\!\in\![1..n).\ \reduction{M'}{M}{\sigma_i}{\sigma_{i+1}}$

Revisiting the examples from the previous subsection, we obtain that all three modules satisfy
$\SRobustNextAcc$. But $\ModB$ does not satisfy $\SRobustIfAcc$: as  already discussed in <ref>,
with a of class Account implemented as in $\ModB$,
starting in a state where no external object has access to a's password, and executing
a.set(42); a.transfer(rogue_account,42) leads to a state where the balance has decreased.
All three modules satisfy $\SRobustThroughAcc$: namely, in all cases, the balance can only decrease if
there was a call to a.transfer(_,p) where $\prg{p}=\prg{a.pwd}$, and since that call can only be made from an external object,
p is externally known at the time of that call.

\   & \ModA \vDash \SRobustNextAcc  \   & \ModB \vDash \SRobustNextAcc \
& \ModC \vDash \SRobustNextAcc \\
\   & \ModA \vDash \SRobustIfAcc  \   & \ModB \nvDash \SRobustIfAcc \
& \ModC \vDash \SRobustIfAcc \\
\   & \ModA \vDash \SRobustThroughAcc  \   & \ModB \vDash \SRobustThroughAcc \
& \ModC \vDash \SRobustThroughAcc \\
\end{array}$

§.§.§ Adaptation

We  now discuss  the adaptation operator.  To see the need,
consider  specification
[language = Chainmail, mathescape=true, frame=lines]
$\text{\Sadapt}$   $\triangleq$  from a:Account $\wedge$ a.balance==350  next a.balance == 250
onlyIf $\exists$ o.[$\external{\texttt{o}}$ $\wedge$ $\calls{\prg{o}}{\prg{a}}{\prg{transfer}}{\prg{\_, \_, \_}}$]

Without adaptation, the semantics of  would be: If
$..,\sigma  \models \prg{a.balance==350}$,
and  $.., \sigma  \leadsto^* \sigma'$ and $\sigma' \models \prg{a.balance==250}$,
between $\sigma$ and $\sigma'$ there must be
call to   a.transfer.
But if $\sigma$ happened to have another account a1 with balance
350, and if we reach $\sigma'$ from $\sigma$ by executing a1.transfer($..,..$); a=a1, then we would
reach a $\sigma'$
without a.transfer having been called: indeed, without the
account a from $\sigma$  having changed at all.

In fact, with such a semantics,  a module would satisfy $\Sadapt$ only if it did not support decrease of []the balance by $100$, or
[]if states where an account's balance is 350 were unreachable!

This is the remit of the adaptation operator: when we consider the
future state, we must “see it from” the perspective of the current
state; the binding for variables such as a must be from the
current state, even though we may have assigned to them in the mean
time.  Thus, $\adapt {\sigma'} {\sigma}$ keeps the heap from $\sigma'$,
and renames the variables
in the top stack frame of  $\sigma'$ so that all variables defined in $\sigma$ have the same

as in   $\sigma$; the continuation must be adapted similarly (see
Fig. <ref>).

Under adaptation, the semantics of is:  if $..,\sigma \models \prg{a.balance==350}$,
and  $.., \sigma \leadsto^* \sigma'$ and $..., \boldsymbol{\adapt {\sigma'}{\sigma}} \models \prg{a.balance==250}$,

then some intermediate state's continuation must contain  a call to a.transfer;
where,  all variables bound in the initial state, $\sigma$,
have the same bindings in $\adapt {\sigma'}{\sigma}$.
[I didn't understand susan's comment on this paragraph: “problem with primes”]

Fig. <ref> illustrates the semantics of $\adapt {\sigma'}{\sigma}$. In   $\sigma$ the variable a points to an Account
with password pwd1, and balance 350;  the variable a1 points to an Account
with password pwd2, and balance 350; and the continuation is a1.transfer($..,..$); a=a1;
We reach $\sigma'$ by executing the first two statements from the continuation.
Thus,  ${\adapt {\sigma'}{\sigma}}\not\models \prg{a.balance==250}$.
Moreover, in $\adapt {\sigma'}{\sigma}$ we introduce the fresh variables y and y1, and replace a and
a1 by y and y1 in the continuation.
This gives that ${\adapt {\sigma'}{\sigma}} \models \calls {\_} {\prg{a1}} {\prg{transfer}} {...}$ and  ${\adapt {\sigma'}{\sigma}}\not\models \calls {\_} {\prg{a}} {\prg{transfer}} {...}$.

Definition <ref> describes the $\adapt{}{}$ operator in all detail
(it is equivalent to, but not identical to the definition  given in <cit.>).
We introduce fresh variables  $\overline{y}$ – as many as in the $\sigma'$ top frame variable map
– $dom(\beta')=\overline{x}$,  and $|\overline{y}| = |\overline{x}|$.
We extend $\sigma$'s variable map ($\beta$), so that it also maps $\overline{y}$
in the way that  $\sigma'$'s variable map ($\beta'$) maps its local variables – $\beta'' =  \beta[\overline{y} \mapsto  {\beta'(\overline{x})}]$. We rename $\overline{x}$   in $\sigma'$ continuation
to $\overline{y}$ –  $\kappa''=[\overline{y}/\overline{x}]\kappa'$.

For any states $\sigma$, $\sigma'$, heaps $\chi$, $\chi'$,
variable maps $\beta$, $\beta'$,
and continuations $\kappa$, $\kappa'$, such that
$\sigma$=$(\chi,(\beta,\kappa):\psi)$, and $\sigma$=$(\chi',(\beta',\kappa'):\psi')$, we define

$\strut \ \ \ \ \bullet$  $\adapt{\sigma'}{\sigma} \triangleq (\chi', (\beta'',\kappa'') : \psi')$

where there exist variables $\overline{y}$ such that   $\beta'' =  \beta[\overline{y} \mapsto  {\beta'(\overline{x})}]$,  and  $\kappa''=[\overline{y}/\overline{x}]\kappa'$, and

$dom(\beta')=\overline{x}$,  and $|\overline{y}| = |\overline{x}|$,  and  $\overline{y}$ are fresh in $\beta$ and $\beta'$.

Strictly speaking, $\adapt {}{}$  does not define one  unique state: Because  variables $\overline{y}$
are arbitrarily chosen,   $\adapt {}{}$ describes an infinite set of states. These states satisfy the same assertions
and therefore are   equivalent with each
This is why it is sound to  use $\adapt {}{}$  as an operator, rather than as a set.

§.§ Expressiveness

We discuss expressiveness of operators, by comparing
them with one another, with temporal operators, and with other examples from the literature.

Relationship between Necessity Operators
The three  operators
are related by generality.

Only If ($\onlyIf{A_1}{A_2}{A}$) implies
Single-Step Only If ($\onlyIfSingle{A_1}{A_2}{A}$), since if $A$ is
a necessary precondition for multiple steps, then it must be a necessary
precondition for a single step.
Only If also implies
an Only Through, where the intermediate state is the starting state
of the execution.  There is no further relationship between
Single-Step Only If and Only Through.

Relationship with Temporal Logic
Two of the three operators can be expressed in traditional
temporal logic:
can be expressed
$A_1\ \wedge\ \Diamond A_2\ \longrightarrow\ A$, and
can be expressed
as $\ A_1\ \wedge\ \bigcirc A_2\ \longrightarrow\ A$
(where $\Diamond$ denotes any future state,  and
$\bigcirc$ denotes the next state).
$\onlyThrough{A_1}{A_2}{A}$ cannot be encoded in temporal logics
without “nominals” (explicit state references), because the state where $A$
holds must be between the state where $A_1$ holds, and the state
where $A_2$ holds; and this must be so on every execution path
from $A_1$ to  $A_2$ <cit.>.
TLA+, for example, cannot describe “only through” conditions
<cit.>, but we have found “only through” conditions critical
to our proofs.

The DOM

This is the motivating example in <cit.>,
dealing with a tree of DOM nodes: Access to a DOM node
gives access to all its parent and children nodes, with the ability to
modify the node's property – where  parent, children and property
are fields in class Node. Since the top nodes of the tree
usually contain privileged information, while the lower nodes contain
less crucial third-party information, we must be able to limit
access given to third parties to only the lower part of the DOM tree. We do this through a Proxy class, which has a field node pointing to a Node, and a field height, which restricts the range of Nodes which may be modified through the use of the particular Proxy. Namely, when you hold a Proxy  you can modify the property of all the descendants of the    height-th ancestors of the node of that particular Proxy.  We say that
pr has modification-capabilities on nd, where pr is
a  Proxy and nd is a Node, if the pr.height-th  parent
of the node at pr.node is an ancestor of nd.

The specification DOMSpec states that the property of a node can only change if
some external object presently has
access to a node of the DOM tree, or to some Proxy with modification-capabilties
to the node that was modified.
[language = Chainmail, mathescape=true, frame=lines]
DOMSpec $\triangleq$ from nd : Node $\wedge$ nd.property = p  to nd.property != p
onlyIf $\exists$ o.[ $\external {\prg{o}}$ $\wedge$
$( \  \exists$ nd':Node.[ $\access{\prg{o}}{\prg{nd'}}$ ]  $\vee$
$\exists$ pr:Proxy,k:$\mathbb{N}$.[$\, \access{\prg{o}}{\prg{pr}}$ $\wedge$ nd.parent$^{\prg{k}}$=pr.node.parent$^{\prg{pr.height}}$ ] $\,$ ) $\,$ ]

More examples

In order to investigate 's expressiveness,
we used it for
examples provided in the literature.

In Appendix <ref>,
we compare with examples proposed by  FASE, and VerX.

§ PROVING NECESSITY

In this Section we provide a proof system for constructing
proofs of the specifications defined in <ref>.
As discussed in <ref>,
[]such proofs consist of
[]four parts:

(Part 1)
Proving Assertion Encapsulation (<ref>)

(Part 2)
Proving Per-Method specifications for a single internal method from the of that method (<ref>)

(Part 3)
Proving Per-Step specifications by combining [replaced per-call by per-method, as the prev sentence talks of per-method]per-method specifications (<ref>)

(Part 4)
Raising necessary conditions to construct proofs of properties of emergent behaviour (<ref>)

[replace concern by part, and reword]Part 1 is, to a certain extent, orthogonal to the main aims of our work;
in this paper we propose a simple approach based on the type system, while also acknowledging that
better solutions are possible.
For Parts 2-4, we  came up with the key ideas outlined in  <ref>, which we
develop in more detail in <ref>-<ref>.

§.§ Assertion Encapsulation

often leverage the fact that some assertions cannot be invalidated unless some
internal (and thus known)
computation took place.
We refer to this property as Assertion Encapsulation.

[reword, and banned model]In this work, we define the property $M\ \vDash A'\ \Rightarrow\ \encaps{A}$, which states that
under the conditions described by assertion $A'$, the assertion $A$ is encapsulated by module $M$.
We  do not mandate how this property should be derived – instead, we rely on a judgment
$M\ \vdash A'\ \Rightarrow\ \encaps{A}$ provided by some external system.
Thus, is parametric over the derivation of the encapsulation
judgment; in fact, several ways to do that are possible <cit.>. In Appendix <ref> and
Figure <ref>  we present a
rudimentary system that is sufficient to support our example

§.§.§ Assertion Encapsulation Semantics

[somebody wrote "WHY THE FUCK IS A' the subject and A the aux assertion", and they were right, so I swapped A and A']
[also, no "models the notion"]

[]As we said earlier,  an assertion $A$  is  encapsulated by a module $M$ under condition $A'$,
if in all possible states which arise from execution of module $M$ with any other external module $M'$, and which satisfy $A'$,
the validity of $A$
[shortened, but all is here] can only be changed via computations internal to that module – i.e.,  via a call to

a method from $M$.
In , that means by
calls to objects defined in $M$ but [removed: that are] accessible from the
[sophia asked if caller should be external, and if that is in coq - it is not in coq, but is implicit given the operational semantics of and the definition of Arising]

An assertion $A$ is encapsulated by module $M$ and assertion $A'$, written as   $M\ \vDash A'\ \Rightarrow\ \encaps{A}$,   if and only if
for all external modules $M'$, and all states $\sigma$, $\sigma'$
such that $\arising{M'}{M}{\sigma}$:

$\;\;\;\;$- $\reduction{M'}{M}{\sigma}{\sigma'}$      }34mm[$\;\;\;\Rightarrow\;\;\;$  $\exists x,\ m,\ \overline{z}. (\ \satisfiesA{M}{\sigma}{\calls{\_}{x}{m}{\overline{z}} \wedge\ \internal{x}}\ )$]

$\;\;\;\;$- $\satisfiesA{M}{\sigma}{A \wedge  A'}$

$\;\;\;\;$- $\satisfiesA{M}{\sigma' \triangleleft \sigma}{\neg A}$

Note that this definition   uses adaptation,
${\sigma' \triangleleft \sigma}$. The application of the adaptation operator is necessary
because we  interpret the assertion $A$ in the current state, $\sigma$, while we interpret the assertion $\neg A$ in
the future state, $\sigma' \triangleleft \sigma$.

Revisiting the examples from  <ref>,
both and encapsulate   the []equality of the balance of an account to some value bal:
[]This equality can only be invalidated through calling  methods on internal objects.

$\ModB\ \vDash \prg{a}:\prg{Account}\ \Rightarrow\ \encaps{\prg{a.balance}=\prg{bal}}$

$\ModC\ \vDash \prg{a}:\prg{Account}\ \Rightarrow\ \encaps{\prg{a.balance}=\prg{bal}}$

Moreover, the property that an object is only accessible from module-internal objects is encapsulated, that is, for all o, and all modules $M$:

$M\ \vDash \prg{o}:\prg{Object}\ \Rightarrow\ \encaps{\wrapped{\prg{o}}}$

This is so because any object which is only internally accessible can become
[]externally accessible only via an internal call.

In general,  code that does not contain
calls to a []given module is guaranteed not to invalidate any assertions encapsulated by that module.
Assertion encapsulation has been used in proof systems to address   the  frame problem

§.§.§ Deriving Assertion Encapsulation

Our logic does not deal with, nor rely on, the specifics of  how   encapsulation
is derived.

Instead, it relies on an encapsulation judgment and expects it to be sound:

A judgement of the form $\proves{M}{\givenA{A'}{\encaps{A}}}$  is  sound,  if
for all modules $M$, and assertions $A$ and $A'$, if

$\strut \hspace{1.5cm} \proves{M}{\givenA{A'}{\encaps{A}}}\ \ \ \ $ implies $\ \ \ \ \satisfies{M}{\givenA{A'}{\encaps{A}}}$.

[I'm not sure this paragraph should exist. It's key, but does it belong here or add anything?
I modified the paragraph on types]

Types for Assertion Encapsulation

[I have unified the two separate descriptions of the types system.]

Even though the derivation of assertion encapsulation  is not the focus of this paper,
for illustrative purposes, we will outline
now a  very simple type system which supports such derivations:
We assume that

field declarations, method arguments
and method results are annotated with class names, and that classes may
be annotated as . A  object
is not accessed by external objects; that is, it is always .

The type system then checks
that field assignments, method calls, and method returns adhere to these expectations,
and in particular, that objects of type
are never returned from method bodies
– this is a simplified version of the type system described in <cit.>.
Because the type system is so simple, we do not include its formalization in the paper.
Note however, that the type system has one further implication: modules are typed
in isolation, thereby implicitly prohibiting
method calls from internal objects to external objects.

Based on this type system, we define a predicate $\intrnl{e}$, in Appendix <ref>,
which asserts that any objects read during the evaluation of $e$ are internal.
Thus, any assertion that only involves $\intrnl{\_}$ expressions is encapsulated – more in Appendix <ref>.

§.§ Per-Method Specifications

In this section we detail how we use
to []prove per-method specifications

of the form

$$\onlyIfSingle{A_1\ \wedge\ x : C\ \wedge\ \calls{\_}{x}{m}{\overline{z}}}{A_2}{A}$$

where $C$ is a class, and $m$ a method in $C$.
[removed "Thus, $A$ is a necessary precondition for reaching $A_2$ from $A_1$ via a method call $m$ to an object of class $C$."
we should know that by now]

The first key idea in <ref>
is that if a precondition and a certain statement is sufficient
to achieve a particular result,
then the negation of that precondition
is necessary to achieve the negation of the result after executing that statement.
$\hoare{P}{s}{Q}$ implies that $\neg P$ is a necessary precondition for $\neg Q$ to
hold following the execution of $\prg{s}$.

For the use in , we define Classical assertions, a subset of , comprising only those
assertions that are commonly present in other specification languages.

[]They are restricted to expressions, class assertions, the usual connectives, negation,
implication, and the usual quantifiers.

Classical assertions, $P$, $Q$, are defined as follows

\begin{syntax}
\syntaxElement{P, Q} {} % {Classical Assertion}
\syntaxline
{e : C}
{P\ \wedge\ P}
{P\ \vee\ P}
{P\ \longrightarrow\ P}
{\neg P}
{\forall x.[P]}
{\exists x.[P]}
\endsyntaxline
\endSyntaxElement\\
\end{syntax}

We assume that there exists some
proof system  that derives
functional specifications of the form  $\proves{M}{\hoare{P}{\prg{s}}{Q}}$.
This implies that we can also have guarantees of

$$M\ \vdash\ \hoare{P}{\prg{res} = x.m(\overline{z})}{Q}$$

That is,

the execution of $x.m(\overline{z})$
with the precondition $P$ results in a program state that
satisfies postcondition $Q$, where the returned value is represented
by res in $Q$.
[]We further assume that such a proof system is sound, i.e. that
if $\proves{M}{\hoare{P}{\prg{res = x.m($\overline{z}$)}}{Q}}$, then
for every program state $\sigma$ that satisfies $P$, the execution of the method call x.m($\overline{z}$)
results in a program state satisfying $Q$.
As we have previously discussed (see <ref>), we build specifications
on top of using the fact that
validity of $\hoare{P}{\prg{res} = x.m(\overline{z})}{Q}$ implies that
$\neg P$ is a necessary pre-condition
to $\neg Q$ being true after execution of ${\prg{res} = x.m(\overline{z})}$.

Proof  rules for per-method specifications are given in
Figure <ref>. Note that the receiver $x$ in the rules
in <ref> is implicitly an internal object. This is because
we only have access to internal code, and thus are only able to prove the validity
of the associated Hoare triple.
[chopped: "If1-Classical and If1-Inside
raise to specifications.
These are rules whose conclusion have the form Single-Step Only If." as it breaks the flow]

Mx : C  ∧ P_1 ∧ P
res = x.m(z)

MP_1 ∧ x : C ∧ _xmz

Mx : C  ∧ P
res = x.m(z)
res ≠y

My ∧ x : C ∧ _xmzyP

Per-Method specifications

If1-Classical states that
if [dropped "by some classical logic" because usually classical logics are first order logics]  the execution of $x.m(\overline{z})$, with precondition $P \wedge \neg P_1$,

leads to a state satisfying postcondition $\neg P_2$, then $P_1$ is a necessary precondition to the
resulting state satisfying $P_2$.

[I removed the old bit that was here because I felt we had already explained this several times before.]

[]If1-Inside states that if  [simpliified] the precondition $\neg P$ guarantees that the result of
the call $x.m(\overline{z})$
is not $y$, then $P$ is a necessary pre-condition to invalidate $\wrapped{y}$ by calling
This is sound, [added details]because the premise of If1-Inside implies that  $P$ is
a necessary precondition for the call $x.m(\overline{z})$ to return an object $y$; this, in turn,
implies that    $P$ is a necessary precondition for the call $x.m(\overline{z}$) to
result in an external object gaining access to $y$.

The latter implication is valid because
[]the rule is applicable only to external states semantics, which means that
the call  $x.m(\overline{z})$ is a call from an external object to
some internal object $x$. Namely, there are only four ways
an object $o$ might gain access to another object $o'$:
[replaced $x$ and $y$ by $o$ and $o'$, because $x$ and $y$ are taken from earlier.]
(1) $o'$ is created by $o$ as the result of a new expression,
(2) $o'$ is written to some field of $o$,
(3) $o'$ is passed to $o$ as an argument to a method call on $o$,
or (4) $o'$ is returned to $o$ as the result of a method call from an object $o''$ that has access to $o'$.

The rule If1-Inside is only concerned with
effects on program state resulting from a method call to some internal object, and thus (1) and (2) need not be considered as
neither object creation or field writes may result in an external object gaining access [was from]to
[used to say "an internal object", but I think this is too weak]object that is only internally accessible.
Since we are only concerned with describing how internal objects grant access to external objects,
our restriction on external method calls within internal code prohibits (3) from occuring. Finally,
(4) is described by If1-Inside.
In further work we plan to weaken the restriction on external method calls, and will
strengthen this rule.
Note that If1-Inside  is essentially  a specialized version of If1-Classical
for the $\wrapped{\_}$ predicate. Since $\wrapped{\_}$ is not a classical
assertion, we cannot use to reason about necessary conditions
for invalidating $\wrapped{\_}$.

§.§ Per-Step Specifications

[for all  C ∈dom(M)  and   m ∈M(C).mths,

[MA_1 ∧ x : C ∧ _xmz

MA_1 ⟶ A_2

M ⊢ A_1A_2A_3

MA_1 ⟶A_1'

MA_2 ⟶A_2'

MA_3' ⟶A_3

MA_1A_2A ∨ A'

∀y,  M([y / x]A_1)A_2A

M∃x. [A_1]A_2A

Selected rules for Single-Step Only If

The second key idea in <ref> allows us to
[rephrase]leverage several per-method specifications
to obtain one per-step specification:

Namely, if an assertion is encapsulated, and all methods within the internal module
require the same condition to the invalidation of that assertion, then

this condition is a necessary, program-wide, single-step condition   to the invalidation of that assertion.
[replaced necessary pre-condition by necessary condition]

[] In this section we present a selection of the rules whose conclusion is of the form Single Step Only If in Fig. <ref>.
The full rule set can be found in Fig. <ref>.

lifts a set of per-method []specifications to a per-step specification.
Any specification which is satisfied for []all method
calls sent to any object in a module, is satisfied for any step, even
an external step, provided that the effect involved, going from $A_1$ states to
$A_2$ states, is encapsulated.

The remaining rules are more standard, and are reminiscent of the Hoare logic rule of consequence.
[]We present a few of the more interesting rules here:

The  rule for implication (If1-$\longrightarrow$) may strengthen
properties of either the starting or ending state, or
weaken the necessary precondition.

The disjunction
elimination rule (IF1-$\vee$E) mirrors typical disjunction elimination
rules, with a variation stating that if it is not possible  to reach
the end state from one branch of the disjunction, then we can eliminate
that branch.

Two rules support existential elimination on the left hand side.
If1-$\exists_1$ states that if any single step of execution starting
from a state satisfying $[y/x]A_1$ for all possible $y$, reaching some state satisfying
$A_2$ has $A$ as a necessary precondition, it follows that any single step execution
starting in a state where such a $y$ exists, and ending in a state satisfying $A_2$,
must have $A$ as a necessary precondition.  The other rule  can be found in Fig. <ref>.

Selected rules for Only Through – the rest can be found in Figure <ref>

Mx : C x : C

Selected rules for Only If – the rest can be found in Figure <ref>

§.§ Emergent Specifications

The third key idea in <ref>  allows us to
[rephrase]leverage several per-step specifications to
obtain  multiple-step specifications, and thus enables the description of the module's emergent behaviour.
combine   per-step specifications into
multiple-step specifications, as well as several  multiple step specifications into further multiple step specifications.

Figure <ref>  presents some of the rules with conclusion Only Through, while Figure <ref>
provides some of the rules with conclusion Only If.
The [I couldn't read Susan's comment on this]full rules can be found in Appendix <ref>.

Changes, in Figure <ref>,
states that
if   [re:susan's coment, is this a question of primes vs subscripts?]$A'$ is a necessary condition for the satisfaction of $A$ to change  in one step, then
it is also a  necessary condition for the satisfaction of $A$ to change  in any number of steps.
This is sound, because if  the satisfaction of some assertion changes over time, then
there must be some specific intermediate state where that change occurred.
Changes is an important
enabler for proofs of emergent properties:
[]Since specifications  are concerned with necessary conditions for change,
their proofs typically hinge around such necessary conditions for certain properties
to change. For example,
under what conditions may our account's balance decrease?

It []might seem natural []that Changes []had the more
general form:

(ChangesUnsound) is not sound because the conclusion  of the rule describes
transitions from a state satisfying $A_1$ to one satisfying $A_2$  which may occur occur over several steps,
while the premise describes a transition that takes place over one single step.
Such a concern does not apply to (Changes),  because
a change in satisfaction for a specific assertion ($A$ to $\neg A$) can only take place in a single step.

Trans$_1$ and Trans$_2$  are []rules about transitivity.
[]They state that necessary conditions to reach intermediate states or
proceed from intermediate states are themselves necessary intermediate states.
[moved]Any Only If specification entails the corresponding
Only Through specification (If).
[]Finally, End states that the ending condition is
a necessary intermediate condition.

Only If also includes a rule for transitivity (If-Trans), but
since the necessary condition must be true in the beginning state,
there is only a single rule. If-Class expresses that
an object's class never changes.
Finally, any starting condition is
itself a necessary precondition (If-Start).

§.§ Soundness of the Logic

Assuming a sound proof system, $\proves{M}{A}$, and
a sound encapsulation inference system, $\proves{M}{\givenA{A}{\encaps{A'}}}$,
and  that on top of these systems we built
the logic according to the rules in Figures <ref>,  <ref>,
<ref>,  and <ref>,   then, for    all modules $M$, and all specifications  $S$:

$$\proves{M}{S}\ \ \ \ \ \ \ \mbox{implies}\ \ \ \ \ \  \ \ \ \satisfies{M}{S}$$

by induction on the derivation of $\proves{M}{S}$.

Theorem. <ref> demonstrates
that the   logic is sound with respect to the semantics of specifications.
The logic parametric wrt to the algorithms for proving validity of assertions
$\proves{M}{A}$, and
assertion encapsulation ($\proves{M}{\givenA{A}{\encaps{A'}}}$), and is sound
provided that these two proof systems are sound.

The mechanized  proof of Theorem <ref> in Coq
can be found in the associated artifact <cit.>.
The   Coq formalism deviates slightly from the system as
presented here,  mostly in the formalization of the
language. The Coq version of restricts variable usage to expressions, and allows only addresses to
be used as part of non-expression syntax.
For example, in the Coq formalism
we can write assertions like $x.f==\prg{this}$ and
$x==\alpha_y$ and  $\access{\alpha_x}{\alpha_y}$, but we cannot write assertions
like $\access{x}{y}$, where $x$ and $y$ are variables, and $\alpha_x$ and $\alpha_y$ are
The reason for this restriction in the Coq formalism is to avoid spending
significant effort encoding variable
renaming and substitution, a well-known difficulty for languages such as Coq.

This restriction does not affect the expressiveness of
our  Coq formalism: we are
able to express assertions such as $\access{x}{y}$, by using addresses and introducing equality expressions
to connect variables to address, $\access{\alpha_x}{\alpha_y} \wedge \alpha_x == x \wedge \alpha_y == y$.
[]The Coq formalism makes use of the CpdtTactics <cit.>
library of tactics to discharge some proofs.

§ PROVING THAT SATISIFES

We now revisit our example from  <ref> and <ref>,
and outline a proof that satisfies .
A summary of this proof has already been discussed in <ref>.
A more complex variant of this example can be found in Appendix <ref>.
It demonstrates dealing with modules consisting of several classes some of which are confined, and
which use ghost fields
defined through functions; it also demonstrates proofs of assertion encapsulation of assertions
which involve reading the values of
several fields. Mechanised versions of the proofs in both this Section, and Appendix <ref>
can be found in the associated Coq artifact <cit.> in simple_bank_account.v and bank_account.v respectively.

[todo: add reference so simple_bank_account.v & bank_account.v]

Recall that an Account includes
at least a  field  (or ghost field)  called balance, and a method called transfer.

We first rephrase
to use the $\wrapped{\_}$ predicate.
[language=Chainmail, mathescape=true, frame=lines]
$\SrobustB$ $\triangleq$ from a:Account $\wedge$ a.balance=bal
to a.balance < bal onlyIf $\neg\wrapped{\prg{a.pwd}}$

We next revisit the   from <ref> and derive the following
PRE- and POST-conditions. The first two pairs of PRE-, POST-conditions correspond to the first two ENSURES
clauses from <ref>, while the next two pairs correspond to the MODIFIES-clause. The current expression in terms
of PRE- and POST-conditions is weaker than the one in <ref>, and is not modular, but is
sufficient for proving adherence to  .

[mathescape=true, frame=lines, language=Chainmail]
$\SclassicP$  $\triangleq$
method transfer(dest:Account, pwd':Password) -> void
(PRE: this.balance$=$bal1 $\wedge$ dest.balance$=$bal2 $\wedge$ this.pwd$=$pwd' $\wedge$ this$\neq$dest
POST: this.balance=bal1-100 $\wedge$ dest.balance=bal2+100)
(PRE: this.balance$=$bal1 $\wedge$ dest.balance$=$bal2 $\wedge$ (this.pwd$\neq$pwd' $\vee$ this$=$dest)
POST: this.balance=bal1 $\wedge$ dest.balance=bal2)
(PRE: a:Account $\wedge$ a.balance$=$bal $\wedge$ a$\neq$this $\wedge$ a$\neq$dest
POST: a.balance=bal)
(PRE: a:Account $\wedge$ a.pwd$=$pwd1
POST: a.pwd=pwd1)

§.§ Part 1: Assertion Encapsulation

The first part of the proof demonstrates that the balance, pwd, and external accessibility to the password are
encapsulated properties. That is, for the balance to change (i.e. for a.balance = bal to be invalidated),
or for the encapsulation of a.pwd to be broken (ie for a transition from ${\wrapped{\prg{a,pwd}}}$ to $\neg {\wrapped{\prg{a.pwd}}}$),
internal computation is required.

We use [used to say "a conservative approach to an encapsulation system" but "conservative" here means sound]a simple encapsulation system, detailed in []Appendix <ref>,
and provide the proof steps below.
aEnc and balanceEnc state that
[]a and a.balance satisfy the Enc$_e$ predicate. That is, if any objects' contents are to be
looked up during execution of these expressions, then these objects are internal.
Enc$_e$(a) holds because no object's contents is looked up,
while Enc$_e$(a.balance) holds because balance is a field of a, and a is

$\proves{\ModC}{\givenA{\prg{a:Account $\wedge$ a.balance=bal}}{\intrnl{\prg{a}}}}$
by Enc$_e$-Obj

$\proves{\ModC}{\givenA{\prg{a:Account $\wedge$ a.balance=bal}}{\intrnl{\prg{a.balance}}}}$
by aEnc and Enc-Field

$\proves{\ModC}{\givenA{\prg{a:Account $\wedge$ a.balance=bal}}{\intrnl{\prg{bal}}}}$
by Enc$_e$-Int

$\proves{\ModC}{\givenA{\prg{a:Account $\wedge$ a.balance=bal}}{\encaps{\prg{a.balance=bal}}}}$
by balanceEnc, balEnc, Enc-Eq, and Enc-=

Moreover,  balEnc states that bal satisfies the Enc$_e$ predicate
– it is an integer, and no object look-up is involved in its calculation.

balanceEnc and balEnc combine to prove that the assertion a.balance = bal is encapsulated –

only internal object lookups are involved in the validity of that assertion, and therefore only
internal computation may cause it to be invalidated.

Using similar reasoning, we prove that a.pwd is encapsulated (PwdEncaps), and
that a.pwd is encapsulated (PwdInsideEncaps).
[I chopped the below "That is, if only internal objects have access
to an account's pwd, then only internal computation may grant  access to pwd
to an external object." as it only repeats the definition.]

by Enc$_e$-Obj, Enc-Field, and Enc-Eq

by Enc-Inside

[removing references to Hoare logic.]

§.§ Part 2: Per-Method Specifications

Part 2 proves necessary preconditions for each method in
the module interface.

We employ the rules from  <ref> which describe how to derive
necessary preconditions from .

SetBalChange uses a
and a rule of consequence

to prove that the set method in Account
never modifies the balance. We then use If1-Classical
and our logic to prove that if it ever did change (a logical absurdity),
then transfer must have been called.

a, a$^\prime$:Account $\wedge$ a$^\prime$.balance=bal
a.set(_, _)
a$^\prime$.balance = bal

a, a$^\prime$:Account $\wedge$ a$^\prime$.balance = bal $\wedge$ $\neg$ false
a.set(_, _)
$\neg$ a$^\prime$.balance < bal

rule of consequence

a, a$^\prime$:Account $\wedge$ a$^\prime$.balance=bal $\wedge$ $\calls{\_}{\prg{a}}{\prg{set}}{\prg{\_, \_}}$
a$^\prime$.balance < bal

by If1-Classical

a, a$^\prime$:Account $\wedge$ a$^\prime$.balance=bal $\wedge$ $\calls{\_}{\prg{a}}{\prg{set}}{\prg{\_, \_}}$
a$^\prime$.balance < bal
$\calls{\_}{\prg{a}^\prime}{\prg{transfer}}{\prg{\_, a$^\prime$.pwd}}$

by Absurd and If1-$\longrightarrow$

Similarly, in SetPwdLeak  we employ
to prove that a method does not leak access to some data (in this case the pwd).
Using If1-Inside, we reason that since the return value of set is
void, and set is prohibited from making external method calls,
no call to set can result in an object (external or otherwise) gaining access to the pwd.

a:Account $\wedge$ a$^\prime$:Account $\wedge$ a.pwd == p
res=a$^\prime$.set(_, _)
res != pwd

a:Account $\wedge$ a$^\prime$:Account $\wedge$ a.pwd == p $\wedge$ $\neg$ false
res=a$^\prime$.set(_, _)
res != p

by rule of consequence

$\wrapped{\prg{pwd}}$ $\wedge$ a, a$^\prime$:Account $\wedge$ a.pwd=p $\wedge$ $\calls{\_}{\prg{a}^\prime}{\prg{set}}{\_, \_}$
$\neg \wrapped{\_}$

by If1-Inside

In the same manner as SetBalChange and SetPwdLeak, we also prove
SetPwdChange, TransferBalChange, TransferPwdLeak, and TransferPwdChange. We provide their
statements, but omit their proofs.

a, a$^\prime$:Account $\wedge$ a$^\prime$.pwd=p $\wedge$ $\calls{\_}{\prg{a}}{\prg{set}}{\prg{\_, \_}}$
$\neg$ a.pwd = p
$\calls{\_}{\prg{a}^\prime}{\prg{set}}{\prg{a$^\prime$.pwd, \_}}$

by If1-Classical

a, a$^\prime$:Account $\wedge$ a$^\prime$.balance=bal $\wedge$ $\calls{\_}{\prg{a}}{\prg{transfer}}{\prg{\_, \_}}$
a$^\prime$.balance < bal
$\calls{\_}{\prg{a}^\prime}{\prg{transfer}}{\prg{\_, a$^\prime$.pwd}}$

by If1-Classical

$\wrapped{\prg{pwd}}$ $\wedge$ a, a$^\prime$:Account $\wedge$ a.pwd=p $\wedge$ $\calls{\_}{\prg{a}^\prime}{\prg{transfer}}{\_, \_}$
$\neg \wrapped{\_}$

by If1-Inside

a, a$^\prime$:Account $\wedge$ a$^\prime$.pwd=p $\wedge$ $\calls{\_}{\prg{a}}{\prg{transfer}}{\prg{\_, \_}}$
$\neg$ a.pwd = p
$\calls{\_}{\prg{a}^\prime}{\prg{set}}{\prg{a$^\prime$.pwd, \_}}$

by If1-Classical

§.§ Part 3: Per-Step Specifications

Part 3 builds upon the proofs of Parts 1 and 2 to
construct proofs of necessary preconditions, not for single method execution,
but for any single execution step. That is, a proof that for
any single step in program execution, [removed "potentially dangerous", since such proof
steps apply whether the changes are potentially dangerous or not] changes
in program state require specific preconditions.

a:Account $\wedge$ a.balance=bal
a.balance < bal
$\calls{\_}{\prg{a}}{\prg{transfer}}{\prg{\_, a.pwd}}$

by BalEncaps, SetBalChange, TransferBalChange, and If1-Internal

a:Account $\wedge$ a.pwd=p
$\neg$ (a.pwd = p)
$\calls{\_}{\prg{a}}{\prg{set}}{\prg{a.pwd, \_}}$

by PwdEncaps, SetPwdChange, TransferPwdChange, and If1-Internal

a:Account $\wedge$ a.pwd=p $\wedge$ $\wrapped{\prg{p}}$
$\neg$ $\wrapped{\prg{p}}$

by PwdInsideEncaps, SetPwdLeak, TransferPwdLeak, and If1-Internal

§.§ Part 4: Emergent Specifications

Part 4 raises necessary preconditions for single execution steps proven in Part 3 to
the level of an arbitrary number of execution steps in order to prove specifications of emergent behaviour.
The proof of takes the following form:

If the balance of an account decreases, then
by BalanceChange there must have been a call
to transfer in []Account with the correct password.

If there was a call where the Account's password
was used, then there must have been an intermediate program state
when some external object had access to the password.

Either that password was the same password as in the starting
program state, or it was different:

(Case A)
If it is the same as the initial password, then since by PasswordLeak
it is impossible to leak the password, it follows that some external object
must have had access to the password initially.

(Case B)
If the password is different from the initial password,
then there must have been an intermediate program state when it
changed. By PasswordChange we know that this must have occurred
by a call to set with the correct password. Thus,
there must be a some intermediate program state where the initial
password is known. From here we proceed by the same reasoning
as (Case A).

a:Account $\wedge$ a.balance=bal
a.balance < bal
$\calls{\_}{\prg{a}}{\prg{transfer}}{\_, \prg{a.pwd}}$

by Changes and BalanceChange
a:Account $\wedge$ a.balance=bal
b.balance(a) < bal

by $\longrightarrow$, Caller-Ext, and Calls-Args

a:Account $\wedge$ a.balance=bal $\wedge$ a.pwd=p
a.balance < bal
$\neg$$\wrapped{\prg{a.pwd}}$ $\wedge$ (a.pwd=p $\vee$ a.pwd != p)

by $\longrightarrow$ and Excluded Middle
a:Account $\wedge$ a.balance=bal $\wedge$ a.pwd=p
a.balance < bal
($\neg$$\wrapped{\prg{a.pwd}}$ $\wedge$ a.pwd=p) $\vee$

($\neg$$\wrapped{\prg{a.pwd}}$ $\wedge$ a.pwd != p)

by $\longrightarrow$
a:Account $\wedge$ a.balance=bal $\wedge$ a.pwd=p
a.balance < bal
$\neg$$\wrapped{\prg{p}}$ $\vee$
a.pwd != p

by $\longrightarrow$

Case A ($\neg\wrapped{\prg{p}}$)
a:Account $\wedge$ a.balance=bal $\wedge$ a.pwd=p
$\wrapped{\prg{p}}\ \vee \neg\wrapped{\prg{p}}$

by If-$\longrightarrow$ and Excluded Middle
a:Account $\wedge$ b:Bank $\wedge$ b.balance(a)=bal $\wedge$ a.password=pwd

by $\vee$E and PasswordLeak

Case B (a.pwd != p)
a:Account $\wedge$ b:Bank $\wedge$ b.balance(a)=bal $\wedge$ a.password=pwd
a.pwd != p
$\calls{\_}{\prg{a}}{\prg{set}}{\prg{p}, \_}$

by Changes and PasswordChange
a:Account $\wedge$ a.balance=bal $\wedge$ a.pwd=p
a.pwd != p

by $\vee$E and PasswordLeak
a:Account $\wedge$ a.balance=bal $\wedge$ a.pwd=p
a.pwd != p

by Case A and Trans

a:Account $\wedge$ a.balance=bal $\wedge$ a.pwd=p
b.balance(a) < bal

by Case A, Case B, If-$\vee$I$_2$, and If-$\longrightarrow$

§ RELATED WORK

Program specification and verification has a long and proud history
These verification techniques assume a closed system, where modules can be trusted
to coöperate —  Design by Contract <cit.> explicitly
rejects “defensive programming”  with an “absolute rule”
that calling a method in violation of its precondition is always a

Open systems, by definition, must interact with
untrusted code: they cannot rely on callers' obeying method
<cit.> define 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.”

<cit.> made the first attempt to formalise defensive consistency and
correctness in a programming language context.  Murray's model was rooted in
counterfactual causation <cit.>: 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

without a specification language for describing effects.

The security community has developed a similar notion of “robust safety” that
originated in type systems for process calculi, ensuring protocols
behave correctly in the presence of “an arbitrary hostile opponent”

More recent work has applied robust safety in the context of
programing languages.  For example,
<cit.> present a logic
for object capability patterns, drawing

on verification techniques for security and
information flow. They prove a robust safety property that
ensures interface objects ("low values") are safe to share with untrusted code,
in the sense that untrusted code cannot use them to break any internal invariants of the encapsulated object.

Similarly, <cit.> have

added  support for information-flow security
using refinement to ensure correctness (in this case confidentiality) by
Concerns like are not, we argue, within the scope of these works.

<cit.>  have deployed
theoretical techniques to address similar problems to .
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.
They have demonstrated solutions to a range of exemplar problems,
including the DOM wrapper (replicated in
<ref>) and a mashup application.

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.
They use powerful mathematical techniques

which  the users need  to understand in order to write their specifications,
while users only need  to understand [as Alex pointed out]small extensions to first order logic.

Finally, none of these systems offer the kinds of
necessity assertions addressing control flow, provenance, and permission
that are at the core of 's approach.

By enforcing encapsulation,
all these approaches are reminiscent of techniques such as
ownership types <cit.>,
which also can
protect internal implementation objects behind
encapsulation boundaries.  <cit.> demonstrated that by
ensuring confinement, ownership
systems can enforce representation independence.
relies on an implicit form of ownership types <cit.>,
where inside objects are encapsulated behind a boundary
consisting of all the internal objects that are accessible outside their
defining module <cit.>.
's definition of
— all references to $o$ are from objects $x$
that are within $M$ (here internal to $M$):
$\all{x}{\access{x}{o}\ \Rightarrow\ \internal{x}}$
with the containment invariant
from simpleOwnership —
all references to $o$ are from objects $x$
whose representation is within ($\prec:$) $o$'s owner:
($\all{x}{\access{x}{o}\ \Rightarrow\ \texttt{rep}(x) \prec:
\texttt{owner}(o)  }$).

In early work,
sketched a  specification language to
specify six correctness policies from <cit.>.

They also
sketched how
a trust-sensitive
example (escrow) could be verified in an open world
<cit.>. More recently,
<cit.> presents the Chainmail language for
“holistic specifications” in open world systems.
Like , Chainmail is able to express specifications of
permission, provenance, and control; Chainmail
also includes spatial assertions and a richer set of temporal
operators, but no proof system.
's restrictions mean
we can provide the proof system that Chainmail lacks.

The recent VerX tool is able to verify a range of
specifications for Solidity contracts automatically <cit.>.

VerX includes  temporal operators, predicates that
model the current invocation on a contract (similar to 's
“calls”), access to variables,

but has no analogues to 's permission or provenance assertions.

Unlike , VerX includes a practical tool that has
been used to verify a hundred properties across case studies of
twelve Solidity contracts. Also unlike , VerX's own correctness
has not been formalised or mechanistically proved.

Like , VerX <cit.> and  Chainmail <cit.> also work on problem-specific guarantees.
Both  approaches can express necessary conditions
like using
temporal logic operators and implication. For example,  could be  written:

$\strut ~  ~ \hspace{.25in} \strut  \prg{a:Account} \ \wedge\ \prg{a.balance==bal}  \ \wedge\
\langle {\color{blue}\texttt{next}}\, \prg{a.balance<bal} \, \rangle $

$\strut ~ \hspace{2.1in} \strut \strut \strut \longrightarrow\   \exists \prg{o},\prg{a'}. \calls{\prg{o}}{\prg{a}}{\prg{transfer}}{\prg{a',a.password}} $

However, to express , one also needs   capability operators which talk about
provenance   and
VerX  does not support capability operators, and thus cannot express   ,
while  Chainmail does support capability operators, and can express  .

Moreover, temporal operators in VerX   and  Chainmail  are first class, may appear in any assertions
and form new assertions. This makes VerX   and  Chainmail very expressive,
and allows specifications which talk about any number of points in time.
However, this expressivity comes at the cost of making it very difficult to develop a logic to
prove adherence to such specifications.

developed Incorrectness logics to reason about the presence of bugs,
based on a Reverse Hoare Logic <cit.>.
Classical Hoare triples $\{ P \}\, C\, \{ Q \}$ express  that starting
at states satisfying $P$ and executing   $C$  is sufficient to reach only states
that satisfy $ Q $ (soundness), while
incorrectness triples $[ P_i ]\, C_i\, [ Q _i ]$ express  that starting at
states satisfying $P_i$ and executing  $C_i$ is sufficient to reach
all states that satisfy $Q_i$ and possibly some more (completeness).

From our perspective, classical Hoare logics and Incorrectness logics
are both about sufficiency, whereas here we are concerned with .

In practical open systems, especially web browsers, defensive
consistency / robust safety is typically supported by sandboxing: dynamically separating
trusted and untrusted code, rather than relying on static verification
and proof.
Google's Caja <cit.>, for example, uses proxies and wrappers to
sandbox web pages.
Sandboxing has been validated
formally:  <cit.> develop a model of
JavaScript and show it prevents trusted dependencies on untrusted code.

<cit.> use dynamic monitoring from function contracts to
control objects flowing around programs;
<cit.> extends this to use fluid
environments to bind callers to contracts.

<cit.> develop $\lambda_{sandbox}$, a low-level language with
built in sandboxing, separating trusted and
untrusted memory. $\lambda_{sandbox}$ features a type system,
and  show that sandboxing achieves robust safety.

address a somewhat different
problem domain than does, low-level systems programming where
there is a possibility of forging references to locations in memory. Such a domain
would subvert ,
in particular a reference to $x$ could always be guessed

thus the assertion $\wrapped{x}$ would no longer be encapsulated.

Necessity does not –yet– support calls of external methods from within internal modules.
While this is a limitation, it is common in the related literature.
For example, VerX <cit.> work on effectively call-back free contracts,
while <cit.> and  <cit.>  drastically restrict  the effect of a callback on a contract.
In further work we are planning to incorporate callbacks by
splitting internal methods at the point where a call to an external method appears.
This would be an adaptation of 's approach,
who  split methods into the
call-free subparts, and use the transitive closure of the effects of all functions from a module
to overapproximate the effect of an external call.

One  useful simplification was proposed by
Permenev: in
“effectively callback free” methods, meaning that we could
include callbacks while also only requiring at most one functional specification

§ CONCLUSION

This paper presents
, a specification language for a program's
emergent behaviour.
constrain when effects can happen in some future state
(“ ”),
in the immediately following state (“”), or
on an execution path

We have developed a proof system to prove that modules meet their specifications.  Our proof system exploits the
pre and
postconditions of to infer per method specifications,
generalises those to cover any single execution step,
and then combines them to capture a program's emergent behaviour.

We have proved our system sound, and used it to
prove a bank account example correct: the Coq mechanisation is
detailed in the appendices and available as an artifact.

In future work we want to consider more than one external module – c.f. <ref>,
and expand a Hoare logic so as to make use of
specifications, and reason about calls into unknown code
- c.f. <ref>.

We want to work on supporting callbacks.

We want to develop a logic for encapsulation rather than rely on a type system.
Finally we want to develop logics about reasoning about risk and trust <cit.>.

We are especially grateful for the careful attention and
judicious suggestions of the anonymous reviewers, which have
significantly improved the paper.
We are deeply grateful for feedback from and discussions with
Chris Hawblitzel,  Dominiqie Devriese, Derek Dreyer,  Mark Harman,
Lindsay  Groves, Michael Jackson, Bart Jacobs from KU Leuven, Gary Leavens, Mark Miller, Peter Mueller, Toby Murray, Matthew Ross
Rachar,  Alexander J. Summers, and members of the WG2.3.
This work is supported in part by the
MarsdenFundRoyal Society of New Zealand (Te
Apārangi) Marsden Fund (Te Pūtea Rangahau a
under grant [https://www.royalsociety.org.nz/what-we-do/funds-and-opportunities/marsden/awarded-grants/marsden-fund-highlights/2018-marsden-fund-highlights/an-immune-system-for-software]Marsden FundVUW1815, and
by gifts from the Ethereum Foundation,
Meta, and Agoric.

We introduce , a simple, typed, class-based, object-oriented language that underlies the specifications
introduced in this paper. includes ghost fields, recursive definitions that may only be
used in the specification language.

To reduce the complexity of our formal models, lacks many
common languages features, omitting static fields and methods, interfaces,
inheritance, subsumption, exceptions, and control flow.  These features are
well-understood: their presence (or absence) would not chanage the
results we claim nor the structures of the proofs of those results.
Similarly, while Loo is typed, we don't present or mechanise
its type system.
Our results and proofs rely only upon type
soundness — in fact, we only need that an expression of
type $T$ (where $T$ is a class $C$ declared in module $M$)
will evaluate to an instance of some class from $M$,
with the same confinement status as $C$.
Featherweight Java extended with modules and assignment
will more than suffice <cit.>.

§.§ Syntax

The syntax of is given in Fig. <ref>.
modules ($M$) map class names ($C$) to class definitions ($\textit{ClassDef}$).
A class definition consists of []an optional annotation ,
a list of field definitions, ghost field definitions, and method definitions.
[]Fields, ghost fields, and methods all have types: types are
classes. Ghost fields may be optionally
annotated as , requiring the argument to have an internal type, and the
body of the ghost field to only contain references to internal objects. This is enforced by the
limited type system of .
A program state ($\sigma$) is represented as a heap ($\chi$), stack ($\psi$) pair,
where a heap is a map from addresses ($\alpha$) to objects ($o$), and a stack is a non-empty list of frames ($\phi$). A frame consists of a local variable
map and a continuation ($c$) that represents the statements that are yet to be executed ($s$),
or a hole waiting to be filled by a method return in the frame above ($x := \bullet; s$).
A statement is either a field read ($x := y.f$), a field write ($x.f := y$), a method call
($x := y.m(\overline{z})$), a constructor call ($\prg{new}\ C(\overline{x})$), a method return statement
($\prg{return}\ x$), or a sequence of statements ($s;\ s$).

also includes syntax for expressions $e$ that may
be used in writing
specifications or the definition of ghost fields.

\[
\begin{syntax}
\syntaxID{x, y, z}{Variable}
\syntaxID{C, D}{Class Id.}
\syntaxElement{T}{Type}
\syntaxline
%				{\_}
\endsyntaxline
\endSyntaxElement\\
\syntaxID{f}{Field Id.}
\syntaxID{g}{Ghost Field Id.}
\syntaxID{m}{Method Id.}
\syntaxID{\alpha}{Address Id.}
\syntaxInSet{i}{\IntSet}{Integer}
\syntaxElement{v}{Value}
\syntaxline
\endsyntaxline
\endSyntaxElement\\
\syntaxElement{e}{Expression}
\syntaxline
{e + e}
{e = e}
{e < e}
\endsyntaxline
\syntaxline
{\prg{if}\ e\ \prg{then}\ e\ \prg{else}\ e}
\endsyntaxline
\endSyntaxElement\\
\syntaxElement{o}{Object}
{\{\prg{class}:=C;\ \prg{flds}:=\overline{f \mapsto v} \}}
\endSyntaxElement\\
\syntaxElement{s}{Statement}
\syntaxline
\endsyntaxline
\syntaxline
{s;\ s}
\endsyntaxline
\endSyntaxElement\\
\syntaxElement{c}{Continuation}
\syntaxline
{x:=\bullet; s}
\endsyntaxline
\endSyntaxElement\\
\syntaxElement{\chi}{Heap}
{\overline{\alpha \mapsto o}}
\endSyntaxElement\\
\syntaxElement{\phi}{Frame}
{\{\prg{local}:=\overline{x\mapsto v};\ \prg{contn}:=c\}}
\endSyntaxElement\\
\syntaxElement{\psi}{Stack}
{\syntaxline{\phi}{\phi : \psi}\endsyntaxline}
\endSyntaxElement\\
\syntaxElement{\sigma}{Program Config.}
\endSyntaxElement\\
\syntaxElement{mth}{Method Def.}
\prg{method}\ m\ (\overline{x : T})\{\ s\ \}
\endSyntaxElement\\
\syntaxElement{fld}{Field Def.}
{\prg{field}\ f\ :\ T}
\endsyntaxline}
\endSyntaxElement\\
\syntaxElement{gfld}{Ghost Field Def.}
{\prg{ghost}\ g\ (x : T)\{\ e\ \} : T}
{\prg{ghost}\ \prg{intrnl}\ g\ (x : T)\{\ e\ \} : T}
\endsyntaxline}
\endSyntaxElement\\
\syntaxElement{An}{Class Annotation}
\endSyntaxElement\\
\syntaxElement{CDef}{Class Def.}
[An]\ \prg{class}\ C\ \{\ \prg{constr}:= (\overline{x : T})\{s\};\ \prg{flds}:=\overline{fld};\ \prg{gflds}:=\overline{gfld};\ \prg{mths}:=\overline{mth}\ \}
\endSyntaxElement\\
\syntaxElement{Mdl}{Module Def.}
\syntaxline{\overline{C\ \mapsto\ ClassDef}}\endsyntaxline
\endSyntaxElement\\
\end{syntax}
\]

§.§ Semantics

is a simple object oriented language, and the operational semantics
(given in Fig. <ref> and discussed later)
do not introduce any novel or surprising features. The operational
semantics make use of several helper definitions that we
define here.

We provide a definition of reference interpretation in Definition <ref>

For a program state $\sigma = (\chi, \phi : \psi)$, we provide the following function definitions:

* $\interpret{\sigma}{x}\ \triangleq\ \phi.(\prg{local})(x)$

* $\interpret{\sigma}{\alpha.f}\ \triangleq\ \chi(\alpha).(\prg{flds})(f)$

* $\interpret{\sigma}{x.f}\ \triangleq\ \interpret{\sigma}{\alpha.f}$ where $\interpret{\sigma}{x}=\alpha$

That is, a variable $x$, or a field access on a variable $x.f$
has an interpretation within a program state of value $v$
if $x$ maps to $v$ in the local variable map, or the field
$f$ of the object identified by $x$ points to $v$.

Definition <ref> defines the class lookup function an object
identified by variable $x$.

For program state $\sigma = (\chi, \phi : \psi)$, class lookup is defined as

$$\class{\sigma}{x}\ \triangleq\ \chi(\interpret{\sigma}{x}).(\prg{class})$$

Definition <ref> defines the method lookup function for a method
call $m$ on an object of class $C$.

For module $M$, class $C$, and method name $m$, method lookup is defined as

$$\meth{M}{C}{m}\ \triangleq\ M(C).\prg{mths}(m)$$

Fig. <ref> gives the operational semantics of .
Program state $\sigma_1$ reduces to $\sigma_2$ in the context of
module $M$ if $\exec{M}{\sigma_1}{\sigma_2}$. The semantics in Fig. <ref>
are unsurprising, but it is notable that reads (Read) and writes (Write)
are restricted to the class that the field belongs to.

σ_1 = (χ, ϕ_1 : ψ)

σ_2 = (χ, ϕ_2 : ϕ_1' : ψ)

ϕ_1.(contn) = (x := y.m(z); s)

ϕ_1' = ϕ_1[contn := (x := ∙; s)]

Mσ_1xm = m(p : T){body}

ϕ_2 = {local:= ([this ↦ σ_1x][p_i ↦ σ_1z_i]), contn:=body}

σ_1 = (χ, ϕ_1 : ψ)

σ_2 = (χ, ϕ_2 : ψ)

ϕ_1.(contn) = (x := y.f; s)

σ_1x.f = v

ϕ_2 = {local:=ϕ_1.(local)[x ↦ v], contn:=s}

σ_1this = σ_1y

σ_1 = (χ_1, ϕ_1 : ψ)

σ_2 = (χ_2, ϕ_2 : ψ)

ϕ_1.(contn) = (x.f := y; s)

σ_1y = v

ϕ_2 = {local:=ϕ_1.(local), contn:=s}

χ_2 = χ_1[σ_1x.f ↦ v]

σ_1this = σ_2x

σ_1 = (χ, ϕ: ψ)

ϕ.(contn) = (x := new C(z); s)

M(C).(constr) = (p : T){ s' }

ϕ' = {local:=[this ↦α],[p_i ↦⌊z_i ⌋_σ_1], contn := s'}

σ_2 = (χ[α ↦ {class:=C, flds:=f ↦ ], ϕ' : ϕ[contn := (x := ∙; s)] : ψ)

σ_1 = (χ, ϕ_1 : ϕ_2 : ψ)

ϕ_1.(contn) = (return x; s) or ϕ_1.(contn) = (return x)

ϕ_2.(contn) = (y := ∙; s)

σ_2 = (χ, ϕ_2[y ↦ σ_1x] : ψ)

operational Semantics

i_1 + i_2 = i

Mσe_1 + e_2i

Mσe_1 = e_2

v_1 ≠ v_2

Mσe_1 = e_2

ghost g(x : T){e} : T' ∈ M(σα).(gflds)

expression evaluation

While the small-step operational semantics of is given in Fig. <ref>,
specification satisfaction is defined over an abstracted notion of
the operational semantics that models the open world, called []external states semantics.
That is, execution occurs in the context of not just an internal, trusted module, but
an external, untrusted module. We borrow the definition of external []states semantics
from , along with the related definition of module linking, given in Definition <ref>.

For all modules $M$ and $M'$, if the domains of $M$ and $M'$ are disjoint,
we define the module linking function as $M\ \circ\ M'\ \triangleq\ M\ \cup\ M'$.

That is, given an internal, module $M$, and an external module $M'$,
we take their linking as the union of the two if their domains are disjoint.

An Initial program state contains a single frame
with a single local variable this pointing to a single object
in the heap of class Object, and a continuation.

A program state $\sigma$ is said to be an initial state ($\initial{\sigma}$)
if and only if

* $\sigma.\prg{heap} = [\alpha\ \mapsto\ \{\prg{class}:=\prg{Object};\ \prg{flds}:=\emptyset\}]$ and

* $\sigma.\prg{stack} = \{\prg{local}:=[\prg{this}\ \mapsto\ \alpha];\ \prg{contn}:= s\}$

for some address $\alpha$ and some statement $s$.

Finally, we provide a semantics for expression evaluation is given in Fig. <ref>.
That is, given a module $M$ and a program state $\sigma$, expression $e$ evaluates to $v$
if $\eval{M}{\sigma}{e}{v}$. Note, the evaluation of expressions is separate from the operational
semantics of , and thus there is no restriction on field access.

§ ENCAPSULATION

Assertion encapsulation (Definition <ref>) is
critical to our approach.  Assertion encapsulation ensures that a
change in satisfaction of an assertion can only depend on computation
internal to the module in which the assertion is encapsulated
— this is related to the footprint of an
assertion <cit.>.
If the footprint of an assertion is contained
within a module, then that assertion is encapsulated,
however there are assertions that are encapsulated by a module
whose footprint is not contained within the module.
Specifically, the assertion $\inside{x}$ is not
contained within an module $M$ since its due to the
universal quantification contained withing
$\inside{x}$, the footprint consists of portions
of the heap that are external to $M$. $\inside{x}$ is
encapsulated by $M$ since if only objects that derive
from $M$ have access to $x$, it follows that a method call
on $M$ is required to gain access to $x$.
Necessity Logic itself does not depend on the details
of the encapsulation scheme — only that we can determine
whether an assertion is encapsulated within a particular
part of the program.  For reasons of simplicity,
we have adopted an encapsulation model for based on
's Confined Types []
(and we rely on their proof).

Confined types partition the objects accessible to code within a
module, based on those objects' defining classes and modules:

* instances of non-classes
constitute their defining module's encapsulation
boundary <cit.>,
and may be accessed anywhere.

* instances of classes
are encapsulated their defining module.

* instances of classes defined in other modules
are not accessible elsewhere

* instances of non-classes defined in other
modules are visible, however methods may only be invoked on such
objects when the confinement system guarantees the particular instance
is only accessible this module.

's Confined Types rely on three syntactic restrictions
to enforce this encapsulation model:

* class declarations must be annotated.

* objects may not be returned by methods of non-classes.

* Ghost fields
may be annotated as intrnl; if so, they must only refer to objects their defining module — i.e. either defined directly in that module, or
instances of non-classes defined in other modules
where those particular instances are only ever accessed within the
defining module.

[Yes, I think that's right. I'm not 100% sure that assertion
encapsulation is defined by the footprint, unless I misunderstand
footprint. It is possible for an assertion to be encapsulated,
but depend on external objects. For example $\neg\access{x}{y}$:
if $\inside{y}$ is true, then $\neg\access{x}{y}$ is encapsulated,
even if $x$ is external.]

We define internally evaluated expressions ($\intrnl{\_}$)
whose evaluation only inspects internal objects or primitvies (i.e. integers or booleans).
For all modules $M$, assertions $A$, and expressions $e$,
$\satisfies{M}{\givenA{A}{\intrnl{e}}}$ if and only if for all heaps $\chi$, stacks $\psi$, and frames $\phi$
such that $\satisfiesA{M}{(\chi, \phi : \psi)}{A}$, we have for all values $v$, such that $\eval{M}{(\chi, \phi : \psi)}{e}{v}$
then $\eval{M}{(\chi', \phi' : \psi)}{e}{v}$, where

* $\chi'$ is the internal portion of $\chi$, i.e.

$\chi' = \{\alpha \mapsto o| \alpha \mapsto o \in \chi\ \wedge \ o.(\prg{cname}) \in M \}$ and

* $\phi'.(\prg{local})$ is the internal portion of the $\phi.(\prg{local})$ i.e.

$\phi' = \{x \mapsto v| x \mapsto v \in \chi\ \wedge \ (v \in \IntSet\ \vee\ v = \true\ \vee\ v = false)\ \vee\ (\exists \alpha, \ v = \alpha \wedge \class{(\chi, \phi : \psi)}{\alpha} \in M\}$

The encapsulation proof system consists of two relations

* Purely internal expressions: $\proves{M}{\givenA{A}{\intrnl{e}}}$ and

* Assertion encapsulation: $\proves{M}{\givenA{A}{\encaps{A'}}}$

Fig. <ref> gives proof rules for an expression comprising purely internal objects.
[]Primitives are $Enc_e$ (Enc$_e$-Int, Enc$_e$-Null, Enc$_e$-True, and Enc$_e$-False).
Addresses of internal objects are $Enc_e$ (Enc$_e$-Obj). Field accesses with internal types of $Enc_e$ expressions
are themselves $Enc_e$ (Enc$_e$-Field). Ghost field accesses annotated as $Enc_e$ on $Enc_e$
expressions are themselves $Enc_e$ (Enc$_e$-Ghost).

MA ⟶ α: C

C ∈ M

MA ⟶ e : C

[field _ f : D] ∈ M(C).(flds)

D ∈ M

MA ⟶ e_1 : C

ghost intrnl g(x : _){e} ∈M(C).(gflds)

Internal Proof Rules

[]Fig. <ref> gives proof rules for whether an assertion is encapsulated, that is whether
a change in satisfaction of an assertion requires interaction with the internal module.
An Intrl expression is also an encapsulated assertion (Enc-Exp). A field
access on an encapsulated expression is an encapsulated expression. Binary and ternary operators
applied to encapsulated expressions are themselves encapsulated assertions (Enc-=, Enc-+, Enc-<, Enc-If).
An internal object may only lose access to another object via internal computation (Enc-IntAccess).
Only internal computation may grant external access to an $\wrapped{\_}$ object (Enc-Inside$_1$).
If an object is $\wrapped{\_}$, then nothing (not even internal objects) may gain access
to that object except by internal computation (Enc-Inside$_2$).
If an assertion $A_1$ implies assertion $A_2$, then $A_1$ implies the encapsulation of any assertion that
$A_2$ does. Further, if an assertion is encapsulated, then any assertion that is implied by it is also encapsulated.
These two rules combine into an encapsulation rule for consequence (Enc-Conseq).

MAe_1 = e_2

MAe_1 + e_2

MAe_1 < e_2

MAif e then e_1 else e_2

MA ⟶ x

Mx : Cx
MA ⟶ x

MA_1 ⟶ A_2

MA ⟶ A'

Assertion Encapsulation Proof Rules

§ MORE ABOUT THE EXPRESSIVENESS OF SPECIFICATIONS

§.§ ERC20

The ERC20 <cit.> is a widely used token standard describing the basic functionality of any Ethereum-based token
contract. This functionality includes issuing tokens, keeping track of tokens belonging to participants, and the
transfer of tokens between participants. Tokens may only be transferred if there are sufficient tokens in the
participant's account, and if either they (using the transfer method) or someone authorized by the participant (using the transferFrom method) initiated the transfer.

We specify these necessary conditions here using . Firstly, ERC20Spec1
says that if the balance of a participant's account is ever reduced by some amount $m$, then
that must have occurred as a result of a call to the transfer method with amount $m$ by the participant,
or the transferFrom method with the amount $m$ by some other participant.
[language = Chainmail, mathescape=true, frame=lines]
ERC20Spec1 $\triangleq$ from e : ERC20 $\wedge$ e.balance(p) = m + m' $\wedge$ m > 0
next e.balance(p) = m'
onlyIf $\exists$ p' p”.[$\calls{\prg{p'}}{\prg{e}}{\prg{transfer}}{\prg{p, m}}$ $\vee$
e.allowed(p, p”) $\geq$ m $\wedge$ $\calls{\prg{p''}}{\prg{e}}{\prg{transferFrom}}{\prg{p', m}}$]

Secondly, ERC20Spec2 specifies under what circumstances some participant p' is authorized to
spend m tokens on behalf of p: either p approved p', p' was previously authorized,
or p' was authorized for some amount m + m', and spent m'.
[language = Chainmail, mathescape=true, frame=lines]
ERC20Spec2 $\triangleq$ from e : ERC20 $\wedge$ p : Object $\wedge$ p' : Object $\wedge$ m : Nat
next e.allowed(p, p') = m
onlyIf $\calls{\prg{p}}{\prg{e}}{\prg{approve}}{\prg{p', m}}$ $\vee$
(e.allowed(p, p') = m $\wedge$
$\neg$ ($\calls{\prg{p'}}{\prg{e}}{\prg{transferFrom}}{\prg{p, \_}}$ $\vee$
$\calls{\prg{p}}{\prg{e}}{\prg{allowed}}{\prg{p, \_}}$)) $\vee$
$\exists$ p”. [e.allowed(p, p') = m + m' $\wedge$ $\calls{\prg{p'}}{\prg{e}}{\prg{transferFrom}}{\prg{p'', m'}}$]

§.§ DAO

The Decentralized Autonomous Organization (DAO) <cit.>  is a well-known Ethereum contract allowing
participants to invest funds. The DAO famously was exploited with a re-entrancy bug in 2016,
and lost $50M. Here we provide specifications that would have secured the DAO against such a
bug. DAOSpec1 says that no participant's balance may ever exceed the ether remaining
in DAO.
[language = Chainmail, mathescape=true, frame=lines]
DAOSpec1 $\triangleq$ from d : DAO $\wedge$ p : Object
to d.balance(p) > d.ether
onlyIf false

Note that DAOSpec1 enforces a class invariant of DAO, something that could be enforced
by traditional specifications using class invariants.
The second specification DAOSpec2 states that if after some single step of execution, a participant's balance is m, then

(a) this occurred as a result of joining the DAO with an initial investment of m,

(b) the balance is 0 and they've just withdrawn their funds, or

(c) the balance was m to begin with

[language = Chainmail, mathescape=true, frame=lines]
DAOSpec2 $\triangleq$ from d : DAO $\wedge$ p : Object
next d.balance(p) = m
onlyIf $\calls{\prg{p}}{\prg{d}}{\prg{repay}}{\prg{\_}}$ $\wedge$ m = 0 $\vee$ $\calls{\prg{p}}{\prg{d}}{\prg{join}}{\prg{m}}$ $\vee$ d.balance(p) = m

[small changes over Julian's]

§.§ Safe

<cit.> used as a running example   a Safe, where a treasure
was secured within a  object, and access to the treasure was only granted by
providing the correct password.
Using , we express , that requires that the treasure cannot be
removed from the safe without knowledge of the secret.
[language = Chainmail, mathescape=true, frame=lines]
SafeSpec $\triangleq$ from s : Safe $\wedge$ s.treasure != null
to s.treasure == null
onlyIf $\neg$ inside(s.secret)

The module  SafeModule described  below satisfies  SafeSpec.

module SafeModule
class Secret
class Treasure
class Safe
field treasure : Treasure
field secret : Secret
method take(scr : Secret)
if (this.secret==scr) then
this.treasure = null
return t

§ MORE LOGIC RULES

Here we give the complete version of the rules in []Fig. <ref>, Fig. <ref>, and
Fig. <ref>.

for all  C ∈dom(M)  and   m ∈M(C).mths,    				MA_1 ∧ x : C ∧ _xmz

MA_1 ⟶ A_2

M ⊢ A_1A_2A_3

MA_1 ⟶A_1'

MA_2 ⟶A_2'

MA_3' ⟶A_3

MA_1 ∨ A_1'A_2A ∨ A'

MA_1A_2 ∨ A_2'A ∨ A'

MA_1A_2A ∨ A'

MA_1A_2A ∧ A'

∀y,  M([y / x]A_1)A_2A

M∃x. [A_1]A_2A

∀y,  MA_1([y / x]A_2)A

MA_1∃x. [A_2]A

Single-Step Specifications

MA_1 ⟶ A_1'

MA_2 ⟶ A_2'

MA_3' ⟶ A_3

MA_1 ∨ A_1'A_2A ∨ A'

MA_1A_2 ∨ A_2'A ∨ A'

MA_1A_2A ∨ A'

MA_1A_2A ∨ A'

∀y,  M([y / x]A_1)A_2A

M∃x. [A_1]A_2A

∀y,  MA_1([y / x]A_2)A

Only Through

MA_1 ⟶ A_1'

MA_2 ⟶ A_2'

MA_3' ⟶ A_3

MA_1 ∨ A_1'A_2A ∨ A'

MA_1A_2 ∨ A_2'A ∨ A'

MA_1A_2A ∨ A'

MA_1A_2A ∧ A'

Mx : C x : C

∀y,  M([y / x]A_1)A_2A

M∃x. [A_1]A_2A

∀y,  MA_1([y / x]A_2)A

Only If

§ LOGIC

Fig. <ref> presents some rules the
proof system relies upon, of the form $\proves{M}{A}$. These rules
are relatively simple, with none presenting any surprising results,
and would be straightforward, but rather time-consuming, to
prove sound in the Coq mechanisation.
Caller-Ext, Caller-Recv, Caller-Args,
and Class-Int are simple properties that arise from
the semantics of .
Fld-Class and Inside-Int are directly drawn from
the simple type system of .
Absurd and Excluded Middle are common logical properties.

Mxymz ⟶ x

Mxymz ⟶ xy

Mxym…, z_i, … ⟶ xz_i
C ∈M
Mx : C ⟶ x
(field _ f : D) ∈ M(C).(flds)
Me : C ⟶ e.f : D
(class  C {_; _}) ∈ M
Mx : C ⟶ x

M ⟶ A

MA ∨ A
(Excluded Middle)

Properties of the proof system.

§  $\MODD$  – A MORE INTERESTING BANK ACCOUNT MODULE

We now revisit the bank account example, and present in Figure <ref>.
is more interesting than , as it allows us  to demonstrate how   logic
deals with  challenges that come with more complex data structures and specifications.
These challenges are

(1) Specifications defined using ghost fields – in this case b.balance(a) returns the balance of account a in Bank b.

(2) Modules with several    classes and methods; they all must be considered when constructing proofs about emergent behaviour.

(3)  The construction of a proof of assertion encapsulation. Such a proof is necessary  here because
the ghost field balance reads several  fields. We use our
simple confinement system,  captured by classes in .

[language=chainmail, mathescape=true, frame=lines]
module $\ModD$
class Account
field password:Object
method authenticate(pwd:Object):bool
return pwd == this.password
method changePass(pwd:Object, newPwd:Object):void
if pwd == this.password
this.password := newPwd
confined class Ledger
field acc1:Account
field bal1:int
field acc2:Account
field bal2:int
ghost intrnl balance(acc):int=
if acc == acc1
else if acc == acc2
else -1
method transfer(amt:int, from:Account, to:Account):void
if from == acc1        to == acc2
bal1 := bal1 - amt
bal2 := bal2 + amt
else if from == acc2        to == acc1
bal1 := bal1 + amt
bal2 := bal2 - amt
class Bank
field book:Ledger
ghost intrnrl balance(acc):int=book.balance(acc)
method transfer(pwd:Object, amt:int, from:Account, to:Account):void
if (from.authenticate(pwd))
book.transfer(amt, from, to)

$\ModD$ – a more interesting bank account implementation

In ,   the balance
of an account is kept in a ledger rather than in the account
consists of three classes: (1)  that
maintains a password, (2) , a public interface
for transferring money from one account to another, and (3) ,
a private class, annotated as , used to map  objects
to their balances.

A Bank has  a Ledger field, a method for transferring
funds between accounts (transfer), and a ghost field,
for looking up the balance of an account at a bank (balance).

A Ledger is
a mapping from Accounts to their balances. For brevity
our implementation only includes two accounts (acc1 and acc2),
but it is easy to see how this could extend to a Ledger
of arbitrary size. Ledger is annotated as , so
's Confined Types will ensure the necceary encapsulation.
Finally, an Account has some password object, and
methods to authenticate a provided password (authenticate),
and to change the password (changePass).

Figures <ref>,  <ref>,
and  <ref> give pre- and postcondition specifications for $\ModD$.
Informally, these
state that

(1) no method returns the password,

(2) the transfer method in Ledger results in a decreased balance to the from Account,

(3) and the transfer method in Bank results in a decreased balance to the from Account only if the correct password is supplied, and

(4) every other method in never modifies any balance in any Bank.

[language=chainmail, mathescape=true, frame=lines]
module $\ModD$
class Account
field password : Object
method authenticate(pwd : Object) : bool
(PRE:  a : Account $\wedge$ b : Bank
POST: b.balance(a)$_\prg{old}$ == b.balance(a)$_\prg{new}$)
(PRE:  a : Account
POST: res != a.password)
(PRE:  a : Account
POST: a.password$_\prg{old}$ == a.password$_\prg{new}$)
return pwd == this.password
method changePassword(pwd : Object, newPwd : Object) : void
(PRE:  a : Account
POST: res != a.password)
(PRE:  a : Account $\wedge$ b : Bank
POST: b.balance(a)$_\prg{old}$ == b.balance(a)$_\prg{new}$)
(PRE:  a : Account $\wedge$ pwd != this.password
POST: a.password$_\prg{old}$ = a.password$_\prg{new}$)
if pwd == this.password
this.password := newPwd

confined class Ledger
$\mbox{continued in  Fig.\ref{f:ex-bankTwo}}$

class Bank
$\mbox{continued in  Fig.\ref{f:ex-bankThree}}$

$\ModD$ , 1st part

[language=chainmail, mathescape=true, frame=lines]
confined class Ledger
field acc1 : Account
field bal1 : int
field acc2 : Account
field bal2 : int
ghost intrnl balance(acc) : int =
if acc == acc1
else if acc == acc2
else -1
method transfer(amt : int, from : Account, to : Account) : void
(PRE:  a : Account $\wedge$ b : Bank $\wedge$ (a != acc1 $\wedge$ a != acc2)
POST: b.balance(a)$_\prg{old}$ == b.balance(a)$_\prg{new}$)
(PRE:  a : Account
POST: res != a.password)
(PRE:  a : Account
POST: a.password$_\prg{old}$ == a.password$_\prg{new}$)
if from == acc1        to == acc2
bal1 := bal1 - amt
bal2 := bal2 + amt
else if from == acc2        to == acc1
bal1 := bal1 + amt
bal2 := bal2 - amt

$\ModD$ , 2nd part

[language=chainmail, mathescape=true, frame=lines]
class Bank
field book : Ledger
ghost intrnrl balance(acc) : int = book.balance(acc)
method transfer(pwd : Object, amt : int, from : Account, to : Account) : void
(PRE:  a : Account $\wedge$ b : Bank $\wedge$ $\neg$ (a == acc1 $\wedge$ a == acc2)
POST: b.balance(a)$_\prg{old}$ a= b.balance(a)$_\prg{new}$)
(PRE:  a : Account
POST: res != a.password)
(PRE:  a : Account
POST: a.password$_\prg{old}$ == a.password$_\prg{new}$)
if (from.authenticate(pwd))
book.transfer(amt, from, to)

$\ModD$ ,  3rd part

§ PROOF OF GUARANTEE OF SAFETY IN <REF>

In this section we provide a proof sketch that ensures our balance
does not decrease in contexts with no access to our password. This
property is expressed in <ref>, and the example is repeated below.

[mathescape=true, language=chainmail, frame=lines]
module $\ModParam{1}$
method cautious(untrusted:Object)
a = new Account
p = new Password

The guarantee for the above code snippet is that  as long as
untrusted does not have external access (whether transitive or direct)
to a.pwd before the call on line 7, then a.balance will not decrease during the
execution of line 8. This property is expressed and proven in Theorem <ref>.

Let BankMdl be some module that satisfies , let
$M$ be any external module, and $\sigma_1 = (\chi_1, \phi_1 : \psi_1)$ be some Arising program state,

* the continuation of $\sdN{\phi_1}$ is

* $\sigma_2 = (\chi_2, \phi_2 : \psi_2)$ is the program state immediately preceding the execution of s

* $\sigma_3 = (\chi_3, \phi_3 : \psi_3)$ is the program state immediately following the execution of s

* $\sigma_4 = (\chi_4, \phi_4 : \psi_4)$ is the program state immediately following the execution of
untrusted.make_payment(a, z1, ..., zn)

* for all objects $o \in \chi_3$ which are transitively accessible (i.e. the transitive closure of $\access{\_}{\_}$) from untrusted
or from z1,...zn:

$\strut \ \ \ \  \ \ \satisfies{\prg{BankMdl}; \sigma_3}{\access{o}{\sdN{\prg{a.pwd}}}}$,   implies     $\satisfies{\prg{BankMdl}; \sigma_3}{\internal{o}}$,

* $\satisfies{\prg{BankMdl}; \sigma_3}{\prg{a.balance} = b}$

* $\satisfies{\prg{BankMdl};\sigma_4}{\prg{a.balance} \geq b}$.

Proof Idea

We would like to apply in state $\sigma_3$, and argue that since by (5) no external object transitively accessible from a,
untrusted, z1, ... zn has access to the password, the balance in $\sigma_4$ will not decrease over what it was in $\sigma_3$.
However, the challenge is that the premise of is stronger than what we have in (5). Namely the premise of requires
that no external object has (direct) access to the password, but this
requirement might not hold in  $\sigma_3$: depending on the contents of the code in s, there may exist  external
objects that have access to a.password.  For example, if s
is the empty code, then $\sigma_1(\prg{this})$ has access to a.

To address this challenge, we will   create
a program state, say $\sigma_3'$. In the new program state $\sigma_3'$ there will be no external access to a.password.
Also, $\sigma_3'$  must be similar enough to
$\sigma_3$ so  that the execution of untrusted.make_payment(a, z1, ..., zn) starting from state $\sigma_3$ is effectively
equivalent to the execution of untrusted.make_payment(a, z1, ..., zn)  when starting from  $\sigma_3'$.
Moreover,  $\sigma_3'$, must also be Arising for us to apply the specification
to it.

This throws up a new challenge: $\sigma_3'$ is not necessarily Arising in BankMdl and $M$. We address the latter challenge by creating a new module, $M'$, such that  $\arising{M'}{\prg{BankMdl}}{\sigma_3'}$.

Proof Sketch

We construct $M'$ from $M$ by 1) modifying  all methods in all
classes in $M$  so that all methods are duplicated: a) the original version, and b)
a version almost identical  to that in $M$ with the addition that it keeps track of all the objects which contain fields pointing to
any objects of the Password class,
2) We add to all classes in $M$ a method called nullify
that compares the contents of each of its fields with the method's argument, and if they are
equal overwrites the field with null,
3) all method calls  are replaced by those in part 1a, except of the body of make_payment,
4) we modify the code in s (and any methods called from it) so that it also keeps track of the current value of
5) after s and before the call untrusted.make_payment(a, z1, ..., zn) we insert  code which
runs through the list created in part 1, and calls nullify with the current value of a.pwd by null as its argument.

By staring with the same initial configuration which reached $\sigma_3$,
but now using $M'$ as the external module, we reach $\sigma_3'$,
that is, $\arising{M'}{\prg{BankMdl}}{\sigma_3'}$. Moreover,  $\sigma_3'$
satisfies the premise of  .
We execute $\prg{untrusted}\prg{.make\_payment}\prg{(a, z1, ..., zn)}$ in the context of   $\sigma_3'$
and reach $\sigma_4'$. We apply  , and obtain that $\satisfies{\prg{BankMdl};\sigma_4'}{\prg{a.balance} \geq b}$.

We use the latter fact, to conclude that $\satisfies{\prg{BankMdl};\sigma_4}{\prg{a.balance} \geq b}$.
Namely, $\sigma_3$ and $\sigma_3'$ are equivalent – up to renaming of addresses  – for all all the objects which are
reachable from o, z1, ... zn, and for all objects from
$\prg{BankMdl}$. Therefore, the execution of make_payment in $M;\prg{BankMdl}$ and $\sigma_3$
will be "equivalent" to that in $M';\prg{BankMdl}$ and $\sigma_3'$. Therefore, $\sigma_4$ and $\sigma_4'$ are equivalent – up to renaming of addresses  – for all all the objects which are
reachable from o, z1, ... zn and for all objects from
This gives us that  $\satisfies{\prg{BankMdl};\sigma_4}{\prg{a.balance} \geq b}$.

[]is able to encode the motivating example of VerX:
an escrow smart contract that ensures that the contract may not be coerced to
pay out or refund more money than has been raised.
The motivating Crowdsale example consists of a Crowdsale contract
for crowd sourcing funding. A Crowdsale object consists of an Escrow object,
an amount raised, a funding goal, and a closing time in which the goal must be met for
the fund to be successful. An Escrow consists of a ledger of investors and how much
they have invested. There are several properties that VerX sought to encode,
and we have provided the encoding of those specifications in Fig. <ref>.
R0 states that if an investor claims a refund from an escrow, then the balance of
the escrow decreases by the amount the investor had deposited in the escrow.
R1 states that if at anytime the escrow has not yet succeeded, then the deposits must
be less than the balance of the escrow.
R2_1 and R2_2 combine to express a single property: no one may ever withdraw and
then subsequently claim a refund or visa versa.
R3 states that if the funding goal is ever met, then no one may subsequently claim a refund.

class Crowdsale
Escrow escrow;
closeTime, raised, goal : int;
method init()
if escrow == null
escrow := new Escrow(new Object);
closeTime := now + 30 days;
raised := 0;
goal := 10000 * 10**18;

method invest(investor : Object, value : int)
if raised < goal
escrow.deposit(investor, value);
raised += value;

method close()
if now > closeTime || raised >= goal
if raised >= goal

Crowdsale Contract

confined class Escrow
owner, beneficiary : Object;
mapping(Object => uint256) deposits;
OPEN, SUCCESS, REFUND : Object;
state : Object;
method init(o : Object, b : Object)
if owner == null || beneficiary == null
owner := o;
beneficiary := b;
OPEN := new Object; SUCCESS := new Object; REFUND := new Object;
state := OPEN;

method close() state = SUCCESS;
method refund() state = REFUND;
method deposit(value : int, p : Object)
deposits[p] := deposits[p] + value;

method withdraw()
if state == SUCCESS
return this.balance;

method claimRefund(p : Object)
if state == REFUND
int amount := deposits[p];
deposits[p] := 0;
return amount;

Escrow Contract

[mathescape=true, language=chainmail]
(R0) $\triangleq$ e : Escrow $\wedge$ $\calls{\_}{\prg{e}}{\prg{claimRefund}}{\prg{p}}$
next e.balance = nextBal onlyIf nextBal = e.balance - e.deposits(p)
(R1) $\triangleq$ e : Escrow $\wedge$ e.state $\neq$ e.SUCCESS $\longrightarrow$ sum(deposits) $\leq$ e.balance
(R2_1) $\triangleq$ e : Escrow $\wedge$ $\calls{\_}{\prg{e}}{\prg{withdraw}}{\prg{\_}}$
to $\calls{\_}{\prg{e}}{\prg{claimRefund}}{\prg{\_}}$ onlyIf false
(R2_2) $\triangleq$ e : Escrow $\wedge$ $\calls{\_}{\prg{e}}{\prg{claimRefund}}{\prg{\_}}$
to $\calls{\_}{\prg{e}}{\prg{withdraw}}{\prg{\_}}$ onlyIf false
(R3) $\triangleq$ c : Crowdsale $\wedge$ sum(deposits) $\geq$ c.escrow.goal
to $\calls{\_}{\prg{c.escrow}}{\prg{claimRefund}}{\prg{\_}}$ onlyIf false

Encoding VerX Crowdsale Example in Necessity