Reykjavík University, Menntavegur 1, 102 Reykjavík, Iceland<EMAIL_ADDRESS>https://orchid.org/0000-0002-2197-3018 Supported by the Icelandic Research
Fund Grant No. 218202-05(1-3). Sapienza, Università di Roma, Rome, Italy
<EMAIL_ADDRESS>https://orchid.org/0000-0001-8859-9844 Reykjavík
University, Menntavegur 1, 102 Reykjavík, Iceland<EMAIL_ADDRESS>https://orcid.org/0000-0001-8219-2285 Supported by the Icelandic Research Fund
Grant No. 218202-05(1-3). Luca Aceto, Daniele Gorla and Stian Lybech

###### Acknowledgements.

We thank the anonymous reviewers for their constructive attitude and for the
fruitful comments that helped us improve our paper. <ccs2012> <concept>
<concept_id>10003752.10010124.10010138.10010143</concept_id>
<concept_desc>Theory of computation Program analysis</concept_desc>
<concept_significance>500</concept_significance> </concept> <concept>
<concept_id>10003752.10010124.10010125.10010130</concept_id>
<concept_desc>Theory of computation Type structures</concept_desc>
<concept_significance>500</concept_significance> </concept> </ccs2012>
[500]Theory of computation Program analysis [500]Theory of computation Type
structures 2 38th European Conference on Object-Oriented Programming(ECOOP
2024) ECOOP 2024 ECOOP 2024 September 16–20, 2024 Vienna, Austria

# A Sound Type System for Secure Currency Flow

Luca Aceto  Daniele Gorla  Stian Lybech

###### Abstract

In this paper we focus on TinySol, a minimal calculus for Solidity smart
contracts, introduced by Bartoletti et al. We start by rephrasing its syntax
(to emphasise its object-oriented flavour) and give a new big-step operational
semantics. We then use it to define two security properties, namely call
integrity and noninterference. These two properties have some similarities in
their definition, in that they both require that some part of a program is not
influenced by the other part. However, we show that the two properties are
actually incomparable. Nevertheless, we provide a type system for
noninterference and show that well-typed programs satisfy call integrity as
well; hence, programs that are accepted by our type system satisfy both
properties. We finally discuss the practical usability of the type system and
its limitations by means of some simple examples.

###### keywords:

smart contracts, call integrity, noninterference, type system

##  1 Introduction

The classic notion of noninterference [11] is a well-known concept that has
been applied in a variety of settings to characterise both integrity and
secrecy in programming. In particular, this property has been defined by
Volpano et al. [27] in terms of a lattice model of security levels (e.g.
‘High’ and ‘Low’, or ‘Trusted’ and ‘Untrusted’); the key point being that
information must not flow from a higher to a lower level. Thus, the lower
levels are unaffected by the higher ones, and, conversely, the higher levels
are ‘noninterfering’ with the lower ones.

Ensuring noninterference seems particularly relevant in a setting where not
only information, but also _currency_ , flows between programs. This is a core
feature of _smart contracts_ , which are programs that run atop a blockchain
and are used to manage financial assets of users, codify transactions, and
implement custom tokens; see e.g. [23] for an overview of the architecture.
The code of a smart contract resides on the blockchain itself, and is
therefore both immutable and publicly visible. This is one of the important
ways in which the ‘smart-contract programming paradigm’ differs from
conventional programming languages.

Public visibility means that _vulnerabilities_ in the code can be found and
exploited by a malicious user. Moreover, if a vulnerability is discovered,
immutability prevents the contract creator from correcting the error. Thus, it
is obviously desirable to ensure that a smart contract is safe and correct
_before_ it is deployed onto the blockchain.

The combination of immutability and visibility has led to huge financial
losses in the past (see, e.g., [1, 7, 18, 19, 25]). A particularly spectacular
example was the infamous DAO-attack on the Ethereum platform in 2016, which
led to a loss of 60 million dollars [7]. This was made possible because a
certain contract (the DAO contract, storing assets of users) was _reentrant_ ,
that is, it allowed itself to be called back by the recipient of a transfer
_before_ recording that the transfer had been completed.

⬇

1contract X { contract Y {

2 ... ...

3 field called := F; deposit(x) {

4 transfer(z) { x.transfer(this):0

5 if $\neg$called $\land$ this.balance $\geq$ 1 }

6 then z.deposit(this):1; }

7 this.called := T;

8 else skip

9 }

10}

Figure 1: Illustration of reentrancy written in the language TinySol.

_Reentrancy_ is a pattern based on mutual recursion, where one method $f$
calls another method $g$ whilst also transferring an amount of currency along
with the call. If $g$ then immediately calls $f$ back, it may yield a
recursion where $f$ will keep transferring funds to $g$. We can illustrate the
problem as in Figure 1, using a simple, imperative and class-based model
language called TinySol [2]. This model language, which we shall formally
describe in Section 2, captures some of the core features of the smart-
contract language Solidity [9], which is the standard high-level language used
to write smart contracts for the Ethereum platform. A key feature of this
language is that contracts have an associated balance, representing the amount
of currency stored in each contract, which cannot be modified _except_ through
method calls to other contracts. Each method call has an extra parameter,
representing the amount of currency to be transferred along with the call, and
a method call thus represents a (potential) outgoing currency flow.

In Figure 1, X.transfer(z) first does a sanity check to ensure that it has not
already been called and that the contract contains sufficient funds, which are
stored in the balance field. Then it calls z.deposit(this) and transfers 1
unit of currency along with the call, where z is the address received as
parameter. However, suppose the address received is Y. Then Y.deposit(x)
immediately calls X.transfer(z) back, with this as actual parameter; this
yields a mutual recursion, because the field called will never be set to T. A
transaction that invokes X.transfer(Y) with any number of currency units will
trigger the recursion.

The problem is that currency cannot be transferred without also transferring
control to the recipient, and the execution of X.transfer(z) comes to depend
on unknown and untrusted code in the contract residing at the address received
as the actual parameter. Simply switching the order of lines 6 and 7 in X
solves the problem in this particular case, but it might not always be
possible to move external calls to the last position in a sequence of
statements. Furthermore, the execution of a function $f$ can also depend on
external fields, and not only on external calls. Thus, reentrancy is not just
a purely syntactic property.

The property of reentrancy in Ethereum smart contracts has been formally
characterised by Grishchenko et al. in [12]. Specifically, they define another
property, named _call integrity_ , which implies the absence of reentrancy
(see [12, Theorem 1]) and has been identified in the literature as one of the
safety properties that smart contracts should have. Informally, this property
requires any call to a method in a ‘trusted’ contract (say, $X$) to yield the
exact same sequence of currency flows (i.e. method calls) even if some of the
other ‘untrusted’ contracts (or their stored values) are changed. In a sense,
the code and values of the other contracts, which could be controlled by an
attacker, must not be able to affect the currency flow from $X$.

A disadvantage of the definition of call integrity given in [12] is that it
relies on a universal quantification over all possible execution contexts,
which makes it hard to be checked in practice. However, call integrity seems
intuitively to be related to noninterference, in the sense that both stipulate
that changes in one part of a program should not have an effect upon another
part. Even though we discover that the two properties are incomparable, one
might hope to be able to apply techniques for ensuring noninterference to also
capture call integrity. Specifically, Volpano et al. [27] show that
noninterference can be soundly approximated using a type system. In the
present paper, we shall therefore create an adaptation of this type system for
secure-flow analysis to the setting of smart contracts and show that the
resulting type system _also_ captures call integrity.

To recap, our main contributions in this paper are: (1) a thorough study of
the connections between call integrity and noninterference for smart contracts
written in the language TinySol, and (2) a sound type system guaranteeing
(noninterference and) call integrity for programs written in that language. We
choose TinySol because it provides a minimal calculus for Solidity contracts
and thus allows us to focus on the gist of our main contributions in a simple
setting. In doing this, we also provide a simpler operational semantics for
this language; this can be considered a third contribution of our work.

The paper is organised as follows: In Section 2, we describe a revised version
of the smart-contract language TinySol [2]. In Section 3, we adapt the
definition of call integrity from [12] and of noninterference from [24] to
this language; we then show that these two desirable properties are actually
incomparable. Nevertheless, there _is_ an overlap between them. In Section 4,
we create a type system for ensuring noninterference in TinySol, along the
lines of Volpano et al. [27], and prove a type soundness result (Theorems
4.5–4.8). Our main result is Theorem 4.12, which shows that well-typedness
provides a sound approximation to _both_ noninterference _and_ call integrity.
This is used on a few examples in Section 5, where we also discuss the
limitations of the type system. We survey some related work in Section 6 and
conclude the paper with some directions for future research in Section 7. All
proofs and some technical details are relegated to the appendix for space
reasons.

##  2 The TinySol language

In [2], Bartoletti et al. present the TinySol language, a standard imperative
language (similar to Dijkstra’s While language [17]), extended with classes
(contracts) and two constructs: (1) a throw command, representing a fatal
error, and (2) a procedure call, with an extra parameter $n$, denoting an
amount of some digital asset, which is transferred along with the call from
the caller to the callee. TinySol captures (some of) the core features of
Solidity, and, in particular, it is sufficient to represent reentrancy
phenomena. In this section, we present a version of TinySol which has been
adapted to facilitate our later developments of the type system. Compared to
the presentation in [2], we have, in particular, added explicit declarations
of variables (local to the scope of a method) and fields (corresponding to the
_keys_ in the original presentation) to have a place for type annotations in
the syntax.

###  2.1 Syntax

$\begin{array}[]{r @{~} c @{~} l}DF\in\text{Dec}_{F}\leavevmode\nobreak\
&::=\hfil\leavevmode\nobreak\ &\epsilon\leavevmode\nobreak\
\leavevmode\nobreak\ \big{|}\leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \texttt{field p := $v$;}DF\cr
DM\in\text{Dec}_{M}\leavevmode\nobreak\ &::=\hfil\leavevmode\nobreak\
&\epsilon\leavevmode\nobreak\ \leavevmode\nobreak\ \big{|}\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \texttt{$f(\widetilde{x})$ \\{ $S$
\\} }DM\cr DC\in\text{Dec}_{C}\leavevmode\nobreak\
&::=\hfil\leavevmode\nobreak\ &\epsilon\leavevmode\nobreak\
\leavevmode\nobreak\ \big{|}\leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \texttt{contract $X$ \\{ }\cr\leavevmode\nobreak\
&\hfil\leavevmode\nobreak\ &\qquad\ \ \ \texttt{field balance := $n$;
$DF$}\cr\leavevmode\nobreak\ &\hfil\leavevmode\nobreak\ &\qquad\ \ \
\texttt{send() \\{ skip \\} $DM$}\cr\leavevmode\nobreak\
&\hfil\leavevmode\nobreak\ &\qquad\ \texttt{\\} $DC$}\cr
m\in\text{MVar}\leavevmode\nobreak\ &::=\hfil\leavevmode\nobreak\
&\texttt{this}\leavevmode\nobreak\ \leavevmode\nobreak\
\big{|}\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\texttt{sender}\leavevmode\nobreak\ \leavevmode\nobreak\
\big{|}\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\texttt{value}\cr L\in\text{LVal}\leavevmode\nobreak\
&::=\hfil\leavevmode\nobreak\ &x\leavevmode\nobreak\ \leavevmode\nobreak\
\big{|}\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\texttt{this.$p$}\cr e\in\text{Exp}\leavevmode\nobreak\
&::=\hfil\leavevmode\nobreak\ &v\leavevmode\nobreak\ \leavevmode\nobreak\
\big{|}\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
x\leavevmode\nobreak\ \leavevmode\nobreak\ \big{|}\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\
m\quad|\quad\texttt{$e$.balance}\leavevmode\nobreak\ \leavevmode\nobreak\
\big{|}\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\ \texttt{
$e$.$p$ }\leavevmode\nobreak\ \leavevmode\nobreak\ \big{|}\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \operatorname{op}(\widetilde{e})\cr
S\in\text{Stm}\leavevmode\nobreak\ &::=\hfil\leavevmode\nobreak\
&\texttt{skip}\leavevmode\nobreak\ \leavevmode\nobreak\
\big{|}\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\texttt{throw}\leavevmode\nobreak\ \leavevmode\nobreak\
\big{|}\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\texttt{var $x$ := $e$ in $S$}\leavevmode\nobreak\ \leavevmode\nobreak\
\big{|}\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\texttt{$L$ := $e$}\leavevmode\nobreak\ \leavevmode\nobreak\
\big{|}\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\texttt{$S_{1}$;$S_{2}$}\cr\leavevmode\nobreak\ &\leavevmode\nobreak\
\leavevmode\nobreak\
\big{|}\nobreak\leavevmode\nobreak\leavevmode\nobreak\leavevmode\hfil\leavevmode\nobreak\
&\texttt{if $e$ then $S_{\text{T}}$ else $S_{\text{F}}$ }\leavevmode\nobreak\
\leavevmode\nobreak\ \big{|}\leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \texttt{while $e$ do $S$}\leavevmode\nobreak\
\leavevmode\nobreak\ \big{|}\leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \texttt{$e_{1}$.$f(\widetilde{e})$:$e_{2}$}\cr
v\in\text{Val}\leavevmode\nobreak\ &::=\hfil\leavevmode\nobreak\
&\mathbb{N}\cup\mathbb{B}\cup\text{ANames}\cr\leavevmode\nobreak\
\cr\lx@intercol\text{where }x,y\in\text{VNames}\text{ (variable
names)},p,q\in\text{FNames}\text{ (field
names)},\hfil\lx@intercol\cr\lx@intercol\qquad\quad X,Y\in\text{ANames}\text{
(address names)},f,g\in\text{MNames}\text{ (method
names)}\hfil\lx@intercol\end{array}$

Figure 2: The syntax of TinySol.

The syntax of TinySol is given in Figure 2, where we use the notation
$\mathop{\tilde{\cdot}}$ to denote (possibly empty) sequences of items. The
set of _values_ , ranged over by $v$, is formed by the sets of integers
$\mathbb{N}$, ranged over by $n$, booleans
$\mathbb{B}=\left\\{\,\text{T},\text{F}\,\right\\}$, ranged over by $b$, and
address names ANames, ranged over by $X,Y$.

We introduce explicit declarations for fields $DF$, methods $DM$, and
contracts $DC$. The latter also encompasses declarations of accounts: an
_account_ is a contract that contains only the declarations of a special field
balance and of a single special method send(), which does nothing and is used
only for transferring funds to the account. By contrast, a contract usually
contains other declarations of fields and methods. For the sake of simplicity,
we make no syntactic distinction between an account and a contract but, for
the purpose of distinguishing, we can assume that the set ANames is split into
contract addresses and account addresses.

We have four ‘magic’ keywords in our syntax:

  * •

balance (type int), a special field recording the current balance of the
contract (or account). It can be read from, but not directly assigned to,
except through method calls. This ensures that the total amount of currency
‘on-chain’ remains constant during execution.

  * •

value (type int), a special variable that is bound to the currency amount
transferred with a method call.

  * •

sender (type address), a special variable that is always bound to the address
of the caller of a method.

  * •

this (type address), a special variable that is always bound to the address of
the contract containing the currently executing method.

The last three of these are local variables, and we collectively refer to them
as ‘magic variables’ $m\in\text{MVar}$. The declaration of variables and
fields are very alike: the main difference is that variable bindings will be
created at runtime (and with scoped visibility), hence we can let the initial
assignment be an _expression_ $e$; whilst the initial assignment to fields
must be _values_ $v$.

The core part of the language is the declaration of expressions $e$ and
statements $S$, that are almost the same as in [2]. The main differences are:
(1) we introduce fields $p$ in expressions, instead of keys; (2) we explicitly
distinguish between (global) fields and (local) variables, where the latter
are declared with a scope limited to a statement $S$; and (3) we introduce
explicit _lvalues_ $L$, to restrict what can appear on the left-hand side of
an assignment (in particular, this ensures that the special field balance can
never be assigned to directly).

As in the original presentation of TinySol, we can also use our new
formulation of the language to describe transactions and blockchains. A
_transaction_ is simply a call, where the caller is an account $A$, rather
than a contract. We denote this by writing $A$->$X$.$f(\widetilde{v})$:$n$,
which expresses that the account $A$ calls the method $f$ on the contract
(residing at address) $X$, with actual parameters $\widetilde{v}$, and
transferring $n$ amount of currency with the call. We can then model
blockchains as follows:

######  Definition 2.1 (Syntax of blockchains).

A _blockchain_ $B\in\mathcal{B}$ is a list of initial contract declarations
$DC$, followed by a sequence of transactions $T\in\text{Tr}$:

$B::=\texttt{$DC$ $T$}\qquad\qquad T::=\epsilon\leavevmode\nobreak\
\leavevmode\nobreak\ \big{|}\leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \texttt{$A$->$X$.$f$($\widetilde{v}$):$n$,$T$}$

Notationally, a blockchain with an empty $DC$ will be simply written as the
sequence of transactions.

###  2.2 Big-step semantics

To define the semantics, we need some environments to record the bindings of
variables (including the three magic variable names this, sender and value),
fields, methods, and contracts. We define them as sets of partial functions as
follows:

######  Definition 2.2 (Binding model).

We define the following sets of partial functions:

$\displaystyle\text{env}_{V}\in\text{Env}_{V}$
$\displaystyle:\text{VNames}\cup\text{MVar}\rightharpoonup\text{Val}$
$\displaystyle\text{env}_{S}\in\text{Env}_{S}$
$\displaystyle:\text{ANames}\rightharpoonup\text{Env}_{F}$
$\displaystyle\text{env}_{F}\in\text{Env}_{F}$
$\displaystyle:\text{FNames}\cup\left\\{\,\texttt{balance}\,\right\\}\rightharpoonup\text{Val}$
$\displaystyle\text{env}_{T}\in\text{Env}_{T}$
$\displaystyle:\text{ANames}\rightharpoonup\text{Env}_{M}$
$\displaystyle\text{env}_{M}\in\text{Env}_{M}$
$\displaystyle:\text{MNames}\rightharpoonup\text{VNames}^{*}\times\text{Stm}$

We regard each environment $\text{env}_{X}$, for any
$X\in\left\\{\,V,F,M,S,T\,\right\\}$, as a list of pairs $(d,c)$ where
$d\in\operatorname{dom}\left(\text{env}_{X}\right)$ and
$c\in\operatorname{codom}\left(\text{env}_{X}\right)$. The notation
$\text{env}_{X}\kern-2.0pt\left[d\mapsto c\right]$ denotes the update of
$\text{env}_{X}$ mapping $d$ to $c$. We write $\text{env}_{X}^{\emptyset}$ for
the empty environment. To simplify the notation, when two or more environments
appear together, we shall use the convention of writing the subscripts
together (e.g. $\text{env}_{MF}$ instead of $\text{env}_{M},\text{env}_{F}$).

Our binding model consists of two environments: a _method table_
$\text{env}_{T}$, which maps addresses to method environments, and a _state_
$\text{env}_{S}$, which maps addresses to lists of fields and their values.
Thus, for each contract, we have the list of methods it declares and its
current state; of course, the method table is constant, once all declarations
are performed, whereas the state will change during the evaluation of a
program.

####  2.2.1 Declarations

The semantics of declarations builds the field and method environments,
$\text{env}_{F}$ and $\text{env}_{M}$, and the state and method table
$\text{env}_{S}$ and $\text{env}_{T}$. We give the semantics in a classic big-
step style; thus, transitions are of the form
$\left<DX,\text{env}_{X}\right>\rightarrow_{DX}\text{env}_{X}^{\prime}$ for
$X\in\left\\{\,F,M,C,S,T\,\right\\}$, and their defining rules are given in
Figure 3. Notationally, here and in what follows, we denote with $e:l$ the
list that results from prepending an element $e$ to the list $l$. We assume
that field and method names are distinct within each contract; therefore, the
rules in Figure 3 define partial, finite functions.

[Dec-F1] $\dfrac{\phantom{P}}{\left<\epsilon,\text{env}_{F}\right>\rightarrow_{DF}\text{env}_{F}}\par$ [Dec-M1] $\dfrac{\phantom{P}}{\left<\epsilon,\text{env}_{M}\right>\rightarrow_{DM}\text{env}_{M}}\par$ [Dec-C1] $\dfrac{\phantom{P}}{\left<\epsilon,\text{env}_{ST}\right>\rightarrow_{DC}\text{env}_{ST}}\par$ [Dec-C2] $\dfrac{\left<DF,\text{env}_{F}^{\emptyset}\right>\rightarrow_{DF}\text{env}_{F}\quad\left<DM,\text{env}_{M}^{\emptyset}\right>\rightarrow_{DM}\text{env}_{M}\quad\left<DC,\text{env}_{ST}\right>\rightarrow_{DC}\text{env}_{ST}^{\prime}}{\left<\texttt{contract $X$ \\{ $DF$ $DM$ \\} $DC$},\text{env}_{ST}\right>\rightarrow_{DC}(X,\text{env}_{F}):\text{env}_{S}^{\prime},(X,\text{env}_{M}):\text{env}_{T}^{\prime}}$ |  [Dec-F2] $\dfrac{\left<DF,\text{env}_{F}\right>\rightarrow_{DF}\text{env}_{F}^{\prime}}{\left<\texttt{field $p$ := $v$;$DF$},\text{env}_{F}\right>\rightarrow_{DF}(p,v):\text{env}_{F}^{\prime}}\par$ [Dec-M2] $\dfrac{\left<DM,\text{env}_{M}\right>\rightarrow_{DM}\text{env}_{M}^{\prime}}{\left<\texttt{$f$($\widetilde{x}$) \\{ $S$ \\} $DM$},\text{env}_{M}\right>\rightarrow_{DM}(f,(\widetilde{x},S)):\text{env}_{M}^{\prime}}\par\vspace*{2.2cm}\par$
---|---
Figure 3: Semantics of declarations.  [Exp-Var] $\dfrac{k\in\operatorname{dom}\left(\text{env}_{V}\right)\quad\text{env}_{V}(k)=v}{\text{env}_{SV}\vdash k\rightarrow_{e}v}\par$ [Exp-Val] $\dfrac{\phantom{P}}{\text{env}_{SV}\vdash v\rightarrow_{e}v}\par$ |  [Exp-Op] $\dfrac{\text{env}_{SV}\vdash\widetilde{e}\rightarrow_{e}\widetilde{v}\quad\operatorname{op}(\widetilde{v})\rightarrow_{\operatorname{op}}v}{\text{env}_{SV}\vdash\operatorname{op}(\widetilde{e})\rightarrow_{e}v}\vspace*{1cm}$
---|---
|  [Exp-Field] $\dfrac{\text{env}_{SV}\vdash e\rightarrow_{e}X\quad
q\in\operatorname{dom}\left(\text{env}_{S}(X)\right)\quad\text{env}_{S}(X)(q)=v}{\text{env}_{SV}\vdash
e.q\rightarrow_{e}v}$
Figure 4: Semantics of expressions.

####  2.2.2 Expressions

Figure 4 gives the semantics of expressions $e$. Expressions have no side
effects, so they cannot contain method calls, but they can access both local
variables and fields of any contract. Thus expression evaluations are of the
form $\text{env}_{SV}\vdash e\rightarrow_{e}v$, i.e. they are relative to the
state and variable environments. We use $k$ to range over this, sender, value
and variables $x$ (i.e. $k\in\operatorname{dom}\left(\text{env}_{V}\right))$,
and $q$ to range over balance and fields $p$ (i.e.
$q\in\operatorname{dom}\left(\text{env}_{F}\right)$).

We do not give explicit rules for the boolean and integer operators subsumed
under $\operatorname{op}$, but simply assume that they can be evaluated to a
unique value by some semantics
$\operatorname{op}(\widetilde{v})\rightarrow_{\operatorname{op}}v$.111To
simplify the definitions, we assume that all operations are total. If this was
not the case, we would have needed some exception handling for partial
operations (e.g., division by zero). It follows that each expression evaluates
to a unique value relative to some given state and variable environments. Note
that we assume that no operation is defined for addresses $X$, so we disallow
any form of pointer arithmetic.

####  2.2.3 Statements

The semantics of statements describes the actual execution steps of a program.
In Figure 2.2.3 we give the semantics in big-step style, where a step
describes the execution of a statement in its entirety. Statements can read
from the method table and they can modify the state (i.e., the variable and
field bindings). The result of executing a statement is a new state, so
transitions must here be of the form
$\text{env}_{T}\vdash\left<S,\text{env}_{SV}\right>\rightarrow_{S}\text{env}_{SV}^{\prime}$
(recall that $\text{env}_{SV}^{\prime}$ stands for
$\text{env}_{S}^{\prime},\text{env}_{V}^{\prime}$), since both the field
values in $\text{env}_{S}$ and the values of the local variables in
$\text{env}_{V}$ may have been modified by the execution of $S$.

[BS-Skip] | $\dfrac{\phantom{P}}{\text{env}_{T}\vdash\left<\texttt{skip},\text{env}_{SV}\right>\rightarrow_{S}\text{env}_{SV}}\par$
---|---
[BS-Seq] | $\dfrac{\text{env}_{T}\vdash\left<S_{1},\text{env}_{SV}\right>\rightarrow_{S}\text{env}_{SV}^{\prime\prime}\quad\text{env}_{T}\vdash\left<S_{2},\text{env}_{SV}^{\prime\prime}\right>\rightarrow_{S}\text{env}_{SV}^{\prime}}{\text{env}_{T}\vdash\left<\texttt{$S_{1}$;$S_{2}$},\text{env}_{SV}\right>\rightarrow_{S}\text{env}_{SV}^{\prime}}\par$
[BS-If] | $\dfrac{\text{env}_{SV}\vdash e\rightarrow_{e}b\quad\text{env}_{T}\vdash\left<S_{b},\text{env}_{SV}\right>\rightarrow_{S}\text{env}_{SV}^{\prime}}{\text{env}_{T}\vdash\left<\texttt{if $e$ then $S_{\text{T}}$ else $S_{\text{F}}$ },\text{env}_{SV}\right>\rightarrow_{S}\text{env}_{SV}^{\prime}}\;\left(b\in\left\\{\,\text{T},\text{F}\,\right\\}\right)\par$
[BS-Loop${}_{\text{T}}$] |
[BS-Loop${}_{\text{F}}$] | $\dfrac{\text{env}_{SV}\vdash e\rightarrow_{e}\text{F}}{\text{env}_{T}\vdash\left<\texttt{while $e$ do $S$},\text{env}_{SV}\right>\rightarrow_{S}\text{env}_{SV}}\par$
[BS-DecV] | $\dfrac{\begin{array}[]{l}x\notin\operatorname{dom}\left(\text{env}_{V}\right)\qquad\text{env}_{SV}\vdash e\rightarrow_{e}v\\\ \text{env}_{T}\vdash\left<S,\text{env}_{S},(x,v):\text{env}_{V}\right>\rightarrow_{S}\text{env}_{S}^{\prime},(x,v^{\prime}):\text{env}_{V}^{\prime}\end{array}}{\text{env}_{T}\vdash\left<\texttt{var $x$ := $e$ in $S$, $\text{env}_{SV}$}\right>\rightarrow_{S}\text{env}_{SV}^{\prime}}\par$
[BS-AssV] | $\dfrac{x\in\operatorname{dom}\left(\text{env}_{V}\right)\qquad\text{env}_{SV}\vdash e\rightarrow_{e}v}{\text{env}_{T}\vdash\left<\texttt{$x$ := $e$},\text{env}_{SV}\right>\rightarrow_{S}\text{env}_{S},\text{env}_{V}\kern-2.0pt\left[x\mapsto v\right]}\par$
[BS-AssF] | $\dfrac{\text{env}_{V}(\texttt{this})=X\quad\text{env}_{S}(X)=\text{env}_{F}\quad p\in\operatorname{dom}\left(\text{env}_{F}\right)\quad\text{env}_{SV}\vdash e\rightarrow_{e}v}{\text{env}_{T}\vdash\left<\texttt{this.$p$ := $e$},\text{env}_{SV}\right>\rightarrow_{S}\text{env}_{S}\kern-2.0pt\left[X\mapsto\text{env}_{F}\kern-2.0pt\left[p\mapsto v\right]\right],\text{env}_{V}}\par$
[BS-Call] | $\dfrac{\begin{array}[]{l}\text{env}_{SV}\vdash e_{1}\rightarrow_{e}Y\qquad\text{env}_{S}(Y)\leavevmode\nobreak\ =\text{env}_{F}^{Y}\qquad(\text{env}_{T}(Y))(f)\leavevmode\nobreak\ =(\widetilde{x},S)\\\ |\widetilde{x}|\leavevmode\nobreak\ =|\widetilde{e}|=k\qquad\qquad\\!\text{env}_{SV}\vdash\widetilde{e}\rightarrow_{e}\widetilde{v}\qquad\ \ \ \text{env}_{SV}\vdash e_{2}\rightarrow_{e}n\\\ \text{env}_{V}(\texttt{this})\leavevmode\nobreak\ =X\qquad\text{env}_{S}(X)\leavevmode\nobreak\ =\text{env}_{F}^{X}\qquad n\leavevmode\nobreak\ \leq\text{env}_{F}^{X}(\texttt{balance})\\\ \text{env}_{S}^{\prime\prime}\leavevmode\nobreak\ =\text{env}_{S}\kern-2.0pt\left[X\mapsto\text{env}_{F}^{X}[\texttt{balance -= }n]\right]\kern-2.0pt\left[Y\mapsto\text{env}_{F}^{Y}[\texttt{balance += }n]\right]\\\ \text{env}_{V}^{\prime\prime}\leavevmode\nobreak\ =(\texttt{this},Y):(\texttt{sender},X):(\texttt{value},n):(x_{1},v_{1}):\ldots:(x_{k},v_{k}):\text{env}_{V}^{\emptyset}\\\ \text{env}_{T}\vdash\left<S,\text{env}_{SV}^{\prime\prime}\right>\rightarrow_{S}\text{env}_{SV}^{\prime}\end{array}}{\text{env}_{T}\vdash\left<\texttt{$e_{1}$.$f(\widetilde{e})$:$e_{2}$},\text{env}_{SV}\right>\rightarrow_{S}\text{env}_{S}^{\prime},\text{env}_{V}}\vspace*{-.4cm}$

Figure 5: Big-step semantics of statements in TinySol.

Most of the rules are straightforward. The rule LABEL:ts_bss_decv is used when
we declare a new variable $x$, with scope limited to the statement $S$; we
implicitly assume alpha-conversion to handle shadowing of an existing name. In
the premise, we evaluate the expression $e$ to a value $v$, and then execute
the statement $S$ with a variable environment $(x,v):\text{env}_{V}$, where we
have added the pair $(x,v)$. During the execution of $S$, this variable
environment may of course be updated (by applications of the rule
LABEL:ts_bss_assv), which may alter any value in the environment, including
$v$. However, outside of the scope of the declaration, $x$ is not visible and
so the pair $(x,v^{\prime})$ is removed from the environment once $S$
finishes. By contrast, any other change made to $\text{env}_{V}^{\prime}$ (as
well as any change made to the global state $\text{env}_{S}$) is retained.

The LABEL:ts_bss_call rule is the most complicated, because we need to perform
a number of actions. Some of them are obvious (e.g., evaluate the address and
the parameters $e_{1}$, $\widetilde{e}$ and $e_{2}$, relatively to the current
execution environment $\text{env}_{SV}$; use the obtained address $Y$ of the
callee to retrieve the field environment $\text{env}_{F}^{Y}$ for this
contract and, through the method table, to extract the list of formal
parameters $\widetilde{x}$ and the body of the method $S$; and check that the
number of actual parameters is the same as the number of formal parameters).
Then, we also have to check that the balance of the caller is at least $n$,
and, in that case, update the state environment by subtracting $n$ from the
balance of $X$ and adding $n$ to the balance of $Y$, in their respective field
environments; this yields a new state $\text{env}_{S}^{\prime\prime}$, where
we write $\text{env}_{F}[\texttt{balance -= }n]$ and
$\text{env}_{F}^{\prime}[\texttt{balance += }n]$ for these two operations.
Finally, we create the new execution environment by creating new bindings for
the special variables this, sender and value, and by binding the formal
parameters $\widetilde{x}$ to the values of the actual parameters
$\widetilde{v}$ in $\text{env}_{V}^{\prime\prime}$. Then we execute the
statement $S$ in this new environment. This yields the new state
$\text{env}_{S}^{\prime}$, and also an updated variable environment
$\text{env}_{V}^{\prime}$, since $S$ may have modified the bindings in
$\text{env}_{V}^{\prime\prime}$. However, these bindings are local to the
method, and therefore we throw them away once the call finishes. So, the
result of this transition is the updated state $\text{env}_{S}^{\prime}$ and
the original variable environment of the caller $\text{env}_{V}$.

It should be noted that a _local_ method call, i.e. a call to a method within
the same (calling) contract, is merely a special case of the rule
LABEL:ts_bss_call. Such a call would have the form this.$f(\widetilde{e})$:0,
since transferring any amount of currency will not alter the balance of the
contract. Thus, we could introduce some syntactic sugar, omitting both the
address and the value, and instead simply write $f(\widetilde{e})$.

[Genesis] $\dfrac{\left<DC,\text{env}_{ST}^{\emptyset}\right>\rightarrow_{DC}\text{env}_{ST}}{\left<\texttt{$DC$ $T$},\text{env}_{ST}^{\emptyset}\right>\rightarrow_{B}\left<T,\text{env}_{ST}\right>}\par$ [Trans] $\dfrac{\text{env}_{T}\vdash\left<\texttt{$X$.$f$($\widetilde{v}$):$n$},\text{env}_{S},(\texttt{this},A):\text{env}_{V}^{\emptyset}\right>\rightarrow_{S}\text{env}_{S}^{\prime},\text{env}_{V}}{\left<\texttt{$A$->$X$.$f$($\widetilde{v}$):$n$,$T$},\text{env}_{ST}\right>\rightarrow_{B}\left<T,\text{env}_{S}^{\prime},\text{env}_{T}\right>}$ |  [Revelation] $\dfrac{\phantom{P}}{\left<\epsilon,\text{env}_{ST}\right>\rightarrow_{B}\text{env}_{ST}}\vspace*{1.2cm}$
---|---
Figure 6: Semantics of blockchains.

####  2.2.4 Transactions and blockchains

The semantics for blockchains is given as a transition system defined by the
rules given in Figure 6. Here, the rule LABEL:ts_genesis describes the
‘genesis event’ where contracts are declared, whilst LABEL:ts_trans describes
a single transaction. This is thus a _small-step_ semantics, invoking the big-
step semantics for declarations and statements for its premises. We remark
that the rules of the operational semantics for blockchains (as well as those
for statements presented above) define a deterministic transition relation.

Note that, unlike in the original formulation of TinySol, we do not include a
rule like [Tx2] in [2] for rolling back a transaction in case it is non-
terminating or it aborts via a throw command. Such a rule would require a
premise that cannot be checked effectively for a Turing-complete language like
TinySol and therefore we omit it, since it is immaterial for the main
contributions we give in this paper.222For instance, rule [Tx2] in [2] has an
undecidable premise that checks whether the execution of the body of a
contract does _not_ yield a final state. It is debatable whether such rules
should appear in an operational semantics. In practice, termination of
Ethereum smart contracts is ensured via a ‘gas mechanism’ and is assumed by
techniques for the formal analysis of smart contracts. However, as observed
in, for instance, [10], proof of termination for smart contracts is non-
trivial even in the presence of a ‘gas mechanism.’ In the aforementioned
paper, the authors present the first mechanised proof of termination of
contracts written in EVM bytecode using minimal assumptions on the gas cost of
operations (see the study [28] for an empirical analysis of the effectiveness
of the ‘gas mechanism’ in estimating the computational cost of executing real-
life transactions). We leave for future work the addition of a ‘gas mechanism’
to TinySol and the adaption of the results we present in this paper to that
setting.

##  3 Call integrity and noninterference in TinySol

Grishchenko et al. [12] formulate the property of _call integrity_ for smart
contracts written in the language EVM, which is the ‘low-level’ bytecode of
the Ethereum platform, and the target language to which e.g. Solidity
compiles. They then prove [12, Theorem 1] that this property suffices for
ruling out reentrancy phenomena, as those described in the example in Figure
1. We first formulate a similar property for TinySol; this requires a few
preliminary definitions.

######  Definition 3.1 (Trace semantics).

A _trace_ of method invocations is given by

$\begin{array}[]{r @{~} c @{~} l}\pi\leavevmode\nobreak\
&::=\hfil\leavevmode\nobreak\ &\epsilon\leavevmode\nobreak\
\leavevmode\nobreak\ \big{|}\leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \texttt{$X$->$Y$.$f(\widetilde{v})$:$n$},\pi\end{array}$

where $X$ is the address of the calling contract, $Y$ is the address of the
called contract, $f$ is the method name, and $\widetilde{v}$ and $n$ are the
actual parameters.

We annotate the big-step semantics with a trace containing information on the
invoked methods to yield labeled transitions of the form
$\xrightarrow{\pi}_{S}$. To do this, we modify the rules in Table 2.2.3 as
follows:

  * •

in rules LABEL:ts_bss_skip, LABEL:ts_bss_whilefalse, LABEL:ts_bss_assv and
LABEL:ts_bss_assp, every occurrence of $\ \rightarrow_{S}\ $ becomes $\
\xrightarrow{\epsilon}_{S}\ $;

  * •

in rules LABEL:ts_bss_if and LABEL:ts_bss_decv, every occurrence of $\
\rightarrow_{S}\ $ becomes $\ \xrightarrow{\pi}_{S}\ $;

  * •

rules LABEL:ts_bss_seq, LABEL:ts_bss_whiletrue and LABEL:ts_bss_call
respectively become:

$\begin{array}[]{l}\dfrac{\begin{array}[]{r @{~} l}\leavevmode\nobreak\ &\\\
\text{env}_{T}\leavevmode\nobreak\
&\vdash\left<S_{1},\text{env}_{SV}\right>\xrightarrow{\pi_{1}}_{S}\text{env}_{SV}^{\prime\prime}\\\
\text{env}_{T}\leavevmode\nobreak\
&\vdash\left<S_{2},\text{env}_{SV}^{\prime\prime}\right>\xrightarrow{\pi_{2}}_{S}\text{env}_{SV}^{\prime}\end{array}}{\text{env}_{T}\vdash\left<\texttt{$S_{1}$;$S_{2}$},\text{env}_{SV}\right>\xrightarrow{\pi_{1},\pi_{2}}_{S}\text{env}_{SV}^{\prime}}\end{array}\begin{array}[]{l}\dfrac{\begin{array}[]{r
@{~} l}\text{env}_{SV}\leavevmode\nobreak\ &\vdash e\rightarrow_{e}\text{T}\\\
\text{env}_{T}\leavevmode\nobreak\
&\vdash\left<S,\text{env}_{SV}\right>\xrightarrow{\pi_{1}}_{S}\text{env}_{SV}^{\prime\prime}\\\
\text{env}_{T}\leavevmode\nobreak\ &\vdash\left<\texttt{while $e$ do
$S$},\text{env}_{SV}^{\prime\prime}\right>\xrightarrow{\pi_{2}}_{S}\text{env}_{SV}^{\prime}\end{array}}{\text{env}_{T}\vdash\left<\texttt{while
$e$ do
$S$},\text{env}_{SV}\right>\xrightarrow{\pi_{1},\pi_{2}}_{S}\text{env}_{SV}^{\prime}}\end{array}$

$\dfrac{\ldots\qquad\text{env}_{T}\vdash\left<S,\text{env}_{SV}^{\prime\prime}\right>\xrightarrow{\pi}_{S}\text{env}_{SV}^{\prime}}{\text{env}_{T}\vdash\left<\texttt{$e_{1}$.$f(\widetilde{e})$:$e_{2}$},\text{env}_{SV}\right>\xrightarrow{\texttt{$X$->$Y$.$f(\widetilde{v})$:$n$},\pi}_{S}\text{env}_{S}^{\prime},\text{env}_{V}}$

The full definition is given in Appendix A. We extend this annotation to the
semantics for blockchains and write $\xrightarrow{\pi}_{B}$ for this annotated
relation.

######  Definition 3.2 (Projection).

The _projection_ of a trace to a specific contract $X$, written
$\pi\downarrow_{X}$, is the trace of calls with $X$ as the calling address.
Formally: ϵ↓_X = ϵ ($Z$->$Y$.$f(\widetilde{v})$:$n$, π) ↓_X =
{$X$->$Y$.$f(\widetilde{v})$:$n$, (π↓X) if $Z=X$π↓Xotherwise

Notationally, given a (partial) function $f$, we write $f|_{X}$ for denoting
the restriction of $f$ to the subset $X$ of its domain.

######  Definition 3.3 (Call integrity).

Let $\mathcal{A}$ denote the set of all contracts (addresses),
$\mathcal{X}\subseteq\mathcal{A}$ denote a set of trusted contracts,
$\mathcal{Y}\overset{\Delta}{=}\mathcal{A}\mathbin{\backslash}\mathcal{X}$
denote all other contracts, and $\text{env}_{ST}^{\mathcal{X}}$ have domain
$\mathcal{X}$. A contract $C\in\mathcal{X}$ has _call integrity_ for
$\mathcal{Y}$ if, for every transaction $T$ and environments
$\text{env}_{ST}^{1}$ and $\text{env}_{ST}^{2}$ such that
$\text{env}_{ST}^{1}(X)|_{\mathcal{X}}=\text{env}_{ST}^{2}(X)|_{\mathcal{X}}=\text{env}_{ST}^{\mathcal{X}}$,
it holds that $\left<T,\text{env}_{ST}^{1}\right>$ $\xrightarrow{\pi_{1}}$_B
$\text{env}_{ST}$^1’ ∧$\left<T,\text{env}_{ST}^{2}\right>$
$\xrightarrow{\pi_{2}}$_B $\text{env}_{ST}$^2’ ⟹π_1 ↓_C = π_2 ↓_C

The definition is quite complicated and contains a number of elements:

  * •

$C$ is the contract of interest.

  * •

$\mathcal{X}$ is a set of _trusted_ contracts, which we assume are allowed to
influence the behaviour of $C$. This set must obviously contain $C$, since $C$
at least must be assumed to be trusted. Thus, a contract $C$ can have call
integrity for all contracts, if $\mathcal{X}=\left\\{\,C\,\right\\}$.

  * •

Conversely, the set $\mathcal{Y}=\mathcal{A}\mathbin{\backslash}\mathcal{X}$
is the set of addresses of all contracts that are _untrusted_.333Note that
this is formulated inversely by Grishchenko et al., who instead formulate the
property for a set of _untrusted_ contracts $\mathcal{A}_{\mathcal{C}}$,
corresponding to $\mathcal{Y}$ in the present formulation. However, using the
set of _trusted_ addresses $\mathcal{X}$ seems more straightforward.

  * •

$\text{env}_{ST}^{1}$ and $\text{env}_{ST}^{2}$ are any two pairs of
method/field environments that coincide (both in the code and in the values)
for all the trusted contracts.444This too is inversely formulated by
Grishchenko et al. The point is that the contracts in $\mathcal{X}$ are
assumed to be known, and hence invariant, whereas any contract in
$\mathcal{Y}$ is assumed to be unknown and may be controlled by an attacker.
Thus, we are actually quantifying over all possible contexts where the
contracts in $\mathcal{X}$ can be run.

  * •

$T$ is any transaction; it may be issued from any account and to any contract.
Thus we also quantify over all possible transactions, since an attacker may
request an arbitrary transaction, that is thus part of the execution context
as well.

Then, the call integrity property intuitively requires that, if we run the
trusted part of the code in any execution context, the behavior of $C$ remains
the same, i.e. $C$ must make exactly the same method calls (and in exactly the
same order). Thus, to _disprove_ that $C$ has call integrity, it suffices to
find two environments and a transaction that will induce a difference in the
call trace of $C$.

The idea in the property of call integrity is that the behaviour of $C$ should
not depend on any untrusted code (i.e. contracts in $\mathcal{Y}$), even if
control is transferred to a contract in $\mathcal{Y}$. The latter could for
example happen if $C$ calls a method on $B\in\mathcal{X}$, and $B$ then calls
a method on a contract in $\mathcal{Y}$. This also means that $C$ cannot
directly call any contract in $\mathcal{Y}$, since that can only happen if $C$
calls a method on a contract, where the address is received as a parameter, or
if it calls a method on a ‘hard-coded’ contract address. In both cases, we can
easily pick up two environments able to induce different behaviors, for
example by choosing a non-existing address for one context (in the first
case), or by ensuring that no contract exists on the hard-coded address in one
context (in the second case). The latter possibility can seem somewhat
contrived, especially if we assume that all contracts are created at the
genesis event, and it might therefore be reasonable to require also that
$\operatorname{dom}\left(\text{env}_{ST}^{1}\right)=\operatorname{dom}\left(\text{env}_{ST}^{2}\right)$,
such that we at least assume that contracts exist on the same addresses.
However, on an actual blockchain, new contracts can be deployed (and in some
cases also deleted) at any time, and if such a degree of realism is desired,
this extra constraint should not be imposed.

The main problem with the definition of call integrity is that it relies on a
universal quantification over all possible executions contexts. This makes it
hard to be checked in practice. However, our previous discussion indicates
that call integrity may intuitively be viewed as a form of _noninterference_
between the trusted and the untrusted contracts. We now see to what extent
this intuition is true and formally compare the two notions.

First of all, we consider a basic lattice of security levels, made up by just
two levels, namely $H$ (for _high_) and $L$ (for _low_), with $L<H$. We tag
every contract to be high or low through a contracts-to-levels mapping
$\lambda:\mathcal{A}\rightarrow\\{L,H\\}$; this induces a bipartition of the
contract names $\mathcal{A}$ into the following sets:

$\mathcal{L}=\left\\{\,X\in\mathcal{A}\;\mid\;\lambda(X)=L\,\right\\}\qquad\qquad\mathcal{H}=\left\\{\,X\in\mathcal{A}\;\mid\;\lambda(X)=H\,\right\\}$

In this way, we create a bipartition of the state into low and high,
corresponding to the fields of the low and of the high contracts,
respectively. Then, we define _low-equivalence_ $=_{L}$ to be the equivalence
on states such that $\text{env}_{S}^{1}=_{L}\text{env}_{S}^{2}$ if and only if
$\text{env}_{S}^{1}(X)=\text{env}_{S}^{2}(X)$, for every $X\in\mathcal{L}$.

We can now adapt the notion of noninterference for multi-threaded programs by
Smith and Volpano [24] to the setting of TinySol.

######  Definition 3.4 (Noninterference).

Given a contracts-to-levels mapping $\lambda:\mathcal{A}\rightarrow\\{L,H\\}$
and a contract environment $\text{env}_{T}$, the contracts satisfy
_noninterference_ if, for every $\text{env}_{S}^{1}$ and $\text{env}_{S}^{2}$
and for every transaction $T$ such that $\text{env}_{S}$^1 =_L
$\text{env}_{S}$^2 $\left<T,\text{env}_{S}^{1},\text{env}_{T}\right>$
$\rightarrow$_B $\text{env}_{S}$^1’,$\text{env}_{T}$
$\left<T,\text{env}_{S}^{2},\text{env}_{T}\right>$ $\rightarrow$_B
$\text{env}_{S}$^2’,$\text{env}_{T}$

it holds that $\text{env}_{S}^{1^{\prime}}=_{L}\text{env}_{S}^{2^{\prime}}$.

######  Remark 3.5 (Incomparability).

Call integrity and noninterference seem strongly related, in the sense that
the first requires that the behaviour of a contract is not influenced by the
(bad) execution context, whereas the second one requires that a part of the
computation (the ‘low’ one) is not influenced by the remainder context (the
‘high’ one). So, one may try to prove a statement like: “$C\in\mathcal{X}$ has
call integrity for
$\mathcal{Y}\overset{\Delta}{=}\mathcal{A}\mathbin{\backslash}\mathcal{X}$ if
and only if it satisfies noninterference w.r.t. $\lambda$ such that
$\mathcal{L}=\mathcal{X}$ and $\mathcal{H}=\mathcal{Y}$.” However, both
directions are false.

For the direction from right to left, consider:

⬇

1contract X { contract Y {

2 field balance = 0 field balance = v

3 go() { } go() { X.go():this.balance }

4} }

where X is trusted and Y untrusted. Since X cannot invoke any method, this
example satisfies call integrity. However, it does not satisfy
noninterference. To see this, consider two environments, one assigning 1 to
Y’s balance and the other one assigning 0, and the transaction Y->Y.go():0.

For the direction from left to right, consider the following:

⬇

1contract X { contract Y {

2 go() { field balance = v;

3 if Y.balance = 0 }

4 then Z.a():0

5 else Z.b():0 contract Z {

6 } a() { }

7} b() { }

8 }

Assuming that both X and Z are low, the example satisfies noninterference:
there is no way for Y to influence the low memory. By contrast, the code does
not satisfy call integrity. Indeed, let v be 0 in one environment and 1 in the
other, and consider $T$ to be X->X.go():0: in the first environment, it
generates X->Z.a():0, whereas in the second one it generates X->Z.b():0.

##  4 A type system for noninterference and call integrity

As demonstrated in Remark 3.5, call integrity and noninterference are
incomparable properties. This is so because noninterference is a 2-property on
the pair of _stores_
($\text{env}_{S}^{1^{\prime}},\text{env}_{S}^{2^{\prime}}$) resulting from two
different executions, whereas call integrity is a 2-property on the pair of
_call traces_ ($\pi_{1},\pi_{2}$) generated during two executions. However,
the two properties have an interesting overlap, because an outgoing currency
flow (i.e. a method call) may also result, at least potentially, in a change
of the stored values of the balance fields of the sender and recipient. Every
method call is therefore _also_ an information flow between the two, even when
no amount of currency is transferred. In [27], Volpano et al. devise a type
system for checking information flows, which, as they show, yields a sound
approximation to noninterference. In the following, we create an adaptation of
this type system to TinySol and show that it may _also_ be used to soundly
approximate call integrity.

###  4.1 Type syntax

We begin by assuming a finite lattice $(\mathcal{S},\sqsubseteq)$ consisting
of a set of _security levels_ $\mathcal{S}$, ranged over by $s$, and equipped
with a partial order $\sqsubseteq$. We write $s_{\bot}$, and $s_{\top}$ for
the least and largest elements in $\mathcal{S}$.

In the simplest setting, we can let
$\mathcal{S}\overset{\Delta}{=}\left\\{\,L,H\,\right\\}$ (for ‘low’ and
‘high’) and define $L\sqsubseteq L$, $L\sqsubseteq H$, and $H\sqsubseteq H$.
This is sufficient for ensuring bi-partite noninterference, but the type
system can also handle more fine-grained security control. With this, we can
define the types:

######  Definition 4.1.

We use the following language of types, where $I\in\text{TNames}$ is a _type
name_ (or ‘interface name’):

$\displaystyle B\in\mathcal{B}::=s\ |\ I_{s}\hskip 45.52458pt$ $\displaystyle
T\in\mathcal{T}::=B\ |\ var(B)\ |\ cmd(s)\ |\ proc(\widetilde{B})\texttt{:}s$
$\displaystyle\Gamma\in\mathcal{G}::=\mathcal{N}\rightharpoonup\mathcal{T}\cup\mathcal{G}\qquad$
$\displaystyle\mathcal{N}::=\text{ANames}\cup\text{FNames}\cup\text{VNames}\cup\text{MNames}\cup\text{TNames}$

We write $\widetilde{T}$ for a tuple of types $(T_{1},\ldots,T_{n})$.

Note that for the purpose of the type system, unless otherwise noted, we shall
assume that the four ‘magic names’ MVar are contained in the respective sets
of field and variable names; i.e. $\texttt{balance}\in\text{FNames}$ and
$\texttt{this},\texttt{sender},\texttt{value}\in\text{VNames}$.

The meaning of the types is as follows:

  * •

$\mathcal{B}$ is a set of _base types_ , which can either be a security level
$s$, or an interface name $I$, annotated with a security level, $I_{s}$.
Security levels are assigned to plain data, i.e. _values_ of type int or bool,
as well as _expressions_ yielding values of these types. The annotated
interface type is assigned to _addresses_ , as well as expressions yielding
addresses. In either case, the meaning of the type $s$ (resp. $I_{s}$), when
given to an expression $e$, is that all variables _read from_ within $e$, are
of level $s$ _or lower_.

Note that for the purpose of the present type system, we do not distinguish
between values of type int and bool, in the sense that we do not check whether
these type constraints are preserved. Instead, we shall just assume that all
programs are well-typed w.r.t. these simple type constraints, such that e.g.
expressions in the guards of if and while constructs indeed yield boolean
values. The present type system can easily be extended to incorporate such a
simple type check by extending the set of base types with annotated value
types ints and bools, similar to the annotated interface types.

  * •

$var(B)$ is a box type given to value _containers_ , i.e. variables and
fields. It denotes that the container can store data of type $B$. In the case
of $var(s)$, it denotes that the box can store data of level $s$ _or lower_ ,
whereas in the case of $var(I_{s})$ it additionally denotes that the address
stored in the variable must be of type $I$.

  * •

$cmd(s)$ is a _phrase type_ given to _code_ , i.e. commands $S$. It denotes
that all _assignments_ in the code are made to variables whose security level
is $s$ _or higher_.

  * •

$proc(\widetilde{B})\texttt{:}s$ is a procedure type given to methods
$f$($\widetilde{x}$) { $S$ }. It denotes that the body $S$ can be typed as
$cmd(s)$, under the assumption that the formal parameters $\widetilde{x}$ have
types $var(\widetilde{B})$. We shall discuss the types assigned to the ‘magic
variables’ this, sender and value below.

Note that every method declaration contains an implicit write to the balance
field of the containing contract: hence, given the meaning of $cmd(s)$, this
also means that the security level of balance must always be $s$ _or higher_
than the level of any method declared in an interface.

Finally, $\Gamma$ is a type environment, which is a partial function from
names to types _or type environments_. The latter possibility is included
because we shall represent each contract declaration as its own type
environment, containing box types and procedure types for the fields and
methods of the contract, and pointed to by the corresponding interface name.
Thus, if a contract has address $X$, then $\Gamma(X)=I_{s}$ for some interface
name $I$ and security level $s$, and $\Gamma(I)=\Gamma_{I}$, where
$\Gamma_{I}$ is a type environment containing the signatures of the methods
and fields of the contract. We shall use the following simple interface
declaration language for the interfaces of contracts:

$\begin{array}[]{r @{~} c @{~} l}IC\leavevmode\nobreak\
&::=\hfil\leavevmode\nobreak\ &\epsilon\leavevmode\nobreak\
\leavevmode\nobreak\ \big{|}\leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \texttt{interface $I$ \\{ $IF$ $IM$ \\} $IC$}\\\
IF\leavevmode\nobreak\ &::=\hfil\leavevmode\nobreak\
&\epsilon\leavevmode\nobreak\ \leavevmode\nobreak\ \big{|}\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \texttt{field $p$
:\leavevmode\nobreak\ $var(B)$; $IF$}\\\ IM\leavevmode\nobreak\
&::=\hfil\leavevmode\nobreak\ &\epsilon\leavevmode\nobreak\
\leavevmode\nobreak\ \big{|}\leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \texttt{method $f$ :\leavevmode\nobreak\
$proc(B)\texttt{:}s$; $IM$}\end{array}$

mirroring the syntax of contract declarations.

We require that all interface declarations be _well-formed_ in the sense that
they must at least contain a declaration for the mandatory members, i.e. the
balance field and the send() method. This ensures that we can define a minimal
interface declaration called $I^{\top}$, such that every well-formed interface
declaration is a specialisation of $I^{\top}$. This minimal interface contains
just the signatures of the mandatory balance field and of the send() method;
i.e.

⬇

1interface $I^{\top}$ {

2 field balance : $var(s_{\top})$;

3 method send : $proc()\texttt{:}s_{\bot}$;

4}

in the aforementioned interface declaration syntax.

Intuitively, this definition ensures that, for any valid interface definition
$I$ (containing at least balance and send) and any security level annotation
$s$, it must hold that $I_{s}$ is a subtype of $I^{\top}_{s_{\top}}$, thus
always allowing us to type $I_{s}$ up to $I^{\top}_{s_{\top}}$. In the
following section, we shall give a definition of a subtyping relation that
will ensure that this indeed is the case.

The inclusion of a contract ‘supertype’ $I^{\top}_{s_{\top}}$ is similar to
what is done in the type system developed for Featherweight Solidity by Crafa
et al. in [6]. This is necessary to enable us to give a type to the ‘magic
variable’ sender, which is available within the body of every method, since
this variable can be bound to the address of any contract or account. We shall
assume that $I^{\top}\in\operatorname{dom}\left(\Gamma\right)$ for any
$\Gamma$ we shall consider.

We shall also use a _typed_ syntax of TinySol, where local variables are now
declared as

$var(B)$ $x$ := $e$

where $B$ is the type of the value of the expression $e$. Likewise, we add
annotated type names $I_{s}$ to contract declarations thus:

contract $X$ : $I_{s}$ { $DF$; $DM$ }

where $I$ is a declared type name. Note that the security level is given on
the _contract_ , rather than on the interface. This is intentional, since
multiple contracts may implement the same interface but nevertheless be
categorised into different security levels. For the sake of simplicity, we
shall omit the explicit definition of interfaces in the code and merely assume
that an interface declaration $\Gamma_{I}$ with an associated name $I$ is
provided for each contract.

###  4.2 Subtyping

We shall introduce a parametrised subtyping relation
$\Gamma\vdash\cdot\mathrel{<:}\cdot$ on types. For each choice of $\Gamma$, we
define it as the least preorder satisfying the rules given in Figure 7. The
parameter $\Gamma$ is needed to handle subtyping for interface names $I$ in
rule LABEL:subs-name. Note that by this rule we have, for each well-formed
interface $I_{s}$ (with security level $s$ and interface name $I$) declared in
$\Gamma$, that $\Gamma\vdash I_{s}\mathrel{<:}I^{\top}_{s_{\top}}$ as
expected. Also note that we write
$\Gamma\vdash\widetilde{B}_{1}\mathrel{<:}\widetilde{B}_{2}$ to mean
$\Gamma\vdash B^{i}_{1}\mathrel{<:}B^{i}_{2}$ for each $i$ ($1\leq i\leq n$,
where $|\widetilde{B}_{1}|=n=|\widetilde{B}_{2}|$).

  [subs-name] $\dfrac{\Gamma\vdash\Gamma(I^{1})\mathrel{<:}\Gamma(I^{2})}{\Gamma\vdash I^{1}_{s^{1}}\mathrel{<:}I^{2}_{s^{2}}}\;\left(s_{1}\sqsubseteq s_{2}\right)\par$ [subs-sec] $\dfrac{\phantom{P}}{\Gamma\vdash s_{1}\mathrel{<:}s_{2}}\;\left(s_{1}\sqsubseteq s_{2}\right)\par$ [subs-var] $\dfrac{\Gamma\vdash B_{1}\mathrel{<:}B_{2}}{\Gamma\vdash var(B_{1})\mathrel{<:}var(B_{2})}\par$ |  [subs-env] $\dfrac{\begin{array}[]{l}\forall n\in\operatorname{dom}\left(\Gamma_{2}\right)\mathrel{.}\\\ \quad\Gamma_{1}(n)\mathrel{<:}\Gamma_{2}(n)\end{array}}{\Gamma\vdash\Gamma_{1}\mathrel{<:}\Gamma_{2}}\;\left(\operatorname{dom}\left(\Gamma_{2}\right)\subseteq\operatorname{dom}\left(\Gamma_{1}\right)\right)\par$ [subs-cmd] $\dfrac{\phantom{P}}{\Gamma\vdash cmd(s_{1})\mathrel{<:}cmd(s_{2})}\;\left(s_{2}\sqsubseteq s_{1}\right)\par$ [subs-proc] $\dfrac{\Gamma\vdash\widetilde{B}_{1}\mathrel{<:}\widetilde{B}_{2}}{\Gamma\vdash proc(\widetilde{B}_{1})\texttt{:}s_{1}\mathrel{<:}proc(\widetilde{B}_{2})\texttt{:}s_{2}}\;\left(s_{2}\sqsubseteq s_{1}\right)\par$
---|---
Figure 7: Subtyping rules.

By rule LABEL:subs-sec, subtyping is covariant in the types of _data_ , i.e.
the security level $s$, and likewise, the box type constructor $var(B)$ is
covariant by rule LABEL:subs-var. On the other hand, the type constructor for
commands, $cmd(s)$, is _contravariant_ by rule LABEL:subs-cmd. Lastly, the
type constructor for methods, $proc(\widetilde{B})\texttt{:}s$, is covariant
in the input parameters $\widetilde{B}$ by rule LABEL:subs-proc, but
contravariant in the ‘return’ type $s$, which indicates the level of the
underlying command type. These variances are consistent with the intended
meaning of the types:

  * •

A box of type $var(B)$ can store something of $B$ or lower (where $B$ is
either $s$ or $I_{s}$). Hence, if $\Gamma\vdash B_{1}\mathrel{<:}B_{2}$, then
a box type $var(B_{2})$ can safely be used wherever a box type $var(B_{1})$ is
needed.

  * •

A command of type $cmd(s)$ will assign to variables whose level is $s$ or
higher. Hence, if $s_{1}\sqsubseteq s_{2}$, then a command type $cmd(s_{1})$
can safely be used wherever a command type $cmd(s_{2})$ is needed.

  * •

A method of type $proc(\widetilde{B})\texttt{:}s$ expects parameters of types
$\widetilde{B}$ and promises that the method body will only assign to
variables that are level $s$ or higher. Hence, if
$\Gamma\vdash\widetilde{B}_{1}\mathrel{<:}\widetilde{B}_{2}$ and
$s_{2}\sqsubseteq s_{1}$, a command type
$proc(\widetilde{B}_{2})\texttt{:}s_{2}$ can safely be used wherever a command
type $proc(\widetilde{B}_{1})\texttt{:}s_{1}$ is needed. This is consistent
with the type for the body $S$ since, if $S$ can be typed to level
$cmd(s_{1})$, then it can also safely be typed to level $cmd(s_{2})$.

###  4.3 Type judgments

We can now give the rules for concluding type judgments, starting with the
type rules for declarations given in Figure 8.

[t-dec-c] | $\dfrac{\Gamma(X)=I_{s}\quad\Gamma_{1}=\Gamma,\texttt{this}:var(I_{s})\quad\Gamma\vdash DC\quad\Gamma_{1}\vdash DF\quad\Gamma_{1}\vdash DM}{\Gamma\vdash\texttt{contract $X$ : $I_{s}$ \\{ $DF$ $DM$ \\} $DC$}}\par\par$
---|---
[t-dec-f] | $\dfrac{\Gamma(\texttt{this})=var(I_{s})\quad p\in\operatorname{dom}\left(\Gamma(I)\right)\quad\Gamma\vdash DF}{\Gamma\vdash\texttt{field $p$ := $v$; $DF$}}\par$
[t-dec-m] | $\dfrac{\begin{array}[]{ll}\Gamma(\texttt{this})=var(I_{s_{1}})\quad\Gamma(I)(f)=proc(\widetilde{B})\texttt{:}s\\\ \Gamma_{1}=\Gamma,\widetilde{x}:var(\widetilde{B}),\texttt{value}:var(s),\texttt{sender}:var(I^{\top}_{s_{\top}})\\\ \Gamma\vdash\texttt{this.balance}:var(s)\quad\Gamma_{1}\vdash S:cmd(s)\quad\Gamma\vdash DM\end{array}}{\Gamma\vdash\texttt{$f(\widetilde{x})$ \\{ $S$ \\} $DM$}}\par\par\par$
Figure 8: Type rules for declarations.

Type judgments for contract declarations are of the form $\Gamma\vdash DC$,
stating that the declarations $DC$ are _well-typed_ w.r.t. the environment
$\Gamma$. This holds if the declarations are consistent with the type
information recorded in $\Gamma$, i.e. every field and method must have a
type, and the body of each method must be typable according to the assumptions
of the type. Note that the check here only ensures that every declared
contract member has a type; the converse check (i.e. that every declared type
in an interface also has an implementation) should also be performed. However,
we shall omit this in the present treatment.

After the initial reduction step, all declarations are stored in the two
environments $\text{env}_{ST}$, and further reductions also use the variable
environment $\text{env}_{V}$ for local variable declarations. Hence, we also
need to be able to conclude _agreement_ between these environments and
$\Gamma$. These rules are given in Figure 9, closely mirroring those of Figure
8. We omit the type rules for empty environments (since an empty environment
is always well-typed). As with declarations above, we also omit the rules for
ensuring that all declared types in an interface also have an implementation
in any contract claiming to implement that interface.

[t-env-t] | $\dfrac{\Gamma,\texttt{this}:\Gamma(X)\vdash\text{env}_{M}\quad\Gamma\vdash\text{env}_{T}}{\Gamma\vdash\text{env}_{T},(X,\text{env}_{M})}\par$
---|---
[t-env-m] | $\dfrac{\begin{array}[]{l}\Gamma(\texttt{this})=var(I_{s_{1}})\quad\Gamma(I)(f)=proc(\widetilde{B})\texttt{:}s\\\ \Gamma_{1}=\Gamma,\widetilde{x}:var(\widetilde{B}),\texttt{value}:var(s),\texttt{sender}:var(I^{\top}_{s_{\top}})\\\ \Gamma\vdash\text{env}_{M}\quad\Gamma\vdash\texttt{this.balance}:var(s)\quad\Gamma_{1}\vdash S:cmd(s)\end{array}}{\Gamma\vdash\text{env}_{M},(f,(\widetilde{x},S))}\par$
[t-env-s] | $\dfrac{\Gamma,\texttt{this}:\Gamma(X)\vdash\text{env}_{F}\quad\Gamma\vdash\text{env}_{S}}{\Gamma\vdash\text{env}_{S},(X,\text{env}_{F})}\par$
[t-env-f] | $\dfrac{\Gamma(\texttt{this})=var(I_{s})\quad p\in\operatorname{dom}\left(\Gamma(I)\right)\quad\Gamma\vdash\text{env}_{F}}{\Gamma\vdash\text{env}_{F},(p,v)}\par$
[t-env-v] | $\dfrac{\Gamma\vdash\text{env}_{V}}{\Gamma\vdash\text{env}_{V},(x,v)}\;\left(x\in\operatorname{dom}\left(\Gamma\right)\right)$
Figure 9: Type rules for environment agreement.

Next, we consider the type rules for statements appearing in the body of
method declarations; they are given in Figure 4.3. Here, judgments are of the
form $\Gamma\vdash S:cmd(s)$, indicating that $s$ is the _lowest_ level of any
variable written to within $S$. This is derived from the types of the
variables occurring in $S$, i.e. the types $var(B)$. However, as $B$ can be
either $s$ or $I_{s}$, we need a way to extract just the security level and
drop the interface name. For this, we write $B\leadsto s$, defined in the
obvious way: s ↝s I_s ↝s

This is used in the rules for assignments (rules LABEL:t-ass-v and
LABEL:t-ass-f). Note that in the rules LABEL:t-if and LABEL:t-loop, we know
(by our assumption that all contracts are well-typed w.r.t. simple type
preservation) that $e$ will evaluate to a boolean value, which therefore
necessarily will have a type $s$. Thus, we do not need the extra step of
$B\leadsto s$ here.

  [t-skip] $\dfrac{\phantom{P}}{\Gamma\vdash\texttt{skip}:cmd(s_{\top})}\par$ [t-throw] $\dfrac{\phantom{P}}{\Gamma\vdash\texttt{throw}:cmd(s_{\top})}\par$ [t-ass-v] $\dfrac{\begin{array}[]{l}\Gamma\vdash x:var(B)\\\ \Gamma\vdash e:B\end{array}}{\Gamma\vdash\texttt{$x$ := $e$}:cmd(s)}\;\left(B\leadsto s\right)\par$ [t-seq] $\dfrac{\begin{array}[]{l}\Gamma\vdash S_{1}:cmd(s)\\\ \Gamma\vdash S_{2}:cmd(s)\end{array}}{\Gamma\vdash\texttt{$S_{1}$; $S_{2}$}:cmd(s)}\par\par$ [t-loop] $\dfrac{\Gamma\vdash e:s\quad\Gamma\vdash S:cmd(s)}{\Gamma\vdash\texttt{while $e$ do $S$}:cmd(s)}\par$ |
---|---

Figure 10: Type rules for statements.

All rules are straightforward, except for LABEL:t-call. According to the
semantics for call (cf. rule LABEL:ts_bss_call), every call includes an
implicit read and write of the balance field of the calling contract, since
the call will only be performed if the value of $e_{2}$ is less than, or equal
to, the value of balance (to ensure that the subtraction will not yield a
negative number). There is thus an implicit flow from this.balance to the body
$S$ of the method call, similar to the case for the guard expression $e$ in an
if-statement. Furthermore, there is an implicit write to the balance field of
the callee, and thus a flow of information from one field to the other. This
might initially seem like it would require both caller and callee to have the
same security level for their balance field. However, the levels _can_ differ,
since by subtyping we can coerce one up to match the level of the other. For
this reason, we have $\Gamma\vdash\texttt{this.balance}$ in the premise, to be
explicitly _concluded_ , rather than as a simple lookup. This enables calls
from a lower security level into a higher security level, but not the other
way around.

  [t-var] $\dfrac{\Gamma\vdash x:var(B)}{\Gamma\vdash x:B}\par$ [t-field] $\dfrac{\Gamma\vdash e.p:var(B)}{\Gamma\vdash e.p:B}\par\par$ [t-subs-e] $\dfrac{\Gamma\vdash e:B_{1}\quad\Gamma\vdash B_{1}\mathrel{<:}B_{2}}{\Gamma\vdash e:B_{2}}$ |  [t-val] $\dfrac{\phantom{P}}{\Gamma\vdash v:B}\;\left(B=\begin{cases}\Gamma(v)&\text{if $v\in\text{ANames}$}\\\ s&\text{otherwise}\end{cases}\right)\par$ [t-op] $\dfrac{\Gamma\vdash e_{1}:B_{1}\quad\ldots\quad\Gamma\vdash e_{n}:B_{n}}{\Gamma\vdash\operatorname{op}(e_{1},\ldots,e_{n}):s}\;\left(\begin{array}[]{l}B_{1}\leadsto s\\\ \vdots\\\ B_{n}\leadsto s\end{array}\right)\par$
---|---
Figure 11: Type rules for expressions

Next, we consider the type rules for expressions $e$, given in Figure 11.
Here, judgments are of the form $\Gamma\vdash e:B$. There are a few things to
note:

  * •

In rule LABEL:t-val, the type of a value $v$ can be chosen freely, if $v$ is a
value type, i.e. of type int or bool. This rule is a consequence of the fact
that there is no simple relationship between the datatype of a value and its
security level. The actual security level will then be determined by the type
of the variable (resp. field) to which it is assigned.

  * •

The rules LABEL:t-var and LABEL:t-field simply unwrap the type of the
contained value from the box type of the container. Note that here we assume
that $x$ also covers the ‘magic variable’ names this, sender and value, and
that $p$ also covers the field name balance.

  * •

Finally, in rule LABEL:t-op, we require that all arguments and the return
value must be typable to the same security level $s$. Note in particular that
we assume that _no_ operation is defined with an address _return_ type; i.e.
we do not allow any form of pointer arithmetic. Operations may be defined on
addresses for their _arguments_ , e.g. equality testing, but the return type
must be one of the other value types, which can be given a security level.
Thus, in the rule LABEL:t-op, we also need to extract the security level $s$
from the types of the argument expressions.

  [t-box-x] $\dfrac{\phantom{P}}{\Gamma\vdash x:var(B)}\;\left(\Gamma(x)=var(B)\right)\par$ [t-m-sub] $\dfrac{\begin{array}[]{l}\Gamma\vdash e.f:proc(\widetilde{B}_{1})\texttt{:}s_{1}\\\ \Gamma\vdash proc(\widetilde{B}_{1})\texttt{:}s_{1}\mathrel{<:}proc(\widetilde{B}_{2})\texttt{:}s_{2}\end{array}}{\Gamma\vdash e.f:proc(\widetilde{B}_{2})\texttt{:}s_{2}}$ |  [t-box-f] $\dfrac{\Gamma\vdash e:I_{s}}{\Gamma\vdash e.p:var(B)}\;\left(\begin{array}[]{l}\Gamma(I)(p)=var(B)\\\ B\leadsto s\end{array}\right)\par$ [t-meth] $\dfrac{\Gamma\vdash e:I_{s}}{\Gamma\vdash e.f:proc(\widetilde{B})\texttt{:}s}\;\left(\Gamma(I)(f)=proc(\widetilde{B})\texttt{:}s\right)\par$
---|---
Figure 12: Type rules for method, variable and field lookup.

Finally, we have the look-up rules for methods, variables and fields, given in
Figure 12.

  * •

In rule LABEL:t-box-x we assume that $x$ also covers the magic variable names
this, sender and value.

  * •

In rule LABEL:t-box-f we assume that $p$ also covers the special field name
balance. Furthermore, we require $e$ in $e.p$ to resolve to an _interface
name_ rather than variable; i.e. the expression must yield an address. This is
again warranted by our assumption that expressions are well-typed w.r.t.
simple type preservation.

  * •

The same is the case in rule LABEL:t-meth for method lookup $e.f$, which is
used in the premise of the rule LABEL:t-call.

In the lookup rules, the expression $e$ is an _object path_ , which must
resolve to an address. As we disallow operations $\operatorname{op}$ to return
addresses, the object paths form a proper subset of the set of expressions,
since they can only consist of variable lookups, field reads or addresses
given as pure values. Note that, in the rules LABEL:t-box-f and LABEL:t-meth,
we require that the object path $e$ must be typable as an interface with the
_same_ security level $s$ as the value (resp. method) that is being looked up.
This is necessary to ensure that values residing in a higher-level part of the
memory cannot affect values at lower levels, in this case by altering the
_path_ to the object being resolved.

###  4.4 Safety and soundness

As is the case for the type system proposed in [27], our type system does not
have a now-safety predicate in the usual sense, since (invariant) safety in
simple type systems is a 1-property, whereas noninterference is a hyper-
property (specifically, a 2-property). Instead, the meaning of ‘safety’ is
expressed directly in the meaning of the types. Specifically:

  * •

If an expression $e$ has type $B$ such that $B\leadsto s$, then it denotes
that all variables _read from_ in the evaluation of $e$ are of level $s$ or
_lower_ , i.e. no read-up.

  * •

If a statement $S$ has type $cmd(s)$, then it denotes that all variables
_written to_ in the execution of $S$ are of level $s$ or _higher_ , i.e. no
write-down.

Intuitively, the meaning of these two types together imply that information
from higher-level variables cannot flow into lower-level variables. For a
statement such as $x$ := $e$ to be well-typed, it must therefore be the case
that, if $\Gamma\vdash x:var(s_{1})$ and $\Gamma\vdash e:s_{2}$, then
$s_{2}\sqsubseteq s_{1}$. Since $s_{2}$ can be coerced up to $s_{1}$ through
subtyping to match the level of the variable, the statement itself can then be
typed as $cmd(s_{1})$. We shall prove that our type system indeed ensures
these properties in Theorems 4.5-4.7 below.

[eq-env-empty] | $\dfrac{\phantom{P}}{\Gamma\vdash\text{env}_{X}^{\emptyset}=_{s}\text{env}_{X}^{\emptyset}}\;\left(X\in\left\\{\,V,S,F,T,M\,\right\\}\right)\par$
---|---
[eq-envV] | $\dfrac{\Gamma\vdash\text{env}_{V}^{1}=_{s}\text{env}_{V}^{2}}{\Gamma\vdash\text{env}_{V}^{1},(x,v_{1})=_{s}\text{env}_{V}^{2},(x,v_{2})}\;\left(\begin{array}[]{l}\Gamma(x)=var(s^{\prime})\\\ s^{\prime}\sqsubseteq s\implies v_{1}=v_{2}\end{array}\right)\par$
[eq-envS] | $\dfrac{\Gamma\vdash\text{env}_{S}^{1}=_{s}\text{env}_{S}^{2}\quad\Gamma(\Gamma(X))\vdash\text{env}_{F}^{1}=_{s}\text{env}_{F}^{2}}{\Gamma\vdash\text{env}_{S}^{1},(X,\text{env}_{F}^{1})=_{s}\text{env}_{S}^{2},(X,\text{env}_{F}^{2})}\par$
[eq-envF] | $\dfrac{\Gamma\vdash\text{env}_{F}^{1}=_{s}\text{env}_{F}^{2}}{\Gamma\vdash\text{env}_{F}^{1},(p,v_{1})=_{s}\text{env}_{F}^{2},(p,v_{2})}\;\left(\begin{array}[]{l}\Gamma(p)=var(s^{\prime})\\\ s^{\prime}\sqsubseteq s\implies v_{1}=v_{2}\end{array}\right)\par$
[eq-envT] | $\dfrac{\Gamma\vdash\text{env}_{T}^{1}=_{s}\text{env}_{T}^{2}}{\Gamma\vdash\text{env}_{T}^{1},(X,\text{env}_{M}^{1})=_{s}\text{env}_{T}^{2},(X,\text{env}_{M}^{2})}\;\left(\begin{array}[]{l}\Gamma(X)=I_{s^{\prime}}\\\ s^{\prime}\sqsubseteq s\implies\text{env}_{M}^{1}=\text{env}_{M}^{2}\end{array}\right)\par$
[eq-envSV] | $\dfrac{\Gamma\vdash\text{env}_{S}^{1}=_{s}\text{env}_{S}^{2}\quad\Gamma\vdash\text{env}_{V}^{1}=_{s}\text{env}_{V}^{2}}{\Gamma\vdash\text{env}_{SV}^{1}=_{s}\text{env}_{SV}^{2}}\par$
[eq-envST] | $\dfrac{\Gamma\vdash\text{env}_{S}^{1}=_{s}\text{env}_{S}^{2}\quad\Gamma\vdash\text{env}_{T}^{1}=_{s}\text{env}_{T}^{2}}{\Gamma\vdash\text{env}_{ST}^{1}=_{s}\text{env}_{ST}^{2}}$
Figure 13: Rules for the $s$-parameterised equivalence relation.

Before proceeding, we need to define a way to express that two _states_ , i.e.
two collections of variable and field environments $\text{env}_{SV}$, are
_equal_ up to a certain security level $s$. This relation, written
$\Gamma\vdash\text{env}_{SV}^{1}=_{s}\text{env}_{SV}^{2}$, is given by the
rules in Figure 13. Note in particular that the definition implies that
$\text{env}_{SV}^{1}$ and $\text{env}_{SV}^{2}$ must have the same domain, and
this carries over to the inner environments $\text{env}_{F}$ inside
$\text{env}_{S}$. The above definition gives us the following obvious result,
which can be shown by induction on the rules of $=_{s}$:

######  Lemma 4.2 (Restriction).

If $\Gamma\vdash\text{env}_{SV}^{1}=_{s}\text{env}_{SV}^{2}$ and
$s^{\prime}\sqsubseteq s$, then
$\Gamma\vdash\text{env}_{SV}^{1}=_{s^{\prime}}\text{env}_{SV}^{2}$.

Given our annotation of security levels on interfaces as well, we also extend
the $=_{s}$ relation to method tables $\text{env}_{T}$, and finally to the
combined representation of state and code, i.e. $\text{env}_{ST}$.

Next, we need the standard lemmas for strengthening and weakening of the
variable environment:

######  Lemma 4.3 (Strengthening).

If
$\Gamma,x:var(B)\vdash(x,v_{1}):\text{env}_{V}^{1}=_{s}(x,v_{2}):\text{env}_{V}^{2}$
then also $\Gamma\vdash\text{env}_{V}^{1}=_{s}\text{env}_{V}^{2}$.

######  Lemma 4.4 (Weakening).

If $\Gamma\vdash\text{env}_{V}^{1}=_{s}\text{env}_{V}^{2}$ and
$x\notin\operatorname{dom}\left(\text{env}_{V}^{1}\right)$ and
$x\notin\operatorname{dom}\left(\text{env}_{V}^{2}\right)$, then also
$\Gamma,x:var(B)\vdash(x,v_{1}):\text{env}_{V}^{1}=_{s}(x,v_{2}):\text{env}_{V}^{2}$
for any $B,v,x$.

Both results can be shown by induction on the rules of $=_{s}$. Furthermore,
both of the lemmas can then be directly extended to
$\Gamma\vdash\text{env}_{SV}^{1}=_{s}\text{env}_{SV}^{2}$. With this, we can
now state the first of our main theorems:

######  Theorem 4.5 (Preservation).

Assume that $\Gamma\vdash S:cmd(s)$, $\Gamma\vdash\text{env}_{T}$,
$\Gamma\vdash\text{env}_{SV}$, and
$\text{env}_{T}\vdash\left<S,\text{env}_{SV}\right>\rightarrow\text{env}_{SV}^{\prime}$.
Then, $\Gamma\vdash\text{env}_{SV}=_{s^{\prime}}\text{env}_{SV}^{\prime}$ for
any $s^{\prime}$ such that $s\not\sqsubseteq s^{\prime}$.

The Preservation theorem assures us that the promise made by the type $cmd(s)$
is actually fulfilled. If $\Gamma\vdash S:cmd(s)$, then every variable or
field written to in $S$ will be of level $s$ _or higher_ ; hence every
variable or field of a level that is _strictly lower_ than, or incomparable
to, $s$ will be unaffected. Thus, the pre- and post-transition states will be
equal on all values stored in variables or fields of level $s^{\prime}$ or
lower, since they cannot have been changed during the execution of $S$. In
other words, what is shown to be ‘preserved’ in this theorem is the _values_
at levels lower than, or incomparable to, $s$.

Note that the theorem does not show preservation of _well-typedness_ for the
environments (as is otherwise usually required in preservation proofs for type
systems). Indeed, a result saying that also
$\Gamma\vdash\text{env}_{SV}^{\prime}$ would be pointless. As can be seen in
Figure 9, the type judgment $\Gamma\vdash\text{env}_{SV}$ only ensures that
every field and variable in $\text{env}_{SV}$ has _any_ type in $\Gamma$. The
_number_ of declared fields and variables cannot change between the pre- and
post-states of a transition (this is ensured by the rule LABEL:ts_bss_decv);
only the stored values can change, but there is no inherent relationship
between a value and its assigned security level.

Our next theorem assures us that the type of an expression is also in
accordance with the intended meaning, namely: if $\Gamma\vdash e:s$, then
every variable (or field) read from in $e$ will be of level $s$ or lower (i.e.
no read-down of values from a higher level). We express this by considering
two different states, $\text{env}_{SV}^{1}$ and $\text{env}_{SV}^{2}$, which
must agree on all values of level $s$ and lower. Evaluating $e$ w.r.t. either
of these states should then yield the same result.

######  Theorem 4.6 (Safety for expressions).

Assume that $\Gamma\vdash e:B$ where $B\leadsto s$,
$\Gamma\vdash\text{env}_{SV}^{1}$, $\Gamma\vdash\text{env}_{SV}^{2}$, and
$\Gamma\vdash\text{env}_{SV}^{1}=_{s}\text{env}_{SV}^{2}$. Then,
$\text{env}_{SV}^{1}\vdash e\rightarrow v$ and $\text{env}_{SV}^{2}\vdash
e\rightarrow v$.

Finally, we can use the preceding two theorems to show soundness for the type
system. The soundness theorem expresses that, if a statement $S$ is well-typed
_to any level_ $s_{1}$ and we execute $S$ with any two states
$\text{env}_{SV}^{1}$ and $\text{env}_{SV}^{2}$ that agree _up to any level_
$s_{2}$, then the resulting states $\text{env}_{SV}^{1^{\prime}}$ and
$\text{env}_{SV}^{2^{\prime}}$ will still agree on all values up to level
$s_{2}$. This ensures noninterference, since any difference in values of a
_higher_ level than $s_{2}$ cannot induce a difference in the computation of
values at any lower levels.

######  Theorem 4.7 (Soundness).

Assume that $\Gamma\vdash S:cmd(s_{1})$, $\Gamma\vdash\text{env}_{T}$,
$\Gamma\vdash\text{env}_{SV}^{1}$, $\Gamma\vdash\text{env}_{SV}^{2}$,
$\Gamma\vdash\text{env}_{SV}^{1}=_{s_{2}}\text{env}_{SV}^{2}$,
$\text{env}_{T}\vdash\left<S,\text{env}_{SV}^{1}\right>\rightarrow\text{env}_{SV}^{1^{\prime}}$,
and
$\text{env}_{T}\vdash\left<S,\text{env}_{SV}^{2}\right>\rightarrow\text{env}_{SV}^{2^{\prime}}$.
Then,
$\Gamma\vdash\text{env}_{SV}^{1^{\prime}}=_{s_{2}}\text{env}_{SV}^{2^{\prime}}$.

Theorem 4.7 corresponds to the soundness theorem proved by Volpano, Smith and
Irvine [27] for their While-like language. However, given the object-oriented
nature of TinySol, we can actually take this one step further and allow even
parts of the code to vary. Specifically, given two ‘method table’
environments, $\text{env}_{T}^{1}$ and $\text{env}_{T}^{2}$, we just require
that these two environments agree up to the same level $s_{2}$ to ensure
agreement of the resulting two states $\text{env}_{SV}^{1^{\prime}}$ and
$\text{env}_{SV}^{2^{\prime}}$. We state this in the following theorem:

######  Theorem 4.8 (Extended soundness).

Assume that $\Gamma\vdash S:cmd(s_{1})$, $\Gamma\vdash\text{env}_{T}^{1}$,
$\Gamma\vdash\text{env}_{T}^{2}$,
$\Gamma\vdash\text{env}_{T}^{1}=_{s_{2}}\text{env}_{T}^{2}$,
$\Gamma\vdash\text{env}_{SV}^{1}$, $\Gamma\vdash\text{env}_{SV}^{2}$,
$\Gamma\vdash\text{env}_{SV}^{1}=_{s_{2}}\text{env}_{SV}^{2}$,
$\text{env}_{T}^{1}\vdash\left<S,\text{env}_{SV}^{1}\right>\rightarrow\text{env}_{SV}^{1^{\prime}}$,
and
$\text{env}_{T}^{2}\vdash\left<S,\text{env}_{SV}^{2}\right>\rightarrow\text{env}_{SV}^{2^{\prime}}$.
Then,
$\Gamma\vdash\text{env}_{SV}^{1^{\prime}}=_{s_{2}}\text{env}_{SV}^{2^{\prime}}$.

###  4.5 Extending the type system to transactions

A transaction is nothing but a method call with real-valued parameters and
sender set to an _account_ address, which corresponds to a minimal
implementation of $I^{\top}$. Thus, the theorems from the preceding section
can easily be extended to transactions and blockchains.

A blockchain consists of a set of contract declarations $DC$, followed by a
list of transactions $\widetilde{T}$. Hence, we can conclude $\Gamma\vdash
DC\leavevmode\nobreak\ \widetilde{T}:cmd(s)$, if it holds that $\Gamma\vdash
DC$ and $\Gamma\vdash\widetilde{T}:cmd(s)$. The latter can be simply concluded
by the following rules:

  [t-empty] $\dfrac{\phantom{P}}{\Gamma\vdash\epsilon:cmd(s)}$ |  [t-trans] $\dfrac{\Gamma\vdash\texttt{$X$.$f$($\widetilde{v}$):$n$}:cmd(s)\quad\Gamma\vdash\widetilde{T}:cmd(s)}{\Gamma\vdash\texttt{$A$->$X$.$f$($\widetilde{v}$):$n$,$\widetilde{T}$}:cmd(s)}$
---|---

This gives us the following two results:

######  Lemma 4.9.

If $\Gamma\vdash DC$ and
$\left<DC,\text{env}_{ST}^{\emptyset}\right>\rightarrow\text{env}_{ST}$, then
$\Gamma\vdash\text{env}_{ST}$.

######  Lemma 4.10.

If
$\Gamma\vdash\texttt{$A$->$X$.$f$($\widetilde{v}$):$n$,$\widetilde{T}$}:cmd(s)$
and $\Gamma\vdash\text{env}_{ST}$ and

$\left<\texttt{$A$->$X$.$f$($\widetilde{v}$):$n$,$\widetilde{T}$},\text{env}_{ST}\right>\rightarrow\left<\widetilde{T},\text{env}_{S}^{\prime},\text{env}_{T}\right>$

then also $\Gamma\vdash\text{env}_{S}^{\prime},\text{env}_{T}$ and
$\Gamma\vdash\widetilde{T}$.

As the initial step (the ‘genesis event’) does nothing except transforming the
declaration $DC$ into the environment representation $\text{env}_{ST}$, the
first result is obvious, and as the rule LABEL:ts_trans just unwraps a
transaction step into a call to the corresponding method, the second result
follows directly from the Preservation theorem. This can then be generalised
in an obvious way to the whole transaction list. Likewise, the Safety and
Soundness theorems can be extended to transactions in the same manner.

###  4.6 Noninterference and call integrity

As immediately evident from Definition 3.4 and Theorem 4.7, well-typedness
ensures noninterference:

######  Corollary 4.11 (Noninterference).

Assume a set of security levels
$\mathcal{S}\overset{\Delta}{=}\left\\{\,L,H\,\right\\}$, with $L\sqsubseteq
L$, $L\sqsubseteq H$ and $H\sqsubseteq H$, and furthermore that
$\Gamma\vdash\widetilde{T}:cmd(s)$, $\Gamma\vdash\text{env}_{ST}^{1}$,
$\Gamma\vdash\text{env}_{ST}^{2}$,
$\Gamma\vdash\text{env}_{ST}^{1}=_{L}\text{env}_{ST}^{2}$,
$\left<\widetilde{T},\text{env}_{ST}^{1}\right>\rightarrow^{*}\text{env}_{ST}^{1^{\prime}}$,
and
$\left<\widetilde{T},\text{env}_{ST}^{2}\right>\rightarrow^{*}\text{env}_{ST}^{2^{\prime}}$.
Then,
$\Gamma\vdash\text{env}_{ST}^{1^{\prime}}=_{L}\text{env}_{ST}^{2^{\prime}}$,

From Corollary 4.11, we then obviously also have that
$\Gamma\vdash\text{env}_{S}^{1^{\prime}}=_{L}\text{env}_{S}^{2^{\prime}}$,
regardless of whether $s$ is $L$ or $H$. In particular, we can assign security
levels to entire contracts, as well as all their members. Thus, our type
system can be used to ensure noninterference according to Definition 3.4.

As we previously argued in Remark 3.5, noninterference and call integrity are
incomparable properties. However, as our next theorem shows, _well-typedness_
actually _also_ ensures call integrity. This is surprising, so before stating
the theorem, we should give some hints as to why this is the case.

The definition of call integrity (Definition 3.3) requires the execution of
any code in a contract $C$ to be unaffected by all contracts in an ‘untrusted
set’ $\mathcal{Y}$, regardless of whether parts of the code in $\mathcal{Y}$
execute before, meanwhile or after the code in $C$. This is expressed by a
quantification over all possible traces resulting from a change in
$\mathcal{Y}$, i.e. either in the code or in the values of the fields.
Regardless of any such change, it must hold that the sequence of method calls
originating from $C$ be the same.

Noninterference, on the other hand, says nothing about execution traces, but
only speaks of the correspondence between values residing in the memory before
and after the execution step. The two counter-examples used in Remark 3.5 made
use of this fact:

  * •

The first counter-example had $C$ be unable to perform any method calls at
all, thus obviously satisfying call integrity, but allowed different balance
values to be transferred into it from a ‘high’ context by means of a method
call, thereby violating noninterference. However, this situation is ruled out
by well-typedness, because well-typedness disallows _any_ method calls from a
‘high’ to a ‘low’ context, precisely because every method call may transfer
the value parameter along with each call.

  * •

The second counter-example had an if statement in $C$ (the ‘low’ context)
depend on a field value in a ‘high’ context. The two branches then perform two
different method calls, thus enabling a change of the ‘high’ context to induce
two different execution traces for $C$. Thus, the example satisfies
noninterference, because no value stored in memory is changed, but it
obviously does not satisfy call integrity. However, this situation is also
ruled out by well-typedness, because the rule LABEL:t-if does not allow the
boolean guard expression $e$ in a ‘low’ context to depend on a value from a
‘high’ context.

Thus, both of the two counter-examples would be rejected by the type system.
With a setting of $L$ for the ‘trusted’ segment and $H$ for the
‘untrusted’,555This counter-intuitive naming can perhaps best be thought of as
indicating our level of _distrust_ in a contract. no values or computations
performed in the untrusted segment can affect the values in the trusted
segment, _nor_ the value of any expression in this segment, nor can it even
perform a call into the trusted segment. On the other hand, the trusted
segment _can_ call out into the untrusted part, but such a call cannot then
reenter the trusted segment: it must return before any further calls from the
trusted segment can happen.

######  Theorem 4.12 (Well-typedness implies call integrity).

Let $\mathcal{S}\overset{\Delta}{=}\left\\{\,L,H\,\right\\}$ with
$L\sqsubseteq L$, $L\sqsubseteq H$ and $H\sqsubseteq H$. Fix the two sets of
addresses $\mathcal{X}$ and $\mathcal{Y}$ as in Definition 3.3, such that
$\mathcal{A}=\mathcal{X}\cup\mathcal{Y}$ and
$\mathcal{A}=\operatorname{dom}\left(\text{env}_{T}\right)$. Fix a type
assignment $\Gamma$ such that

  * •

$\forall X\in\mathcal{X}\mathrel{.}\Gamma(X)=I_{L}$ for some $I$ where

    * –

$\forall p\in\Gamma(I)\mathrel{.}\Gamma(I)(p)=var(B)$ where $B\leadsto L$, and

    * –

$\forall f\in\Gamma(I)\mathrel{.}\Gamma(I)(f)=proc(\widetilde{B})\texttt{:}L$
for any $\widetilde{B}$

  * •

and with the level $H$ given to all other interfaces, fields and methods.

Also assume that $\Gamma\vdash T:cmd(s)$, $\Gamma\vdash\text{env}_{ST}^{1}$,
$\Gamma\vdash\text{env}_{ST}^{2}$,
$\Gamma\vdash\text{env}_{ST}^{1}=_{L}\text{env}_{ST}^{2}$,
$\left<T,\text{env}_{ST}^{1}\right>\xrightarrow{\pi_{1}}\text{env}_{ST}^{1^{\prime}}$,
and
$\left<T,\text{env}_{ST}^{2}\right>\xrightarrow{\pi_{2}}\text{env}_{ST}^{2^{\prime}}$.
Then, $\pi_{1}\downarrow_{X}=\pi_{2}\downarrow_{X}$, for any
$X\in\mathcal{X}$.

Theorem 4.12 tells us that _every_ contract $X$ in the trusted segment
$\mathcal{X}$ has call integrity w.r.t. the untrusted segment $\mathcal{Y}$.
This is thus a stronger condition than that of Definition 3.3, which only
defines call integrity for a _single_ contract $C\in\mathcal{X}$, rather than
for the whole set. This means that our type system will reject cases where
e.g. $C$ calls another contract $Z\in\mathcal{X}$ and $Z$ calls send() methods
of different contracts, depending on a ‘high’ value. As send() is always
ensured to do nothing, such calls could never lead to $C$ being reentered, so
this would actually still be safe, even though $Z$ itself would not satisfy
call integrity. Thus, this is an example of what resides in the ‘slack’ of our
type system.

However, this situation seems rather contrived, since it depends specifically
on the send() method, which is always ensured to do nothing except returning.
For practical purposes, it would be strange to imagine a contract
$C\in\mathcal{X}$ having call integrity w.r.t. $\mathcal{Y}$, but _without_
the other contracts in $\mathcal{X}$ also satisfying call integrity w.r.t.
$\mathcal{Y}$. Thus, our type system seems to yield a reasonable approximation
to the property of call integrity.

##  5 Examples and limitations

Let us see a few examples of the application of the type system. To begin
with, consider the first counter-example in Remark 3.5, which should be ill-
typed by the type system. In the counter-example we say that X is Low and Y is
High, so we let them both implement the interface $I$<s> defined as follows:

⬇

1interface I<s> { contract X : I<L> { ... }

2 field balance : $var(s)$

3 method go : $proc()\texttt{:}s$ contract Y : I<H> { ... }

4}

where $I$<L> (resp. $I$<H>) is a shorthand for $I_{L}$ (resp. $I_{H}$) with
all occurrences of $s$ within the interface definition replaced by $L$ (resp.
$H$). A part of the failing typing derivation for the body of the method
Y.go() in the declaration of contract Y is:

$\dfrac{\dfrac{\dfrac{\Gamma(\texttt{this})=\texttt{I<H>}}{\Gamma\vdash\texttt{this}:\texttt{I<H>}}\qquad\begin{array}[]{l}\Gamma(\texttt{I<H>})(\texttt{balance})\\\
\quad=var(H)\end{array}}{\Gamma\vdash\texttt{this.balance}:var(H)}\qquad\dfrac{\dfrac{\Gamma(\texttt{X})=\texttt{I<L>}}{\Gamma\not\vdash\texttt{X}:\texttt{I<H>}}\qquad\begin{array}[]{l}\Gamma(\texttt{I<L>})(\texttt{go})\\\
\quad\neq
proc()\texttt{:}H\end{array}}{\Gamma\not\vdash\texttt{X.go}:proc()\texttt{:}H}}{\Gamma\not\vdash\texttt{X.go():this.balance}:cmd(H)}$
(1)

We have that $\Gamma\vdash\texttt{this.balance}:var(H)$ in contract Y, so in
order for the method declaration go() { X.go():this.balance } in Y to be well-
typed, the body of the method must be typable as $proc()\texttt{:}H$ by rule
LABEL:t-dec-m. However, as the derivation in (1) illustrates, this constraint
cannot be satisfied, because the lookup $\Gamma(\texttt{I<L>})(\texttt{go})$
yields $proc()\texttt{:}L$, but $proc()\texttt{:}H$ is needed, and this cannot
be obtained through subtyping, because the $proc(\widetilde{B})\texttt{:}s$
type constructor is contravariant in $s$.

The above example is simple, since the name X is ‘hard-coded’ directly in the
body of Y.go(), and therefore the type check fails already while checking the
contract definition. However, suppose X were instead received as a parameter.
Then the signature of the method Y.go would have to be method go :
$proc(\texttt{I<H>})\texttt{:}H$ instead, and the type check would then fail
at the call-site, if a Low address were passed. The following shows a part of
the failing typing derivation for the call Y.go(X):this.balance, where the
parameter X is assumed to implement the interface I<L> as before:

$\dfrac{\dfrac{\dfrac{\Gamma(\texttt{X})=\texttt{I<L>}}{\Gamma\vdash\texttt{X}:\texttt{I<L>}}\qquad\dfrac{\begin{array}[]{c}\\\
L\sqsubseteq H\end{array}\qquad\dfrac{\dfrac{L\sqsubseteq H}{\Gamma\vdash
L\mathrel{<:}H}}{\Gamma\vdash
var(L)\mathrel{<:}var(H)}\qquad\dfrac{H\not\sqsubseteq L}{\Gamma\not\vdash
proc()\texttt{:}L\mathrel{<:}proc()\texttt{:}H}}{\Gamma\not\vdash\texttt{I<L>}\mathrel{<:}\texttt{I<H>}}}{\Gamma\not\vdash\texttt{X}:\texttt{I<H>}}}{\Gamma\not\vdash\texttt{Y.go(X):this.balance}:cmd(H)}$
(2)

Here $\Gamma\vdash\texttt{Y.go}:proc(\texttt{I<H>})\texttt{:}H$ (not shown).
The method call expects a parameter of type I<H>, but I<L> cannot be coerced
up to I<H> through subtyping, because its definition of the method go() has
type $proc()\texttt{:}L$, as given in the code listing above, and
$\Gamma\not\vdash proc()\texttt{:}L\mathrel{<:}proc()\texttt{:}H$ due again to
contravariance of the type constructor. Thus we see that the type system
indeed prevents calls from High to Low, regardless of whether the Low address
is ‘hard-coded’ or passed as a parameter to a High method. However, the
aforementioned examples also illustrate a limitation of our type system
approach to ensuring call integrity: the entire blockchain must be checked,
i.e. both the contracts _and_ the transactions. This is necessary since the
type check can fail at the call-site of a method, as in the example shown in
(2), and the call-site of any method can be a transaction.

Next, we shall briefly consider two examples, reported by Grishchenko et al.
in [12], of Solidity contracts that are misclassified w.r.t. reentrancy by the
static analyser Oyente [15]; a false positive and a false negative example.

The false negative example relies on a misplaced update of a field value, just
as in the example in Figure 1 (page 1).666It also involves the presence of a
‘default function’, which is a special feature of Solidity. It is a
parameterless function that is implicitly invoked by send(), thus allowing the
recipient to execute code upon reception of a currency transfer. This feature
is not present in TinySol, yet we can achieve a similar effect by simply
allowing the mandatory send() method to have an arbitrary method body, rather
than just skip. This has no effect on the type system and associated proofs,
since the send() method is treated as any other method therein. Hence, this
situation is in principle the same as if the sender had invoked some other
method than send(), similarly to the example in Figure 1.  In this example,
suppose X were assigned the level $L$ and Y the level $H$. With a transaction
$A$->X.transfer(Y):$n$ (for any address $A$ and any amount of currency $n$),
the type system would then correctly reject this blockchain because of the
inherent flow from High to Low that is implicit in the call X.transfer(this)
issued by Y. The typing derivation would fail in a similar manner as the
situation depicted in (2).

The false positive example of Grishchenko et al. from [12] is also similar to
the example in Figure 1, but this time just with the assignment to the guard
variable correctly placed _before_ the method call (i.e. with lines 6 and 7
switched in Figure 1). This too would be rejected by our type system, since it
does not take the ordering of statements in sequential composition into
account (i.e. rule LABEL:t-seq). Thus, this example constitutes a false
positive for our type system as well, which is hardly surprising.

⬇

1contract X : IBankL { contract Y : IBankH {

2 field owner = A; field credit = 0;

3 transfer(recipient, amount) { deposit(owner) {

4 if this.sender = this.owner then this.credit = this.value;

5 recipient this.owner = owner

6 .deposit(this.sender):amount }

7 else skip ...

8 } }

9 ...

10}

Figure 14: A two-bank setup.

Finally, let us consider a true positive example. Figure 14 illustrates a part
of the code for two banks, which would allow users to store some of their
assets and also to transfer assets between them.777TinySol does not have a
‘mapping’ type such as in Solidity, so the setup here is limited to a single
user. We assume both banks implement the same interface IBank, but with
different security settings: X is $L$ and Y is $H$, meaning the latter is
untrusted. There is no callback from Y, so in this setup a blockchain with a
transaction A->X.transfer(Y,1):0 would actually be accepted by the type
system, because the Low values from X can safely be coerced up (via subtyping)
to match the setting of High on Y.

##  6 Related work

In light of the visibility and immutability of smart contracts, which makes it
hard to correct errors once they are deployed in the wild, it is not
surprising that there has been a substantial research effort within the formal
methods community on developing formal techniques to prove safety properties
of those programs—see, for instance, [25] for a survey. The literature on this
topic is already huge and the whole gamut of techniques from the field of
verification and validation has been adapted to the smart-contract setting.
For example, this includes contributions employing frameworks based on finite-
state machines to design and synthesise Ethereum smart contracts [16], a
variety of static analysis techniques and accompanying tools, such as those
presented in [8, 14, 22, 26], and deductive verification [4, 5, 20], amongst
others. The Dafny-based approach reported in [5] is able to model arbitrary
reentrancy in a setting with the ‘gas mechanism’, whereas [3] presents a way
to analyse safety properties of smart contracts exhibiting reentrancy in a
gas-free setting.

The study in [13] is close in spirit to ours in that it uses a sound type
system to guarantee the absence of information flows that violate integrity
policies in Solidity smart contracts. That work also presents a type verifier
and its prototype implementation within the K-framework [21], which is then
applied to analyse more than one hundred smart contracts. However, their
technique has not been related to call integrity, which, by contrast, is the
focus of our work. Thus, our contribution in the present paper complements
this work and serves to further highlight the utility and applicability of
secure-flow types in the smart-contract setting. However, there are also clear
differences between this aforementioned work and the present one. Most
notably, our type system uses a more refined subtyping relation, which also
handles subtyping of method and address types, whereas subtyping is not
defined for the former in [13], and the latter is not given a type altogether.
This gives us a more fine-grained control over the information flow, since it
allows us to assign different security levels to a contract and its members.
For example, a High contract might have certain Low methods, which hence would
not be callable from another High contract, whereas High methods would. This
is in line with standard object-oriented principles, e.g. Java-style
visibility modifiers.

Another approach to using a type system to ensure smart-contract safety in a
Solidity-like language is presented by Crafa et al. in [6]. This work is
indeed related to ours in that both are based on well-known typing principles
from object-oriented languages, especially subtyping for contract/address
types and the inclusion of a ‘default’ supertype for all contracts, similar to
our $I^{\top}$. However, the aim of [6] is rather different from ours, in that
the type system offered in that paper seeks to prevent _runtime errors_ that
do not stem from a negative account balance, e.g. those resulting from
attempts to access nonexistent members of a contract. Incidentally, such
runtime errors would _also_ be prevented by our type system (rules
LABEL:t-call and LABEL:t-field in particular), due to our use of ‘interfaces’
as address types, if the converse check (ensuring every declared type in an
interface has an implementation) were also performed. However, our focus has
been on checking the currency flow, rather than preventing runtime errors of
this kind.

The aforementioned paper [6] introduced Featherweight Solidity (FS). Like
TinySol, FS is a calculus that formalises the core features of Solidity and,
as mentioned above, it supports the static analysis of safety properties of
smart contracts via type systems. Therefore, the developments in the present
paper might conceivably have been carried out in FS instead of TinySol. Our
rationale for using TinySol is that it provided a very simple language that
was sufficient to express the property of call integrity, thus allowing us to
focus on the core of this property. Of course, ‘simplicity’ is a subjective
criterion and the choice of one language instead of another is often a matter
of preference and convenience. To our mind, TinySol is slightly simpler than
FS, which includes functionalities such as callback functions and revert
labels. Moreover, the big-step semantics of TinySol provided was more
convenient for the development of our type system than the small-step
semantics given for FS. Furthermore, unlike FS, TinySol also formalises the
semantics of blockchains. Having said so, TinySol and FS are quite similar and
it would be interesting to study their similarities in more detail. To this
end, in future work, we intend to carry out a formal comparison of these two
core languages and to see which adaptations to our type system are needed when
formulated for FS. In particular, we note that FS handles the possibility of
an explicit type conversion (type cast) of address to address payable by
augmenting the address type with type information about the contract to which
it refers. This distinction is not present in our version of TinySol, as we
require all contracts and accounts to have a default send() function, so all
addresses are in this sense ‘payable’. However, our type system does not
depend on the presence of a send() function, so this difference is not
important here.

##  7 Conclusion and future work

In this paper we studied two security properties, namely call integrity and
noninterference, in the setting of TinySol, a minimal calculus for Solidity
smart contracts. To this end, we rephrased the syntax of TinySol to emphasise
its object-oriented flavour, gave a new big-step operational semantics for
that language and used it to define call integrity and noninterference. Those
two properties have some similarities in their definition, in that they both
require that some part of a program is not influenced by the other part.
However, we showed that the two properties are actually incomparable.
Nevertheless, we provided a type system for noninterference and showed that
well-typed programs _also_ satisfy call integrity. Hence, programs that are
accepted by our type systems lie at the intersection between call integrity
and noninterference.

A challenging development of our work would be to prove whether the type
system exactly characterises the intersection of these two properties, or to
find another characterisation of this set of programs. Orthogonally, it would
be important to devise type inference algorithms for the present type system,
to be used in practical situations where the typing environment is hard to
guess. It would also be interesting to compare our typing-based proof method
with those proposed, e.g., in [12, 15, 22]. Finally, we also aim at applying
our static analysis methodology to many concrete case studies, to better
understand the benefits of using a completely static proof technique for call
integrity. To do so, it would be useful to extend TinySol with a ‘gas
mechanism’ allowing one to prove the termination of transactions and to
compute their computational cost.

A potential limitation of the approach presented in this paper is that the
entire blockchain must be checked to show call integrity of a contract.
Indeed, since a typing derivation can fail at the call-site and the call-site
of a method can be a transaction, transactions must be well-typed too. In
passing, we note that this kind of problem is also present in [24, 27] (and,
in general, in many works on type systems for security), where the whole code
needs to be typed in order to obtain the desired guarantees. We think that an
important avenue for future work, and one we intend to pursue, is to explore
whether, and to what extent, other typing disciplines can be employed to
mitigate this problem. As mentioned earlier, we also plan to extend the
language (and the type system) to enable checking of real-life Solidity
contracts; this will also allow us to better assess how (un)feasible it would
be to check the whole blockchain.

## References

  * [1] Nicola Atzei, Massimo Bartoletti, and Tiziana Cimoli.  A survey of attacks on ethereum smart contracts (sok).  In Proc. of POST, volume 10204 of LNCS, pages 164–186. Springer, 2017.  doi:10.1007/978-3-662-54455-6\\_8.
  * [2] Massimo Bartoletti, Letterio Galletta, and Maurizio Murgia.  A minimal core calculus for solidity contracts.  In Cristina Pérez-Solà, Guillermo Navarro-Arribas, Alex Biryukov, and Joaquin Garcia-Alfaro, editors, Data Privacy Management, Cryptocurrencies and Blockchain Technology, pages 233–243, Cham, 2019. Springer International Publishing.  doi:10.1007/978-3-030-31500-9\\_15.
  * [3] Christian Bräm, Marco Eilers, Peter Müller, Robin Sierra, and Alexander J. Summers.  Rich specifications for Ethereum smart contract verification.  Proc. ACM Program. Lang., 5(OOPSLA):1–30, 2021.  URL: https://doi.org/10.1145/3485523.
  * [4] Franck Cassez, Joanne Fuller, and Aditya Asgaonkar.  Formal verification of the Ethereum 2.0 Beacon Chain.  In 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 13243 of LNCS, pages 167–182. Springer, 2022.  URL: https://doi.org/10.1007/978-3-030-99524-9_9.
  * [5] Franck Cassez, Joanne Fuller, and Horacio Mijail Anton Quiles.  Deductive verification of smart contracts with Dafny.  In 27th International Conference on Formal Methods for Industrial Critical Systems, volume 13487 of LNCS, pages 50–66. Springer, 2022.  URL: https://doi.org/10.1007/978-3-031-15008-1_5.
  * [6] Silvia Crafa, Matteo Di Pirro, and Elena Zucca.  Is solidity solid enough?  In Financial Cryptography Workshops, 2019.
  * [7] The dao smart contract.  http://etherscan.io/address/0xbb9bc244d798123fde783fcc1c72d3bb8c189413#code, 2016\.
  * [8] Josselin Feist, Gustavo Grieco, and Alex Groce.  Slither: a static analysis framework for smart contracts.  In Proceedings of the 2nd International Workshop on Emerging Trends in Software Engineering for Blockchain, pages 8–15. IEEE / ACM, 2019\.  URL: https://doi.org/10.1109/WETSEB.2019.00008.
  * [9] Ethereum Foundation.  Solidity documentation.  https://docs.soliditylang.org/, 2022.  Accessed: 2024-01-15.
  * [10] Thomas Genet, Thomas P. Jensen, and Justine Sauvage.  Termination of Ethereum’s smart contracts.  In Proc. of the 17th International Joint Conference on e-Business and Telecommunications - Volume 2: SECRYPT, pages 39–51. ScitePress, 2020.  URL: https://doi.org/10.5220/0009564100390051.
  * [11] J. A. Goguen and J. Meseguer.  Security policies and security models.  In 1982 IEEE Symposium on Security and Privacy, pages 11–11, 1982\.  doi:10.1109/SP.1982.10014.
  * [12] Ilya Grishchenko, Matteo Maffei, and Clara Schneidewind.  A semantic framework for the security analysis of ethereum smart contracts.  In Lujo Bauer and Ralf Küsters, editors, Principles of Security and Trust, pages 243–269, Cham, 2018. Springer International Publishing.
  * [13] Xinwen Hu, Yi Zhuang, Shangwei Lin, Fuyuan Zhang, Shuanglong Kan, and Zining Cao.  A security type verifier for smart contracts.  Comput. Secur., 108:102343, 2021.  URL: https://doi.org/10.1016/j.cose.2021.102343.
  * [14] Sukrit Kalra, Seep Goel, Mohan Dhawan, and Subodh Sharma.  ZEUS: analyzing safety of smart contracts.  In 25th Annual Network and Distributed System Security Symposium. The Internet Society, 2018.  URL: https://www.ndss-symposium.org/wp-content/uploads/2018/02/ndss2018_09-1_Kalra_paper.pdf.
  * [15] Loi Luu, Duc-Hiep Chu, Hrishi Olickel, Prateek Saxena, and Aquinas Hobor.  Making smart contracts smarter.  In Proc. SIGSAC Conf. on Computer and Communications Security, page 254–269. ACM, 2016.  URL: https://doi.org/10.1145/2976749.2978309.
  * [16] Anastasia Mavridou and Aron Laszka.  Designing secure Ethereum smart contracts: A finite state machine based approach.  In 22nd Conference on Financial Cryptography and Data Security, volume 10957 of LNCS, pages 523–540. Springer, 2018.  URL: https://doi.org/10.1007/978-3-662-58387-6_28.
  * [17] Hanne Riis Nielson and Flemming Nielson.  Semantics with Applications: An Appetizer.  Springer-Verlag London, 2007.  doi:10.1007/978-1-84628-692-6.
  * [18] The parity wallet breach.  https://www.coindesk.com/30-million-ether-reported-stolen-parity-wallet-breach/, 2017\.
  * [19] The parity wallet vulnerability.  https://paritytech.io/blog/security-alert.html, 2017.
  * [20] Daejun Park, Yi Zhang, and Grigore Rosu.  End-to-end formal verification of Ethereum 2.0 Deposit Smart Contract.  In Shuvendu K. Lahiri and Chao Wang, editors, Computer Aided Verification - 32nd International Conference, CAV Proceedings, Part I, volume 12224 of Lecture Notes in Computer Science, pages 151–164. Springer, 2020.  URL: https://doi.org/10.1007/978-3-030-53288-8_8.
  * [21] Grigore Rosu and Traian-Florin Serbanuta.  An overview of the K semantic framework.  J. Log. Algebraic Methods Program., 79(6):397–434, 2010.  URL: https://doi.org/10.1016/j.jlap.2010.03.012.
  * [22] Clara Schneidewind, Ilya Grishchenko, Markus Scherer, and Matteo Maffei.  ethor: Practical and provably sound static analysis of ethereum smart contracts.  In Proc. of SIGSAC Conf. on Computer and Communications Security, pages 621–640. ACM, 2020.  URL: https://doi.org/10.1145/3372297.3417250.
  * [23] Pablo Lamela Seijas, Simon J. Thompson, and Darryl McAdams.  Scripting smart contracts for distributed ledger technology.  IACR Cryptol. ePrint Arch., 2016:1156, 2016.
  * [24] Geoffrey Smith and Dennis M. Volpano.  Secure information flow in a multi-threaded imperative language.  In Proc. of 25th POPL, pages 355–364. ACM, 1998.
  * [25] Palina Tolmach, Yi Li, Shang-Wei Lin, Yang Liu, and Zengxiang Li.  A survey of smart contract formal specification and verification.  ACM Computing Surveys (CSUR), 54(7):148:1–148:38, 2020.  URL: https://doi.org/10.1145/3464421.
  * [26] Petar Tsankov, Andrei Marian Dan, Dana Drachsler-Cohen, Arthur Gervais, Florian Bünzli, and Martin T. Vechev.  Securify: Practical security analysis of smart contracts.  In Proc. of SIGSAC Conference on Computer and Communications Security, pages 67–82. ACM, 2018.  URL: https://doi.org/10.1145/3243734.3243780.
  * [27] Dennis Volpano, Geoffrey Smith, and Cynthia Irvine.  A sound type system for secure flow analysis.  Journal of Computer Security, 4, 08 2000.  doi:10.3233/JCS-1996-42-304.
  * [28] Renlord Yang, Toby Murray, Paul Rimba, and Udaya Parampalli.  Empirically analyzing Ethereum’s gas mechanism.  In Proc. of IEEE European Symposium on Security and Privacy Workshops, pages 310–319. IEEE, 2019.  URL: https://doi.org/10.1109/EuroSPW.2019.00041.

##  Appendix A Trace semantics

A _trace_ of method invocations is given by

$\begin{array}[]{r @{~} c @{~} l}\pi\leavevmode\nobreak\
&::=\hfil\leavevmode\nobreak\ &\epsilon\leavevmode\nobreak\
\leavevmode\nobreak\ \big{|}\leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \texttt{$X$->$Y$.$f(\widetilde{v})$:$n$},\pi\end{array}$

where $X$ is the address of the calling contract, $Y$ is the address of the
called contract, $f$ is the method name, and $\widetilde{v}$ and $n$ are the
actual parameters. We annotate the big-step semantics of Figure 2.2.3 with a
trace containing information on the invoked methods to yield labeled
transitions of the form $\xrightarrow{\pi}$. The rules are as follows:

[BS-Skip] | $\dfrac{\phantom{P}}{\text{env}_{T}\vdash\left<\texttt{skip},\text{env}_{SV}\right>\xrightarrow{\epsilon}\text{env}_{SV}}\par$
---|---
[BS-Seq] |
[BS-If] |
[BS-Loop${}_{\text{T}}$] |
[BS-Loop${}_{\text{F}}$] | $\dfrac{\text{env}_{SV}\vdash e\rightarrow_{e}\text{F}}{\text{env}_{T}\vdash\left<\texttt{while $e$ do $S$},\text{env}_{SV}\right>\xrightarrow{\epsilon}\text{env}_{SV}}\par$
[BS-DecV] |
[BS-AssV] | $\dfrac{\text{env}_{SV}\vdash e\rightarrow_{e}v}{\text{env}_{T}\vdash\left<\texttt{$x$ := $e$},\text{env}_{SV}\right>\xrightarrow{\epsilon}\text{env}_{S},\text{env}_{V}\kern-2.0pt\left[x\mapsto v\right]}\;\left(x\in\operatorname{dom}\left(\text{env}_{V}\right)\right)\par$
[BS-AssF] | $\dfrac{\begin{array}[]{l}\text{env}_{V}(\texttt{this})=X\\\ \text{env}_{S}(X)=\text{env}_{F}\end{array}\quad\begin{array}[]{l}p\in\operatorname{dom}\left(\text{env}_{F}\right)\quad\text{env}_{SV}\vdash e\rightarrow_{e}v\end{array}{l}}{\text{env}_{T}\vdash\left<\texttt{this.$p$ := $e$},\text{env}_{SV}\right>\xrightarrow{\epsilon}\text{env}_{S}\kern-2.0pt\left[X\mapsto\text{env}_{F}\kern-2.0pt\left[p\mapsto v\right]\right],\text{env}_{V}}\par$
[BS-Call] | $\dfrac{\begin{array}[]{l}\text{env}_{SV}\vdash e_{1}\rightarrow_{e}Y\qquad\text{env}_{S}(Y)\leavevmode\nobreak\ =\text{env}_{F}^{Y}\qquad(\text{env}_{T}(Y))(f)\leavevmode\nobreak\ =(\widetilde{x},S)\\\ |\widetilde{x}|\leavevmode\nobreak\ =|\widetilde{e}|=k\qquad\qquad\\!\text{env}_{SV}\vdash\widetilde{e}\rightarrow_{e}\widetilde{v}\qquad\ \ \ \text{env}_{SV}\vdash e_{2}\rightarrow_{e}n\\\ \text{env}_{V}(\texttt{this})\leavevmode\nobreak\ =X\qquad\text{env}_{S}(X)\leavevmode\nobreak\ =\text{env}_{F}^{X}\qquad n\leavevmode\nobreak\ \leq\text{env}_{F}^{X}(\texttt{balance})\\\ \text{env}_{S}^{\prime\prime}\leavevmode\nobreak\ =\text{env}_{S}\kern-2.0pt\left[X\mapsto\text{env}_{F}^{X}[\texttt{balance -= }n]\right]\kern-2.0pt\left[Y\mapsto\text{env}_{F}^{Y}[\texttt{balance += }n]\right]\\\ \text{env}_{V}^{\prime\prime}\leavevmode\nobreak\ =(\texttt{this},Y):(\texttt{sender},X):(\texttt{value},n):(x_{1},v_{1}):\ldots:(x_{k},v_{k}):\text{env}_{V}^{\emptyset}\\\ \text{env}_{T}\vdash\left<S,\text{env}_{SV}^{\prime\prime}\right>\xrightarrow{\pi}\text{env}_{SV}^{\prime}\end{array}}{\text{env}_{T}\vdash\left<\texttt{$e_{1}$.$f(\widetilde{e})$:$e_{2}$},\text{env}_{SV}\right>\xrightarrow{\texttt{$X$->$Y$.$f(\widetilde{v})$:$n$},\pi}\text{env}_{S}^{\prime},\text{env}_{V}}$

##  Appendix B Proof of Theorem 4.5

######  Proof B.1.

By induction on the derivation of $\Gamma\vdash S:cmd(s)$.

  * •

If LABEL:t-skip was used to conclude the judgment $\Gamma\vdash S:cmd(s)$,
then $S$ = skip. Then the result is immediate, since skip does not affect
$\text{env}_{SV}$.

  * •

If LABEL:t-throw was used to conclude the judgment $\Gamma\vdash S:cmd(s)$,
then $S$ = throw. The statement then holds vacuously, since
$\text{env}_{T}\vdash\left<\texttt{throw},\text{env}_{SV}\right>\not\rightarrow$.

  * •

If LABEL:t-decvar was used to conclude the judgment $\Gamma\vdash S:cmd(s)$,
then $S$ = $var(B)$ $x$ := $e$ in $S^{\prime}$, and from the premise we know
that $\Gamma,x:var(B)\vdash S^{\prime}:cmd(s)$. By LABEL:ts_bss_decv we have
that

$\text{env}_{T}\vdash\left<\texttt{$var(B)$ $x$ := $e$ in
$S^{\prime}$},\text{env}_{SV}\right>\rightarrow\text{env}_{SV}^{\prime}$

where $x\notin\operatorname{dom}\left(\text{env}_{V}^{\prime}\right)$. From
the premise, we know that

$\displaystyle\text{env}_{SV}$ $\displaystyle\vdash e\rightarrow v$
$\displaystyle\text{env}_{T}$
$\displaystyle\vdash\left<S^{\prime},\text{env}_{S},(x,v):\text{env}_{V}\right>\rightarrow\text{env}_{S}^{\prime},(x,v^{\prime}):\text{env}_{V}^{\prime}$

We can then apply the induction hypothesis to conclude that

$\Gamma,x:var(B)\vdash\text{env}_{S},(x,v):\text{env}_{V}=_{s^{\prime}}\text{env}_{S}^{\prime},(x,v^{\prime}):\text{env}_{V}^{\prime}$

By Lemma 4.3 we can then conclude
$\Gamma\vdash\text{env}_{SV}=_{s^{\prime}}\text{env}_{SV}^{\prime}$ as
required.

  * •

If LABEL:t-ass-v was used, then $S$ = $x$ := $e$. From the premise, we know
that $\Gamma\vdash x:var(s)$ and $\Gamma\vdash e:s$. By LABEL:ts_bss_assv, we
know that

$\text{env}_{T}\vdash\left<\texttt{$x$ :=
$e$},\text{env}_{SV}\right>\rightarrow\text{env}_{S},\text{env}_{V}\kern-2.0pt\left[x\mapsto
v\right]$

where $\text{env}_{SV}\vdash e\rightarrow v$ from the premise. As $s^{\prime}$
is strictly lower than $s$, we therefore conclude
$\Gamma\vdash\text{env}_{SV}=_{s^{\prime}}\text{env}_{S},\text{env}_{V}\kern-2.0pt\left[x\mapsto
v\right]$.

  * •

If LABEL:t-ass-f was used, then $S$ = this.$p$ := $e$. The argument is then
the same as above, except that it is $\text{env}_{S}$, rather than
$\text{env}_{V}$ that is updated.

  * •

If LABEL:t-seq was used, then $S$ = $S_{1}$; $S_{2}$. From the premise, we
know that $\Gamma\vdash S_{1}:cmd(s)$ and $\Gamma\vdash S_{2}:cmd(s)$. By
LABEL:ts_bss_seq we know that

$\text{env}_{T}\vdash\left<S_{1};S_{2},\text{env}_{SV}\right>\rightarrow\text{env}_{SV}^{\prime}$

and from the premise that

$\displaystyle\text{env}_{T}$
$\displaystyle\vdash\left<S_{1},\text{env}_{SV}\right>\rightarrow\text{env}_{SV}^{\prime\prime}$
$\displaystyle\text{env}_{T}$
$\displaystyle\vdash\left<S_{2},\text{env}_{SV}^{\prime\prime}\right>\rightarrow\text{env}_{SV}^{\prime}$

By twice application of the induction hypothesis, the statement holds for both
premises, so we conclude that

$\displaystyle\Gamma$
$\displaystyle\vdash\text{env}_{SV}=_{s^{\prime}}\text{env}_{SV}^{\prime\prime}$
$\displaystyle\Gamma$
$\displaystyle\vdash\text{env}_{SV}^{\prime\prime}=_{s^{\prime}}\text{env}_{SV}^{\prime}$

as required.

  * •

If LABEL:t-if was used, then $S$ = if $e$ then $S_{\text{T}}$ else
$S_{\text{F}}$. From the premise, we know that $\Gamma\vdash
S_{\text{T}}:cmd(s)$ and $\Gamma\vdash S_{\text{F}}:cmd(s)$. By
LABEL:ts_bss_if we know that

$\text{env}_{T}\vdash\left<\texttt{if $e$ then $S_{\text{T}}$ else
$S_{\text{F}}$},\text{env}_{SV}\right>\rightarrow\text{env}_{SV}^{\prime}$

and from the premise that
$\text{env}_{T}\vdash\left<S_{b},\text{env}_{SV}\right>\rightarrow\text{env}_{SV}^{\prime}$
where $b\in\left\\{\,\text{T},\text{F}\,\right\\}$ depending on the evaluation
value of $e$. Regardless of which branch was chosen, the statement then holds
by the induction hypothesis.

  * •

If LABEL:t-loop was used, then $S$ = while $e$ do $S^{\prime}$, and from the
premise we know that $\Gamma\vdash S^{\prime}:cmd(s)$. We now have two cases,
depending on the value of $e$:

    1. 1.

If $e$ evaluates to F, then the transition is concluded by
LABEL:ts_bss_whilefalse. The result is the immediate, since $\text{env}_{SV}$
is not modified.

    2. 2.

If $e$ evaluates to T, then the transition is concluded by
LABEL:ts_bss_whiletrue. From the premise, we know that

$\displaystyle\text{env}_{T}$
$\displaystyle\vdash\left<S^{\prime},\text{env}_{SV}\right>\rightarrow\text{env}_{SV}^{\prime\prime}$
$\displaystyle\text{env}_{T}$ $\displaystyle\vdash\left<\texttt{while $e$ do
$S^{\prime}$},\text{env}_{SV}^{\prime\prime}\right>\rightarrow\text{env}_{SV}^{\prime}$

As we know the loop will terminate, the statement then holds by twice
application of the induction hypothesis.

  * •

If LABEL:t-call was used, then $S$ = $e_{1}$.$f(\widetilde{e})$ : $e_{2}$, and
from the premise we know that

$\displaystyle\Gamma$ $\displaystyle\vdash
e_{1}.f:proc(\widetilde{B})\texttt{:}s$ $\displaystyle\Gamma$
$\displaystyle\vdash\texttt{this.balance}:var(s)$ $\displaystyle\Gamma$
$\displaystyle\vdash\widetilde{e}:\widetilde{B}$ $\displaystyle\Gamma$
$\displaystyle\vdash e_{2}:s$

and we know from LABEL:t-dec-m that $\Gamma^{\prime}\vdash S^{\prime}:cmd(s)$,
where $S^{\prime}$ is the body of the method and
$\Gamma^{\prime}=\Gamma,\widetilde{x}:var(\widetilde{B}),\texttt{value}:var(s)$,
and $\Gamma\vdash\texttt{$Y$.balance}:var(s)$, where $Y$ is the address of the
callee.

The transition must have been concluded by LABEL:ts_bss_call. In the premise,
there are two writes to the balance fields of caller and callee, both of which
are typed as $var(s)$. The new environment is $\text{env}_{S}^{\prime\prime}$,
so it holds that
$\Gamma\vdash\text{env}_{S}=_{s^{\prime}}\text{env}_{S}^{\prime\prime}$.

We have that
$\text{env}_{V}^{\prime\prime}=(\widetilde{x},\widetilde{v}),(\texttt{this},Y),(\texttt{sender},X),(\texttt{value},n)$,
so $\Gamma^{\prime}\vdash\text{env}_{V}^{\prime\prime}$ holds. Then
$\text{env}_{T}\vdash\left<S^{\prime},\text{env}_{SV}^{\prime\prime}\right>\rightarrow\text{env}_{SV}^{\prime}$,
and by the induction hypothesis
$\Gamma^{\prime}\vdash\text{env}_{SV}^{\prime\prime}=_{s^{\prime}}\text{env}_{SV}^{\prime}$
then holds.

As the extensions of $\Gamma^{\prime}$ only concern variables, they can
therefore be removed. Hence,
$\Gamma\vdash\text{env}_{SV}=_{s^{\prime}}\text{env}_{S}^{\prime},\text{env}_{V}$
holds by Lemma 4.3.

  * •

If LABEL:t-subs-s was used, then we know from the premise that $\Gamma\vdash
S:cmd(s^{\prime})$ and $\Gamma\vdash cmd(s^{\prime})\mathrel{<:}cmd(s)$. By
the induction hypothesis, the statement holds for $\Gamma\vdash
S:cmd(s^{\prime})$. Thus
$\Gamma\vdash\text{env}_{SV}=_{s^{\prime}}\text{env}_{SV}^{\prime}$. By
subtyping rule LABEL:subs-cmd, we have that $\Gamma\vdash
s\mathrel{<:}s^{\prime}$, and by LABEL:subs-sec that $s\sqsubseteq
s^{\prime}$. Therefore
$\Gamma\vdash\text{env}_{SV}=_{s}\text{env}_{SV}^{\prime}$ obviously also
holds.

##  Appendix C Proof of Theorem 4.6

######  Proof C.1.

By induction on the derivation of $\Gamma\vdash e:B$.

  * •

If LABEL:t-val was used to conclude $\Gamma\vdash e:B$, then $e$ = $v$. The
result is immediate, since the value does not depend on $\text{env}_{SV}$.

  * •

If LABEL:t-var was used, then $e$ = $x$, and from the premise we have that
$\Gamma\vdash x:var(B)$, which was concluded by LABEL:t-box-x. By assumption,
$B\leadsto s$ and $\Gamma\vdash\text{env}_{SV}^{1}=_{s}\text{env}_{SV}^{2}$ so
$\text{env}_{V}(x)=\text{env}_{V}(x)$. Thus we can conclude by LABEL:Exp-Var.

  * •

If LABEL:t-field was used, then $e$ = $e^{\prime}.p$, and from the premise we
have that $\Gamma\vdash e^{\prime}.p:var(B)$, which was concluded by
LABEL:t-box-f. From the premise and side condition of that rule, we then know
that $\Gamma\vdash e^{\prime}:I_{s}$, $\Gamma(I)(p)=var(B)$ and $B\leadsto s$.
By assumption, $\Gamma\vdash\text{env}_{SV}^{1}=_{s}\text{env}_{SV}^{2}$.
Therefore by the induction hypothesis

$\displaystyle\text{env}_{SV}^{1}\vdash e^{\prime}\rightarrow v^{\prime}$
$\displaystyle\text{env}_{SV}^{2}\vdash e^{\prime}\rightarrow v^{\prime}$

where $v^{\prime}$ is an address $X$. Then
$\text{env}_{S}^{1}(X)(p)=\text{env}_{S}^{2}(X)(p)$ Thus we can conclude by
LABEL:Exp-Field.

  * •

If LABEL:t-op was used, then $e$ = $\operatorname{op}(e_{1},\ldots,e_{n})$.
From the premise, we know that each of the arguments $e_{i}$ are typable as
$\Gamma\vdash e_{i}:B$ where $B\leadsto s$ so by $n$ applications of the
induction hypothesis, we get that $\text{env}_{SV}^{1}\vdash e_{i}\rightarrow
v_{i}$ and $\text{env}_{SV}^{2}\vdash e_{i}\rightarrow v_{i}$, so we can
conclude by rule LABEL:Exp-Op.

  * •

If LABEL:t-subs-e was used, then we know from the premise that $\Gamma\vdash
e:B^{\prime}$ and $\Gamma\vdash B^{\prime}\mathrel{<:}B$. By the subtyping
rules LABEL:subs-sec resp. LABEL:subs-name, we know that
$s^{\prime}\sqsubseteq s$. Hence, by Lemma 4.2,
$\Gamma\vdash\text{env}_{SV}^{1}=_{s^{\prime}}\text{env}_{SV}^{2}$ also holds.
Then by the induction hypothesis, the statement holds for $\Gamma\vdash
e:B^{\prime}$ where $B^{\prime}\leadsto s^{\prime}$.

This concludes the proof.

##  Appendix D Proof of Theorem 4.7

######  Proof D.1.

There are two cases to consider: In the first case, assume
$s_{1}\not\sqsubseteq s_{2}$ (i.e. $s_{2}$ is either strictly below $s_{1}$,
or they are incomparable). By Theorem 4.5 we can then conclude the following:

  * •

$\Gamma\vdash\text{env}_{SV}^{1}=_{s_{2}}\text{env}_{SV}^{1^{\prime}}$

  * •

$\Gamma\vdash\text{env}_{SV}^{2}=_{s_{2}}\text{env}_{SV}^{2^{\prime}}$

As we know that $\Gamma\vdash\text{env}_{SV}^{1}=_{s_{2}}\text{env}_{SV}^{2}$
it therefore also holds that
$\Gamma\vdash\text{env}_{SV}^{1^{\prime}}=_{s_{2}}\text{env}_{SV}^{2^{\prime}}$.

For the other case, where $s_{1}\sqsubseteq s_{2}$, we proceed by induction on
the derivation of $\Gamma\vdash S:cmd(s_{1})$.

  * •

If LABEL:t-skip was used to conclude the judgment $\Gamma\vdash S:cmd(s_{1})$,
then $S$ = skip. Then the result is immediate, since skip does not affect
$\text{env}_{SV}$.

  * •

If LABEL:t-throw was used to conclude the judgment $\Gamma\vdash
S:cmd(s_{1})$, then $S$ = throw. The statement then holds vacuously, since
$\text{env}_{T}\vdash\left<\texttt{throw},\text{env}_{SV}\right>\not\rightarrow$.

  * •

If LABEL:t-decvar was used to conclude the judgment $\Gamma\vdash
S:cmd(s_{1})$, then $S$ = $var(B)$ $x$ := $e$ in $S^{\prime}$, and from the
premise we know that $\Gamma\vdash e:B$ and $\Gamma,x:var(B)\vdash
S^{\prime}:cmd(s_{1})$. By LABEL:ts_bss_decv we have that

$\displaystyle\text{env}_{T}$ $\displaystyle\vdash\left<\texttt{$var(B)$ $x$
:= $e$ in
$S^{\prime}$},\text{env}_{SV}^{1}\right>\rightarrow\text{env}_{SV}^{1^{\prime}}$
$\displaystyle\text{env}_{T}$ $\displaystyle\vdash\left<\texttt{$var(B)$ $x$
:= $e$ in
$S^{\prime}$},\text{env}_{SV}^{2}\right>\rightarrow\text{env}_{SV}^{2^{\prime}}$

where $x\notin\operatorname{dom}\left(\text{env}_{V}^{i^{\prime}}\right)$ for
$i\in\left\\{\,1,2\,\right\\}$. From the premise, we know that

$\displaystyle\text{env}_{SV}^{1}$ $\displaystyle\vdash e\rightarrow v_{1}$
$\displaystyle\text{env}_{SV}^{2}$ $\displaystyle\vdash e\rightarrow v_{2}$
$\displaystyle\text{env}_{T}$
$\displaystyle\vdash\left<S^{\prime},\text{env}_{S}^{1},(x,v_{1}):\text{env}_{V}^{1}\right>\rightarrow\text{env}_{S}^{1^{\prime}},(x,v_{1}^{\prime}):\text{env}_{V}^{1^{\prime}}$
$\displaystyle\text{env}_{T}$
$\displaystyle\vdash\left<S^{\prime},\text{env}_{S}^{2},(x,v_{2}):\text{env}_{V}^{2}\right>\rightarrow\text{env}_{S}^{2^{\prime}},(x,v_{2}^{\prime}):\text{env}_{V}^{2^{\prime}}$

In order to apply the induction hypothesis, we must show that

$\Gamma,x:var(B)\vdash\text{env}_{S}^{1},(x,v_{1}):\text{env}_{V}^{1}=_{s_{2}}\text{env}_{S}^{2},(x,v_{2}):\text{env}_{V}^{2}$

For this purpose, assume $B\leadsto s^{\prime}$ for some $s^{\prime}$ There
are then two cases to consider:

    1. 1.

If $s^{\prime}\sqsubseteq s_{2}$ then it follows from Theorem 4.6, since all
variables read within $e$ are of a lower level than $s_{2}$, and by
assumption, $\text{env}_{SV}^{1}$ and $\text{env}_{SV}^{2}$ agree on all
values up to, and including, $s_{2}$. Hence $v_{1}=v_{2}=v$ and thus

$\Gamma,x:var(B)\vdash\text{env}_{S}^{1},(x,v):\text{env}_{V}^{1}=_{s_{2}}\text{env}_{S}^{2},(x,v):\text{env}_{V}^{2}$

also holds.

    2. 2.

If $s^{\prime}\not\sqsubseteq s_{2}$, then $s^{\prime}$ is either strictly
higher than $s_{2}$, or they are incomparable. Then

$\Gamma,x:var(B)\vdash\text{env}_{S}^{1},(x,v_{1}):\text{env}_{V}^{1}=_{s_{2}}\text{env}_{S}^{2},(x,v_{2}):\text{env}_{V}^{2}$

holds by definition of the $\Gamma\vdash\cdot=_{s}\cdot$ relation.

Then by the induction hypothesis we have that

$\Gamma,x:var(B)\vdash\text{env}_{S}^{1^{\prime}},(x,v_{1}^{\prime}):\text{env}_{V}^{1^{\prime}}=_{s_{2}}\text{env}_{S}^{2^{\prime}},(x,v_{2}^{\prime}):\text{env}_{V}^{2^{\prime}}$

By Lemma 4.3 we can then conclude
$\Gamma\vdash\text{env}_{SV}^{1^{\prime}}=_{s_{2}}\text{env}_{SV}^{2^{\prime}}$
as required.

  * •

If LABEL:t-ass-v was used, then $S$ = $x$ := $e$. From the premise, we know
that $\Gamma\vdash x:var(B_{1})$ and $\Gamma\vdash e:B_{1}$ where
$B_{1}\leadsto s_{1}$. By LABEL:ts_bss_assv, we know that

$\displaystyle\text{env}_{SV}^{1}$ $\displaystyle\vdash e\rightarrow v_{1}$
$\displaystyle\text{env}_{SV}^{2}$ $\displaystyle\vdash e\rightarrow v_{2}$
$\displaystyle\text{env}_{T}$ $\displaystyle\vdash\left<\texttt{$x$ :=
$e$},\text{env}_{SV}^{1}\right>\rightarrow\text{env}_{S}^{1},\text{env}_{V}^{1}\kern-2.0pt\left[x\mapsto
v_{1}\right]$ $\displaystyle\text{env}_{T}$
$\displaystyle\vdash\left<\texttt{$x$ :=
$e$},\text{env}_{SV}^{2}\right>\rightarrow\text{env}_{S}^{2},\text{env}_{V}^{2}\kern-2.0pt\left[x\mapsto
v_{2}\right]$

We know that $s_{1}\sqsubseteq s_{2}$, and by assumption
$\Gamma\vdash\text{env}_{SV}^{1}=_{s_{2}}\text{env}_{SV}^{2}$. By Theorem 4.6,
we can therefore conclude that $v_{1}=v_{2}=v$. Thus

$\Gamma\vdash\text{env}_{S}^{1},\text{env}_{V}^{1}\kern-2.0pt\left[x\mapsto
v\right]=_{s_{2}}\text{env}_{S}^{2},\text{env}_{V}^{2}\kern-2.0pt\left[x\mapsto
v\right]$

also holds.

  * •

If LABEL:t-ass-f was used, then $S$ = this.$p$ := $e$. The argument is then
the same as above, except that it is $\text{env}_{S}$, rather than
$\text{env}_{V}$ that is updated.

  * •

If LABEL:t-seq was used, then $S$ = $S_{1}$; $S_{2}$. From the premise, we
know that $\Gamma\vdash S_{1}:cmd(s_{1})$ and $\Gamma\vdash S_{2}:cmd(s_{1})$.
By LABEL:ts_bss_seq we know that

$\displaystyle\text{env}_{T}$
$\displaystyle\vdash\left<S_{1};S_{2},\text{env}_{SV}^{1}\right>\rightarrow\text{env}_{SV}^{1^{\prime}}$
$\displaystyle\text{env}_{T}$