Securing Smart Contract On The Fly
Extracted source text · arXiv 1911.12555
% \documentclass[conference]{IEEEtran}
\pdfoutput=1
\documentclass[sigplan,10pt]{acmart}\settopmatter{printfolios=true,printccs=false,printacmref=false}
\makeatletter %1
\def\mdseries@tt{m} %1
\makeatother %1
\AtBeginDocument{%
\providecommand\BibTeX{{%
\normalfont B\kern-0.5em{\scshape i\kern-0.25em b}\kern-0.8em\TeX}}}
\bibliographystyle{ACM-Reference-Format}
\settopmatter{printacmref=false}
\setcopyright{none}
\acmConference{}
\acmYear{}
\acmISBN{} % \acmISBN{978-x-xxxx-xxxx-x/YY/MM}
\acmDOI{} % \acmDOI{10.1145/nnnnnnn.nnnnnnn}
\startPage{1}
\renewcommand\footnotetextcopyrightpermission[1]{}
\newcommand{\systemname}{\sc{Solythesis}}
\newcommand{\inlinesol}[1]{\mintinline{JavaScript}{#1}}
\newcommand{\sourcecode}[1]{\texttt{#1}}
\newcommand{\pluseq}{\mathrel{+}=}
\newcommand{\minuseq}{\mathrel{-}=}
\newcommand{\rom}[1]{\uppercase\expandafter{\romannumeral #1\relax}}
% \pagestyle{plain}
% \usepackage{minted}
\usepackage[frozencache=true]{minted}
% \usepackage[finalizecache=true]{minted}
\usepackage[figure,vlined,linesnumbered]{algorithm2e}
\usepackage{amsmath}
\usepackage{stmaryrd}
% \usepackage[natbib]{biblatex}
% \usepackage{mathtools}
\usepackage{pgf-pie}
\usepackage{pgfplots}
\usepackage{esvect}
\usepackage[htt]{hyphenat}
\usepackage{mathpartir}
% \setlength{\abovecaptionskip}{-1pt}
% \setlength{\droptitle}{-3em}
% \setlength{\textfloatsep}{3pt}
% \setlength{\dbltextfloatsep}{3pt}
\graphicspath{{./figures}}
\setminted{
frame=lines,
baselinestretch=0.7,
fontsize=\footnotesize,
linenos,
baselinestretch=1,
breaklines,
xleftmargin=17pt,
escapeinside=??
}
\SetKwInOut{Input}{Input}
\SetKwInOut{Output}{Output}
\SetKw{kwGoTo}{go to}
\SetKw{kwThrow}{throw}
\SetKw{To}{ to }
\SetKw{In}{ in }
\SetKw{Not}{ not }
\SetKw{Continue}{continue}
\SetKw{Is}{ is }
\SetKw{Or}{ or }
\begin{document}
%don't want date printed
\date{}
\title{Securing Smart Contract On The Fly}
\author{Ao Li}
\affiliation {
\institution{University of Toronto}
}
\email{leo@cs.toronto.edu}
\author{Jemin Andrew Choi}
\affiliation {
\institution{University of Toronto}
}
\email{choi@cs.toronto.edu}
\author{Fan Long}
\affiliation {
\institution{University of Toronto}
}
\email{fanl@cs.toronto.edu}
\input{files/abstract}
\maketitle
% \input{files/abstract}
\input{files/introduction}
\input{files/observations}
\input{files/example}
\input{files/design}
\input{files/implementation}
\input{files/evaluation}
\input{files/relatedwork}
\input{files/conclusion}
% {\normalsize \bibliographystyle{IEEEtran}
% }
%% Bibliography
\bibliography{references}
% \printbibliography
\end{document}
\begin{abstract}
We present {\systemname}, a source to source Solidity compiler which takes a
smart contract code and a user specified invariant as the input and
produces an instrumented contract that rejects all transactions that
violate the invariant. The design of {\systemname} is driven by our
observation that the consensus protocol and the storage layer are the
primary and the secondary performance bottlenecks of Ethereum,
respectively. {\systemname} operates with our novel delta update and delta
check techniques to minimize the overhead caused by the instrumented
storage access statements. Our experimental results validate our hypothesis
that the overhead of runtime validation, which is often too expensive for
other domains, is in fact negligible for smart contracts. The CPU overhead
of {\systemname} is only 0.12\% on average for our 23 benchmark contracts.
% We also propose multiple optimization
% techniques that can improve the performance of instrumented smart
% contract significantly.
%{\systemname} employs multiple optimization techniques in order to
%mitigate the overhead introduced by smart contract instrumentation.
%In order to demonstrate the expressiveness of {\systemname} language,
%we specify the specifications for ERC20, ERC721, and ERC1202 standards.
%Our experiment results confirm that the instrumentation of the smart
%contract will not slow down the existing blockchain system. Due to
%the fact that transaction processing
%and smart contract execution is not the bottleneck of the blockchain
%systems, our result highlight the possibilities of bringing runtime
%verifications to smart contracts.
\end{abstract}
\section{Introduction}
Smart contracts are one of the most important features of blockchain
systems~\cite{ethereum}. A smart contract is a program that encodes a set of
transaction rules. Once deployed to a blockchain, its encoded rules are
enforced by all participants of the blockchain network, and therefore it
eliminates counter party risks in sophisticated transactions. People have
applied smart contracts to a wide range of domains such as finance, supply
chain management, and insurance.
Unfortunately, like other programs, smart contracts may contain errors. Errors
inside smart contracts are particularly severe because 1) it is often
impossible or at least difficult to change a smart contract once deployed; 2)
smart contracts often stores and manages critical information such as
digital assets and identities; 3) errors are treated as intended behavior of
the smart contract and faithfully executed by blockchain systems. As a result,
errors inside smart contracts often lead to large financial losses in the real
world~\cite{dao, bec}.
To make smart contracts secure and correct, one approach is to build static
analysis tools. But such static analysis tools are often inaccurate and
generate a large amount of false positives and/or false negatives~\cite{securify}.
Another approach is to formally verify the consistency between the
implementation and specification of a smart contract~\cite{kevm, verisolid, evmstar}. But such
verification processes typically require human intervention and are often too
expensive to apply in practice.
\subsection{Runtime Validation with {\systemname}}
In this paper, we argue that runtime validation is an effective and efficient
approach to secure smart contracts. For traditional programs, with the access
of runtime information, runtime validation techniques can be fully automated
and can typically achieve much higher coverage than static analysis techniques.
The downside of runtime validation is its excessive performance overhead.
However, the Proof-of-Work consensus is the primary performance bottleneck of
existing blockchain systems. For example, the consensus protocol of Ethereum
can only process up to 38 transactions per second, while the execution engine
of Parity~\cite{parity}, a popular efficient Ethereum implementation, can
process more than 700 transactions on an ordinary laptop with a SSD. Therefore,
our hypothesis is that the overhead of runtime validation, which is often too
expensive for other domains, is in fact negligible for smart contracts.
To validate our hypothesis, we design and implement {\systemname}, a novel
runtime validation framework for \break Ethereum smart contracts. Unlike static
analysis and formal verification techniques that attempt to detect errors in
smart contracts offline, {\systemname} works as a source to source Solidity
compiler and detects errors at runtime. {\systemname} provides an expressive
language that includes quantifiers to allow users to specify critical safety
invariants of smart contracts. Taking a potentially insecure smart contract and
the specified invariants as inputs, {\systemname} instruments the Solidity code
of the smart contract with runtime checks to enforce the invariants. The
instrumented contract is guaranteed to nullify all transactions that violate
the specified invariants.
The design of {\systemname} is driven by our observation that the storage layer
is the secondary performance bottleneck of Ethereum after the consensus layer. Our
program counter profiling results show that the execution engine of Parity
spent over 67\% of time on components that are relevant to blockchain state
load and store operations. Such load and store operations are expensive
because 1) it may be amplified to multiple slow disk I/O operations, 2) it is
translated by the Solidity compiler into multiple instructions (up to 11 EVM instructions), and
3) the Solidity compiler uses expensive cryptographic hash functions to compute the
address of accessed state objects. We therefore design the instrumentation
algorithm of {\systemname} to minimize the number of blockchain state accesses.
This enables {\systemname} to generate secure contracts with acceptable overhead
even if Ethereum or future blockchain systems adopt a fast consensus protocol.
One naive approach to enforce the invariant is to just instrument the runtime
checks at the end of each transaction. For sophisticated invariants that
involve iterative sums, maps, and quantifiers, the runtime checks must use
loops to access many blockchain state values, which will be extremely
expensive. To address this challenge, {\systemname} instead uses a novel
combination of \emph{delta update} and \emph{delta check} techniques.
{\systemname} statically analyzes the source code of each contract function to
conservatively determine the set of state values that could be modified and the
set of sub-constraints that could be violated during a transaction. It then
instruments the instructions to maintain these potentially changed values and to
only enforce these potentially violated constraints.
% Furthermore, {\systemname} optimizes the
% decorated smart contract so that the overhead introduced by the runtime
% verification is negligible.
%Instead of detecting vulnerabilities offline, {\systemname} rejects
%transactions that violates the specification and secures the smart
%contract on the fly.
% {\systemname} exploits that the transaction
% processing and smart contract execution are not the bottleneck of the
% current blockchain system. Moreover, adding runtime checks to the
% smart contract is effortless since most smart contracts follows a
% common standard and once the standard is formally defined, it can be
% applied to all contracts that conform the same standard.
%Consider the smart contract as a state machine, and the smart contract
%implementation defines the transition rules from states to states. A
%smart contract standard specifies a valid state and the goal of
%{\systemname} is to reject all states that violate the standard.
% {\systemname} traverses the abstract syntax tree (AST) parsed from the
% smart contract and applies a list of rewrite rules to the AST.
%The state of a smart contract is represented by a list of state variables
%stored in persistent storage of the blockchain system.
%Given a constraint defined in the standard, {\systemname} creates a list
%of new state variables to monitor the states of the smart contract and
%the state variables are updated accordingly when the states of the
%smart contract are updated.
%{\systemname} traverses the abstract syntax tree (AST) parsed from the
%smart contract and applies a list of rewrite rules to the AST to update
%the state variables generated from constraints. Every time a instrumented
%smart contract executes a transaction, the state variables of the standard
%are updated and the transactions that violate the standard are reverted.
% Constraints are checked at the end of
% transaction execution and {\systemname}
%Operations of dynamically allocated state variables are expensive
%for smart contracts because it uses a crypto hash function to compute
%the addresses of the variables. Besides, invoking crypto hash function
%requires the program to push the data to the memory first. One challenge
%{\systemname} meets is that the vanilla implementation of {\systemname}
%will add excessive state variable operations to the instrumented smart
%contract. The smart contract compiler fails to optimize such operations
%and the overhead introduced by state variable operations is observable.
% Adding security checks at runtime requires additional computations to
% process each transaction, which may slow down the blockchain system.
% Solidity uses state variables to store values in persistent memory,
% but accessing dynamic allocated state variables is
% expensive
%Another challenge {\systemname} faces is that a smart contract has
%multiple entry points and exit points. Simply adding assertions
%at the end of each function is not enough and may introduce false
%alarms.
% the standard requires
% {\systemname} to check constraints only when the transaction finishes.
% However, the entry point of the smart contract and the call stack are
% not fixed. Simply adding assertions at the end of each function is not
% enough and may introduce false positives.
%To mitigate the overhead introduced by accessing state variables,
%{\systemname} optimizes the decorated source code, which caches the
%storage variable in the operation stack.
% Furthermore, Solidity uses
% state variable to share data among different functions which is
% overkill because accessing state variables are more expensive.
%{\systemname} uses inline assembly to create an in-memory array,
%which allows {\systemname} to pass data across functions. It
%prevents {\systemname} from using state variables to share data
%across functions. In order to increase the accuracy and check
%constraints only at the end of transaction execution, {\systemname}
%builds a call graph of the smart contract to track the call sites
%of each function. For the functions without
%any caller, {\systemname} add assertions at the end of those
%functions. Otherwise, {\systemname} creates a variable to
%track the depth of the current call stack and only verifies constraints
%when the function exits and the depth is zero. In addition,
%{\systemname} takes the benefits from the call graph and only checks
%the constraints containing the state variables that updated by the
%function or its callee.
%\subsection{Standard Specification}
%Bugs and errors inside smart contracts may lead to unintended states.
%Noticing the fact that states are represented by state variables
%and an unintended states always contains disagreements between state variables,
%{\systemname} provides two aggregate operators that allows a user to specify
%the constraints and invariants between different state variables.
%{\systemname} translates those invariants and constraints into assertions,
%which act as validators and reject invalid states when the standard
%is violated.
\subsection{Experimental Results}
We evaluate {\systemname} with 23 smart contracts from \break
ERC20~\cite{erc20}, ERC721~\cite{erc721}, and ERC1202~\cite{erc1202} standards.
ERC20 and ERC721 are two Ethereum smart contract standards for fungible and
non-fungible tokens. ERC1202 is a draft standard for a voting system which is
the key process to many blockchain applications. For each standard, we first
compose an invariant and then apply {\systemname} to instrument the smart
contracts.
Our experimental results show that {\systemname} prevents all vulnerable
contracts from violating the defined invariants. The results also validate our
hypothesis --- the instrumentation overhead is negligible with only 0.12\% CPU
usage overhead and 4.2KB/s disk write overhead on average. Our results also
highlight the effectiveness of our instrumentation algorithm. Even in
extreme cases where the consensus protocol is no longer the performance
bottleneck at all, the {\systemname} instrumentation only causes 24\% overhead
in transaction throughput on average. In comparison, if we use the naive
approach that inserts runtime checks at the end of each transaction, the
transaction throughput would be two orders of magnitude smaller. We believe
our results encourage future explorations on new languages, new analyses, and
new virtual machine designs that can further exploit rigorous runtime
validation to secure smart contracts (see
Section~\ref{sec:results:discussion}).
%We evaluate {\systemname} with smart contracts in three standards
%ERC20~\cite{erc20}, ERC721~\cite{erc721}, and ERC1202~\cite{erc1202}. ERC20 and
%ERC721 are two important smart contracts for fungible and non-fungible tokens.
%ERC1202 is a draft standard for a voting system which is the key process to
%many blockchain applications. For each standard, we first compose an invariant
%and {\systemname} to instrument the smart contracts following the standard.
%To understand the impact of
%runtime checks on different smart contract functions, we not only download
%real word transactions from Ethereum main net but also synthesis transactions
%that call different smart contract functions.
%We modifies the Parity Ethereum
%client, which is the most efficient Ethereum client currently, so that it
%generates blocks at a fixed speed. This eliminates the uncertainty introduced
%by proof of work.
%Our results show that {\systemname} is effective. It prevents all vulnerable
%contracts from violating the defined invariants and the overhead introduced by
%instrumentation is negligible because of the existing consensus bottleneck. Our
%results also highlight the effectiveness of our instrumentation algorithm. Even
%if we turn off the consensus protocol, Parity only process 24\% less
%transactions per second for the instrumented contracts. In comparison, if we
%use the naive instrumentation approach that inserts runtime checks at the end of
%each transaction, Parity would process 94\% less transactions per second.
%Besides, the runtime checks is able to improve security
%of smart contracts significantly. {\systemname} does not suffer from false
%alarms and it guarantees that the transaction that violates the constraints
%will be reverted. The experiment also demonstrates that our optimization
%technique is effective and improves the performance of instrumented smart
%contracts for all benchmarks. The performance of optimized smart contract
%increases more than 18\% for four benchmarks. The remaining 2 benchmarks only
%invoke simple functions of the smart contract, and even the non-optimized
%instrumented smart contracts are able to achieve the same performance of origin
%smart contracts.
\subsection{Contributions}
This paper makes the following contributions:
\begin{itemize}
\item \textbf{Runtime Validation for Smart Contracts:} Our experiment results
show that processing transactions and smart contract execution are not
the bottleneck of current blockchain systems. We show that runtime
validation has the potential of significantly increasing the security
of the smart contracts with only a small or even negligible overhead.
\item \textbf{{\systemname}:} This paper presents a novel source to source
Solidity compiler, {\systemname}, which instruments smart contracts
to reject transactions that violate the specified invariants on the
fly.
% \item \textbf{Standard Specifications:} This paper presents
% an expressive language that allows developers to define standards formally.
% We further define three standards ERC-20, ERC-721, and ERC-1202 using
% the language.
\item \textbf{Instrumentation Optimizations:} This paper presents novel delta
update and delta check techniques to optimize runtime
instrumentation.
\end{itemize}
% The remaining paper is organized as follows. Section~\ref{sec:observation}
% presents our observations on the blockchain system performance bottlenecks and
% discusses how it would influence the way we secure smart contracts.
% Section~\ref{sec:example} presents a motivating example of {\systemname}.
% Section~\ref{sec:design} and Section~\ref{sec:impl} present the design and the
% implementation of {\systemname}, respectively. We evaluate {\systemname} at
% Section~\ref{sec:results}. In Section~\ref{sec:related} we discuss related
% work. We finally conclude in Section~\ref{sec:conclusion}.
\section{Observation}
\label{sec:observation}
We next present our observations on Ethereum blockchain performance. Ethereum
uses a modified version of Nakamoto consensus as its consensus
protocol~\cite{Bitcoin, GHOST, ethereum}. It stores transactions in a chain of blocks.
Participants solve proof-of-work (PoW) problems to generate new blocks to
extend the chain.
\noindent \textbf{Consensus Bottleneck:}
Nakamoto consensus and its chain structure limits the performance of Ethereum
--- it generates a new block every 13 seconds and the sizes of the blocks are
limited by its gas mechanism, which measures the size and the complexity
of a transaction~\cite{ethereum}. Currently, each Ethereum block has a gas
limit of 10,000,000~\cite{gas_limit}, and it was 8,000,000
when we performed our experiments.
A simple transaction that only transfers Ether consumes 21,000
gas, and the gas consumption for transactions calling smart contract functions
is higher.
\begin{figure}[t]
\begin{center}
\begin{tabular}{ |c|c|c|c|c|c|c|c| }
\hline
& \textbf{ERC20} & \textbf{ERC721} & \textbf{ERC1202}\\
\hline
\textbf{Native} & 34 & 11 & 9 \\
\hline
\textbf{NoConsensus} & 2181 & 1184 & 1439 \\
\hline
\textbf{NoConsensus+Empty} & 3647 & 1869 & 2460 \\
\hline
\end{tabular}
\end{center}
\caption{Number of transactions can be processed by Parity client
with different configurations.}
\label{fig:consensus-observation}
\end{figure}
To understand the impact of the consensus layer on the overall performance of
Ethereum, we run experiments with representative transaction traces for the
following contracts: the BEC contract~\cite{bec_contract}, an ERC-20 smart contract for
managing fungible BEC tokens, the DozDoll contract~\cite{doz_contract}, an ERC-721 smart
contract for managing non-fungible DOZ tokens, and an example contract in
the ERC-1202 contract standard~\cite{erc1202}, which is designed for hosting voting on
Ethereum. We use Parity, the most efficient Ethereum client that is publicly available,
to start a private Ethereum network to process these transactions.
Figure~\ref{fig:consensus-observation} presents the number of transactions that
can be processed per second for each contract. Note that we run our experiments
with three different configurations: 1) we use the Ethereum state at the block
height 5,052,259 as the initial state and run PoW consensus to pack and process
transactions (corresponding to the group ``Native'' in
Figure~\ref{fig:consensus-observation}); 2) we remove the PoW consensus limit
so that Parity can process as many transactions as its transaction execution
engine allows (corresponding to the group ``NoConsensus'' in
Figure~\ref{fig:consensus-observation}); 3) we remove the PoW limit and
start Parity with an empty genesis state instead (corresponding to the group
``NoConsensus+Empty'' in Figure~\ref{fig:consensus-observation}).
The results in Figure~\ref{fig:consensus-observation} show that the consensus
protocol of Ethereum is the primary performance bottleneck. Parity only
processes 9 to 34 transactions per second for the ERC-20, ERC-721, and ERC-1202
contracts. If the consensus protocol is disabled, Parity processes 1184 to 2181
transactions per second for the same set of contracts. Therefore, our hypothesis
is that the overhead of runtime validation is negligible for smart contracts,
because the transaction execution engine is not the bottleneck of Ethereum
clients like Parity at all.
%\noindent\fbox{
% \parbox{0.95\columnwidth}{
% \noindent \textbf{Observation 1:} The consensus protocol is the primary
% performance bottleneck of Ethereum clients.
% }
%}
\noindent \textbf{Storage Bottleneck:} The results in
Figure~\ref{fig:consensus-observation} show that Parity would run much faster
with an empty initial state than with an initial state corresponding to the
real Ethereum network at block 5,052,259. This is because all Ethereum clients,
including Parity, store the blockchain state as a Merkle Patricia Tree
(MPT)~\cite{ethereum} on the disk. Each update on the blockchain
state will be amplified to multiple disk I/O operations depending on the height
of the MPT. When Parity starts with an empty state, the MPT is simpler.
Therefore, there will be fewer I/O operations than starting with
a complicated state.
\begin{figure}[t]
\begin{center}
\begin{tabular}{ |c|c|c|c|c|c|c|c| }
\hline
& \textbf{Storage} & \textbf{Verifier} & \textbf{EVM} & \textbf{Other}\\
\hline
\textbf{ERC20} & 67.0\% & 25.9\% & 3.9\% & 3.2\% \\
\hline
\textbf{ERC721} & 73.5\% & 18.3\% & 5.7\% & 2.5\% \\
\hline
\textbf{ERC1202} & 73.1\% & 20.5\% & 3.6\% & 2.8\% \\
\hline
\end{tabular}
\end{center}
\caption{The performance counter results for different
components of Parity client.}
\label{fig:pc_counter}
\end{figure}
To better understand the performance impact of the block chain state updates
(i.e., load/store EVM instructions), we profile Parity in our experimental runs
to collect the performance counters of different components in Parity.
Figure~\ref{fig:pc_counter} presents the profiling results. It classifies the
performance counters into four categories: 1) the modules for the blockchain
state updates, including the RocksDB storage layer and the functions in the EVM
interpreter for the load/store Solidity statements; 2) the modules for
verifying signatures in transactions; 3) the modules for other EVM instructions
except loads/stores; 4) all remaining modules.
Our results show that the blockchain state updates account for more than 67\%
of the performance counters for all experimental runs of Parity when we turn
off the consensus layer. The load and store operations to the blockchain state
are particularly expensive because 1) these operations could trigger one or
more disk I/O operations, 2) the Solidity compiler often generates expensive
SHA3 EVM instructions to compute the address operands of these
operations~\cite{solar, verx}, and 3) the Solidity compiler often translates
one state load/store statement into multiple EVM instructions (up to eleven).
%\noindent\fbox{
% \parbox{0.95\columnwidth}{
% \noindent \textbf{Observation 2:} The state storage layer is the
% secondary performance bottleneck of Ethereum clients.
% }
%}
Therefore, if Ethereum or any other blockchain system could adapt a fast
consensus protocol which eliminates the consensus performance bottleneck, the
state storage layer would become the new bottleneck of the system. This
observation implies that, to reduce the overhead of a runtime instrumentation
tool, one should minimize the number of instrumented load/store statements.
\section{Example}\label{sec:example}
\begin{figure}[t]
\centering
\inputminted{JavaScript}{./code/examples/vote.sol}
\caption{Simplified source code from a voting contract.}
\label{code:voting}
\end{figure}
We next present a motivating example to illustrate the design of {\systemname}.
Figure~\ref{code:voting} shows a simplified source code from the draft of
ERC1202~\cite{erc1202}, which is a technical standard draft that defines a set
of function interfaces to implement a voting system. A voting system allows a
user to vote different issues, and returns the winning option. This example is
used for illustration purposes in the ERC1202 draft, but it contains a logic
error.
In Figure~\ref{code:voting}, the \sourcecode{vote()} function updates the vote
of a transaction initiator given an option and an issue. The contract
implements \sourcecode{vote()} and other functions with five state variables.
\sourcecode{options} stores the available options of each issue;
\sourcecode{isOpen} stores the current status of the issue;
\sourcecode{weights} stores the weight of each voter on each issue;
\sourcecode{weightedVoteCount} stores the total weighted count of each option on
each issue; \sourcecode{ballots} stores the vote of each voter on each
issue.
In the implementation of the \sourcecode{vote()} function, it first fetches the
weight of the transaction initiator and updates the weighted votes of the given
option and issue (lines 11 and 13 in Figure~\ref{code:voting}). However, the
implementation contains two errors: 1) the original implementation fails to
consider the case where the transaction initiator votes multiple times on the
same issue; 2) it is possible for an attacker to trigger an overflow error at
line 13 to illegally modify the weighted vote count. Note the original
implementation misses line 12 and line 14 which are necessary to avoid these
errors. We next apply
{\systemname} to the contract and describe how {\systemname} instruments the
contract to nullify these errors.
\begin{figure}[t]
\centering
\inputminted{JavaScript}{./code/examples/vote.txt}
\caption{Specification for ERC1202 standard.}
\label{code:erc1202}
\end{figure}
\noindent \textbf{Specify Invariant:}
Note that both of these errors cause the contract to potentially violate the
ERC-1202 invariant where the total weighted count of an option on an issue
should equal to the sum of all weights of voters who voted for the
option. To apply {\systemname}, we first specify this invariant shown as
Figure~\ref{code:erc1202}. The first line in Figure~\ref{code:erc1202} defines
an intermediate map $s$ that corresponds to the sum of all weights of the
voters that voted for an issue and option pair. The second line defines a
constraint with the \sourcecode{ForAll} quantifier to enforce that for all
pairs of issues and options, the intermediate map $s$ should equal to the
calculated \sourcecode{weightedVoteCount} in the state. Note that in ERC-1202,
zero is a special option id to denote that a voter did not vote yet. Therefore
our invariant excludes the option id zero.
Figure~\ref{code:erc1202} highlights the expressiveness of the invariant
language in {\systemname}. A user can refer to any state variable in the contract
(e.g., \sourcecode{weights}, \sourcecode{ballot}, and
\sourcecode{weightedVoteCount} in Figure~\ref{code:erc1202}), define
intermediate values including maps, and specify constraints on state
variables and defined intermediate values. {\systemname} supports
sophisticated operations such as a conditional sum over values inside maps
(e.g., line 1 in Figure~\ref{code:erc1202}) and a \sourcecode{ForAll} quantifier
to define a group of constraints for multiple state values at once (e.g., line
2 in Figure~\ref{code:erc1202}).
\begin{figure}[t]
\centering
\inputminted{JavaScript}{./code/examples/vote_secured.sol}
\caption{Instrumented voting contract.}
\label{code:vote_secured}
\end{figure}
\noindent \textbf{Instrument the Contract:}
One naive approach to enforce the invariant in Figure~\ref{code:erc1202} is to
instrument a brute force check at the end of every transaction. This would
cause prohibitive overhead because of the iterative sum
operation and the quantifier constraint. It would cost two or even three
nested loops to check the invariant for every transaction. {\systemname}
instead instruments code to perform \emph{delta updates} and \emph{delta
checks} to reduce the overhead. The intuition is to maintain intermediate
values such as $s$ in Figure~\ref{code:erc1202} and to instrument updates and
checks only when necessary. Figure~\ref{code:vote_secured} presents the
instrumented contract code generated by {\systemname} for our example.
\noindent \textbf{Instrument Delta Updates:}
For every intermediate value such as $s$ in Figure~\ref{code:erc1202},
{\systemname} instruments the contract to add it as a state variable. Then for
every write operation to an original state variable in the contract (e.g., line
18 in Figure~\ref{code:vote_secured}), {\systemname} performs static analysis
to determine whether modifying the original variable may cause the
intermediate value to change. If so, {\systemname} instruments code to update
the intermediate value conditionally (e.g., line 17 and 21 in
Figure~\ref{code:vote_secured}).
\sloppypar{
\noindent \textbf{Compute Free Variable Bindings:}
For every state write operation in the contract, {\systemname} computes
\emph{free variable bindings} against each rule in the invariant. For example,
for the write operation to \sourcecode{ballots} at line 18 in
Figure~\ref{code:vote_secured}, {\systemname} determines that the operation may
change the intermediate value defined in the first line of the invariant.
{\systemname} also binds the free variable $a$ in the invariant to
\sourcecode{issueId}, binds $b$ to \sourcecode{msg.sender},
and binds $c$ to \sourcecode{ballot[issueId][msg.sender]}. These bindings indicate that the
write to \sourcecode{ballot[issueId][msg.sender]} may only change the
intermediate value \sourcecode{s[issueId][ballot[issueId][msg.sender]]}. Therefore
{\systemname} instruments code at lines 17 and 21 to only update this value.}
\noindent \textbf{Instrument Delta Check:}
For every state write operation, {\systemname} also checks it against
\sourcecode{Assert} constraints in the invariant. For example, for the write
operation to \sourcecode{ballots} at line 18 in Figure~\ref{code:vote_secured},
{\systemname} first runs its binding analysis against the constraint at line 2
in Figure~\ref{code:voting} which contains a \sourcecode{ForAll} quantifier.
This analysis determines that the write operation may cause the contract to
violate the constraint when $x$ binds to \sourcecode{issueId} and $y$ binds to
\sourcecode{ballot[issueId][msg.sender]}. {\systemname} defines additional
arrays like \sourcecode{x\_arr} and \sourcecode{y\_arr} to collect such free
variable combinations that may lead to constraint violations lines 3 and 4 in Figure~\ref{code:vote_secured}.
{\systemname} then instruments statements at lines 14-15 and 19-20 to
appropriately maintain these arrays. {\systemname} finally instruments a loop
at the end of the transactions to only check these potentially violated
constraints (lines 25-26).
\noindent \textbf{Nullify Errors:}
{\systemname} generates the instrumented program as its output shown as
Figure~\ref{code:vote_secured}. This instrumented program will enforce the
invariant faithfully during runtime and detect any malicious transactions
that cause the contract to violate the invariant. In our example, we deploy the
instrumented contract to Ethereum and intentionally trigger the error by
sending transactions to vote for an issue multiple times. The instrumented
assertion at line 22 catches this error and aborts the offending transactions
as NoOps. Therefore {\systemname} successfully nullifies the error.
\section{Design}
\label{sec:design}
We next formally present the design of {\systemname}. In this section, we use
the notation $s[X/Y]$ to denote replacing every occurrence of $X$ in the
statement $s$ with $Y$. To avoid confusion, we will use ``$\llbracket
\rrbracket$'' instead of ``$[]$'' to denote indexing of map variables. We also
use the notation $\vv{x}$ to denote a list of variables $x_1, x_2, \ldots$.
\subsection{Invariant and Contract Languages}
\begin{figure}
\input{figures/core-lang-standard.tex}
\caption{The invariant specification language.}
\label{fig:core}
\end{figure}
\noindent \textbf{Invariant Language:}
Figure \ref{fig:core} presents the syntax of our invariant specification
language with integers, variables, arithmetic expressions, conditional
expressions, intermediate value declarations, and constraints. There are
three types of variables: state variables, intermediate variables, and free
variables. State variables are variables declared in smart contracts and stored
in persistent storage. Intermediate variables correspond to the intermediate
values defined in the invariant rules of the form ``$v=\text{Map}\ldots$''.
Note that in our language we do not distinguish these two kinds of variables,
because {\systemname} instruments code to declare intermediate variables as
state variables. Free variables are only used together with \sourcecode{Map},
\sourcecode{Sum} or \sourcecode{ForAll}. They act as indexes for a defined
intermediate map, as iterators for a sum operation, or as quantifier variables
to define a group of constraints at once.
Expressions are built out of variables and integer constants. ``aop'' represents
an arbitrary binary operator; ``cop'' represents an arbitrary integer
comparison operator. There are three possible types for expressions, integers
for scalar values, maps that have integer keys, and booleans for conditional
expressions. All variables and expressions should be well typed. $e\llbracket x
\rrbracket$ denotes accessing the map $e$ at the index $x$, where $e$ must be
an expression with a map type and $x$ must be a free variable with the integer
type. It is possible to have multi-dimensional maps. In the rest of this
section, the notation $e\llbracket\vv{x}\rrbracket$ is an abbreviation of
$e\llbracket x_1 \rrbracket \llbracket x_2 \rrbracket \llbracket \ldots
\rrbracket$ for accessing such multi-dimensional maps.
%Similar to Solidity and
%EVM, a map is initially empty --- an empty map will map everything to zero or
%another empty map that has one less dimension.
%Free variables are only used in \sourcecode{sum} and \sourcecode{forall} aggregates.
%They are used as placeholders and represent all possible integers.
%The types of free variables are inferred using inference rules described
%in Section~\ref{sec:design:type}. Note if a type of a free variable can not be
%determined statically using type inference rules, the standard is ill-defined.
% \noindent\textbf{Types: }There are two types of types. An elementary type is a type
% of arity 0. {\systemname} supports three elementary types: Integer, Address, and Boolean.
% A mapping type is a type of arity 2, the first one is index type and the
% second is object type.
% A type signature $\Sigma$ is a partial mapping from the
% variables $v$ and $mu$ to $t$.
%\noindent\textbf{Expressions:} Expressions are built out of variables and constants.
%$\oplus$ represents an arbitrary binary operator. An indexing expression is
%represented by $e_1\llbracket e_2\rrbracket$ where $e_1$ is the object expression
%and $e_2$ is the index expression.
%The language considers only well-typed expressions. Types of expressions can be
%determined statically using type inference rules described in
%Section~\ref{sec:design:type}.
The language has two kinds of rules: intermediate value declaration rules and
constraint declaration rules. An intermediate value declaration can define a
map value indexing over a list of free variables and can conditionally and iteratively sum over
state variable values to compute each map entry. For a rule of the form
``$v=$Map $\vv{x}$ Sum $e$ Over $\vv{y}$ Where $c$'', each entry of the intermediate map $v$ is defined as follows:
$$
\forall\vv{x}\; v\llbracket\vv{x}\rrbracket=\sum{_{\vv{y}}}\left\{
\begin{array}{ll}
e & \mbox{if } c \mbox{ is True}\\
0 & \mbox{otherwise}
\end{array}
\right.
$$
A constraint declaration rule of the form ``ForAll $\vv{x}$ Assert $c$'' checks
all possible assignments of $\vv{x}$ to ensure that $c$ is always satisfied.
Note that free variable lists after \sourcecode{Map} and \sourcecode{ForAll} can be empty.
Therefore, users can use these rules to define scalar values and simple
constraints as well. Also note that free variables in invariants iterate over
all defined keys in maps where those variables are used as indexes. For
example, in ``ForAll $\vv{x}$ Assert $e\llbracket x\rrbracket$'', $x$ should
iterate over values that correspond to defined keys in $e$.
%\subsection{Type Inference}\label{sec:design:type}
%\if 0
%\begin{figure}
% \input{figures/types.tex}
% \caption{Type rules for expressions.}
%\label{fig:type}
%\end{figure}
%\fi
%Figure~\ref{fig:type} presents a set of rules defining well-typed
%expressions with respect to a type signature $\Sigma$, which is
%a partial mapping from the variables $v$ and $\mu$ to type $t$.
%There are two types of types. An integer type is an elementary
%type of arity 0. A mapping type is a type of arity 2, the first
%one is the type of index element and the second one is the type of object element.
%Each rule is of the form $\Sigma\vdash exp:t$ which denotes
%that expression $exp$ has the type $t$. All state variables have a data type
%explicitly declared in smart contracts or standard specifications.
%If a variable is used as the index element of a mapping expression with type
%$\text{Mapping}\;i\;t$, the variable has type $i$.
%Both operands of binary expression have integer types.
%The type of \sourcecode{sum} expression is defined recursively by types of $\vv{\mu}$.
%The \sourcecode{sumtype} function shows the algorithm to compute the type
%of \sourcecode{sum} expression. The input of the function is a list of
%types of $\vv{\mu}$. The function creates a mapping type which has n+1 dimension and
%n is the length of $\vv{\mu}$.
\begin{figure}
\input{figures/core-lang-contract.tex}
\vspace{-7mm}
\caption{Core language for smart contracts.}
\vspace{-3mm}
\label{fig:smart-contract}
\end{figure}
\noindent \textbf{Smart Contract Language:}
Figure~\ref{fig:smart-contract} presents the core language of smart contracts
that we use to illustrate {\systemname}. ``op'' denotes an
arbitrary binary operator. We do not distinguish normal expressions and
conditional expressions in our contract language. There are two kinds of
variables: state variables that may be referred in the invariant and temporary
scalar variables that are local to the contract program.
``load'' and ``store'' are statements for accessing blockchain state variables.
Similar to Solidity, state variables can be either scalar values or maps. ``for
$t_1,t_2,\ldots$ in $v$ \{$s_1$\}'' would iterate over all possible assignment
combinations of $t_1, t_2, \ldots$ based on how $t_1,t_2,\ldots$ are used as
indexing variables for the map $v$ in $s_1$. If any of these variables are not
used as indexing variables for $v$, this statement is undefined. Loop
statements in our language capture the most common usage of loops in Solidity
contracts, and its syntax simplifies the presentation of our instrumentation
algorithm. Note that in Solidity, every state variable has to be declared
before its use. We omit the declaration syntax for brevity.
%The languages of
%constants, variables, and expression are the same as standard specification.
%The statements of a smart contract are similar to statements of C programming
%language including branching, loop, assignment, function call and return.
%Besides the mapping type mentioned in Section~\ref{sec:design:type}, the smart
%contract allows variables with array types: $\mathrm{array}\;t$. Both array
%variables and mapping variables can be indexed in smart contracts.
% A smart contract function
% is a function
% \subsection{Free Variable Binding and Substitution}
\subsection{Instrumentation Algorithm}
\begin{algorithm}[t]
\input{figures/instrument.tex}
\caption{Instrumentation algorithm.}
\label{fig:instrument}
\end{algorithm}
Figure~\ref{fig:instrument} presents the {\systemname} instrumentation
algorithm. Given a program $P$ as a list of contract statements and an
invariant $R$ as a list of rules, the algorithm produces an instrumented
program $P'$ that enforces the invariant dynamically. The algorithm has two
parts. Lines 2-12 handle the intermediate value declarations in $R$, while
lines 13-24 handle the quantifier constraint rules in $R$.
For every defined intermediate value $v$, the algorithm instruments a fresh
state variable declaration for the value (line 4). The algorithm then inspects
every store statement $s$ in $P$ and instruments the contract to maintain $v$
(lines 5-12). The algorithm first computes possible bindings of free variables
in the definition of $v$ (lines 6-7). A binding is a set of pairs of free
variables in the definition and expressions in the contract. The binding
corresponds to possible entries of $v$ (if $v$ is a map) that $s$ may influence
via state variable write operations. The algorithm prepares statement templates
for updating $v$ (lines 8 and 10), rewrites free variables in these templates
based on the computed bindings (lines 9 and 11), and then instruments the
rewritten statements into $P'$ (line 12). The update strategy is to first
subtract the old expression value (e.g., $\mathit{pre}$ in lines 8-9) before
the execution of $s$, and then add the new expression value (e.g.,
$\mathit{post}$ in lines 10-11) after the execution of $s$. See
Section~\ref{sec:design:binding} for our binding and rewrite algorithms.
For every quantifier constraint rule $r$, the algorithm also instruments the
declaration for a fresh state map variable $\alpha$. Note that because of the
\sourcecode{ForAll} quantifier, $r$ may correspond to multiple constraint instances. To
handle this, the algorithm inspects every store statement $s$ in $P$ and uses
its binding algorithm to determine whether the execution of $s$ may cause some
previously satisfied constraint instance of $r$ to be violated again. If so,
the algorithm sets the corresponding entry in $\alpha$ (lines 16-19) to mark
these instances. The algorithm finally instruments a \sourcecode{for} loop iterating
over $\alpha$ at the end of the contract to check these potentially violated
constraints (lines 21-24).
%{\systemname} uses an underlying parser to parse a smart contract
%source code into an abstract syntax tree. Given the standard
%specification, {\systemname} creates new state variables for
%statements with \sourcecode{sum} or \sourcecode{forall} aggregates.
%For \sourcecode{sum} aggregates, the types of state variables are
%determined using type inference rule described in Section~\ref{sec:design:type}.
%For \sourcecode{forall} aggregates, {\systemname} creates an array
%for each free variable used by the aggregate.
% For each constraint statement with a \sourcecode{forall} expression
% $\mathrm{constraint\;forall}(\vv{\mu},\bullet)$, {\systemname} creates a list of state
% variables $\vv{v}$ and each variable is an array that is used to store potential
% values of $\mu$.
%\noindent\textbf{Functions:} The algorithm uses following utility functions.
%\begin{itemize}
% \item \sourcecode{getLeftHandSide}($s$) returns the left hand side
% expression of an assignment statement.
% \item \sourcecode{isIndexing}($e$) returns true if the input expression
% is an indexing expression.
% \item \sourcecode{isVar}($e$) returns true if the input expression is
% a variable.
% \item \sourcecode{getObjectExpression}($e$) returns the object expression
% of the input indexing expression.
% \item \sourcecode{getIndexExpression}($e$) returns the index expression
% of the input indexing expression.
% \item \sourcecode{rewrite}($e, \psi$) takes a standard expression and
% a free variable mapping as input. It substitutes smart contract
% expressions for free variables in standard expression and returns
% a smart contract expression.
% \item \sourcecode{getStateVarFor}($\vv\mu$) takes a list of free
% variables as input and returns a list of state variables used to
% store the potential values of free variables.
% \item \sourcecode{createVar}() creates a smart contract temporary variable.
%\end{itemize}
\subsection{Binding and Rewrite Algorithms}
\label{sec:design:binding}
\begin{figure}[t]
\input{figures/binding.tex}
\caption{Binding algorithm.}
\label{fig:binding}
\end{figure}
\noindent\textbf{Free Variable Binding:}
Figure~\ref{fig:binding} presents our binding algorithm. It defines two
functions $\mathrm{BindExpr()}$ and $\mathrm{BindCond()}$ that are used in our
instrumentation algorithm (see Figure~\ref{fig:instrument}). Given a modified
address $a$ in a contract store statement and an expression $e$ in an invariant
rule, $\mathrm{BindExpr}(a, e)$ returns a set of binding maps that maps free
variables in $e$ to indexing expressions in $a$. To compute
$\mathrm{BindExpr}(a, e)$, {\systemname} recursively traverses the structure of
$e$ and looks for the map indexing expressions that match the state variable
in $a$. The fifth rule in Figure~\ref{fig:binding} creates a binding map for
such matching index expressions for the matching free variables.
Note that because $e$ is an expression from the invariant, it can have multiple
instantiations with different free variable assignments. Intuitively, a binding
map corresponds possible free variable assignments for $e$ that the state value
at the address $a$ may influence. Because one free variable may map to multiple
indexing expressions in a binding map, in our notation we represent the binding
map as a set of pairs of free variables and indexing expressions. For example,
$\mathrm{BindExpr}(a,e)=\{\{\langle x_1, e_1\rangle, \langle x_2,
e_2\rangle\}\}$ means that state value changes at the address $a$ may influence
the evaluation of the instantiations of $e$ in which we replace $x_1$ with
$e_1$ and $x_2$ with $e_2$. If $\mathrm{BindExpr}(a, e)$ returns a set that
contains multiple binding maps, it means that the state value changes at $a$
may influence instantiations that are represented by all of these maps.
Given a modified address $a$ and a condition expression $c$ in an invariant
rule, $\mathrm{BindCond(a, c)}$ returns a tuple pair of a free variable and an
expression. The instrumentation algorithm in Figure~\ref{fig:instrument} uses
$\mathrm{BindCond}()$ to handle intermediate value declaration rules only. The
computation of $\mathrm{BindCond()}$ scans for the condition of the form $e_1
== x$, where $x$ is a free variable. If an intermediate value declaration rule
has such a condition, {\systemname} can directly infer that the free variable
$x$ must equal to the expression $e_1$ for all cases.
%Maintaining the aggregates first requires {\systemname} to substitute free
%variables with smart contract expressions. The \sourcecode{bind} function
%described in Figure~\ref{fig:binding} represents the algorithm that maps all
%free variables of a standard statement $s_1$ to smart contract expressions of
%$s_2$. The function iterates over all sub-expressions of $s_1$ and calls
%\sourcecode{bindExpression} function respectively. A free variable $\mu$ is
%mapped to a smart contract expression $e$ if and only if they are index
%expression of both the same dimension and the same state variable, which is
%described in \sourcecode{buildExpression} function.
% Binding occurs between a standard statement $s_1$ and a smart
% contract statement $s_2$.
% The \sourcecode{bind} function stops if $e_1$ is
% not an indexing expression. Otherwise, the \sourcecode{bind} function
% traverses $e_2$ to find the corresponding indexing expression.
% Figure~\ref{fig:state-var} shows the algorithm that extracts the state
% variable used by the indexing expression.
% The mapping results are stored in the map $\psi$.
% Free variables with the same name should be mapped to the same smart contract
% expression and all free variables of an aggregate should be bound to
% after the binding.
\begin{algorithm}[t]
\input{figures/rewrite.tex}
\caption{The definition of $\mathrm{Rewrite}()$.}
\label{fig:rewrite}
\end{algorithm}
\noindent \textbf{Free Variable Rewrite:} Figure~\ref{fig:rewrite} presents the
definition of $\mathrm{Rewrite}()$. Given a statement template $s$ that may
contain free variables, a set of binding maps $\mathcal{B}$ extracted from
expressions with $\mathrm{BindExpr}()$, and a binding tuple $b$ extracted from
conditions with $\mathrm{BindCond}()$, $\mathrm{Rewrite}(s, \mathcal{B}, b)$
produces a new statement with all free variables being rewritten based on the
provided bindings.
The Rewrite algorithm iterates over binding maps in $\mathcal{B}$ and generates
one statement instantiation based on each binding map. For each free variable
in $s$, it detects whether it has exactly one appearance in the binding map. If
the free variable appears multiple times, i.e., the free variable maps to
multiple indexing expressions, the algorithm instruments additional \sourcecode{if}
statement guards to ensure that all of the matched indexing expressions have the
same value (line 7). The algorithm then removes redundant tuples and only keeps
one of these indexing expressions (line 8). If the free variable does not
appear in the binding map, the algorithm would wrap the statement with a
\sourcecode{for} loop to handle this missing binding and add a tuple that maps the
missing free variable to the iterator variable of the loop (lines 10-13).
Therefore, at line 14, the binding map $B'$ should map each free variable in $s$
exactly to each expression. The algorithm then replaces these free variables with
their corresponding expressions (lines 14-18).
%\noindent\textbf{Aggregates Instrumentation:}
%{\systemname} next traverses the AST of the smart contract and instruments all
%assignment statements where the value of a state variable is updated.
%Figure~\ref{fig:decorator} presents the psudo code for instrumenting a smart
%contract for an assignment statement $s$ and a list of standard statements $K$.
%The output of the function are instrumented statements $s$ and assertion
%statements $\alpha$. For each standard statement $s'$, if the updated state
%variable $v$ is used in $s'$ the \sourcecode{visit} function calls the
%\sourcecode{instrument} function to instrument the smart contract.
% the value of a state variable, the \sourcecode{visit} function
% iterates over all standard statements in $K$ and call
% \sourcecode{instrument} function if the updated variable is used in
%Figure~\ref{fig:rewrite} presents the instrumentation rules for
%different standard statements.
% $\alpha$ is a list of statements that
% Figure~\ref{fig:decorator} presents our rewrite rules that instruments
% the smart contract to maintain the state of the smart contract.
% $s'$ is a standard statement, $s$ is an assignment statement from
% smart contract, and $\alpha$ are smart contract statements checks whether
% the invariants of the standards are violated.
%For a \sourcecode{sum} statement, {\systemname} first builds a free
%variable mapping
%for $s'$ and substitutes free variables in $s'$. {\systemname} then
%creates two statements that deducts and increases $e_1'$ from
%$v\llbracket\vv\mu_1'\dot e_2'\rrbracket$ respectively, which
%updates the state variables used to track the status of the smart
%contract. Not that if the created statements contains assignment
%statements, {\systemname} will recursively instrument the generated
%statements as well.
%For a \sourcecode{forall} statement, {\systemname} does not check
%whether the constraints holds or not immediately. Instead,
%{\systemname} pushes the the values of the expressions that
%are mapped to free variables to the arrays $\vv v$ created for the
%\sourcecode{forall} statement. \sourcecode{push} is a utility function
%provided by the smart contract to push a value into an array.
%Besides, {\systemname} creates a for statement that iterates
%over all bindings of $\vv{\mu}$ and for each iteration, {\systemname}
%calls the \sourcecode{assert} function, a utility function
%that reverts the transaction if the condition fails. The for statement
%is appended to $\alpha$ to be executed when the transaction finishes.
%For a simple constraint statement, {\systemname} creates a statement
%that calls the \sourcecode{assert} function and append to $\alpha$.
% $s$
% with an assignment
% statement $s$. The function gets the state variable $v$ that is being
% updated and processes each aggregate $k$ which contains $s$. $pre$ and $post$ are
% two lists of AST nodes that stores the statements should be inserted before and after
% the statement $s$. For each aggregate $k$, the function calls function \sourcecode{bind}
% to bind all free variables in $k$ to smart contract expressions in $s.left$, which
% is the left hand side expression of the assignment statement.
% The function then calls $\mathrm{rewrite}$ function which replaces the free
% variables in aggregate expressions to smart contract expressions stored in $\psi$.
% If $k$ is a $\mathrm{forall}$ expression, {\systemname} does not check the
% assertions immediately. Instead, {\systemname} pushes values of free variables
% to the arrays of the \sourcecode{forall} expression and the assertions are checked
% when transaction finishes. $\mathrm{push}(x, y)$ is a utility function that
% pushes value $y$ to array $x$.
% Finally, the $\mathrm{visit}$ function visit the generated statements recursively
% and it calls \sourcecode{decorate} function if the AST node is an assignment statement.
%\noindent\textbf{Assertion Decoration:}
%\begin{algorithm}[t]
% \input{figures/constraint-collection.tex}
% \caption{Algorithm collects constraints to be added for each
% function.}
%\label{fig:constraint-collection}
%\end{algorithm}
%Remember the constraints are not checked immediately after any
%state variable inside the constraints are updated but
%they are checked when the transaction execution finishes. This avoids
%false positives because a constraint broken by an assignment statement
%may later be fixed by following assignment statements. Note that,
%unlike normal computer programs that only have a single
%entry point, smart contracts allows any public function
%to be the entry point, which requires {\systemname} to add assertions
%at the exit point of each public function. Besides, a public function
%may call other public functions defined in the smart contract, and
%the assertions of the callee function should be suppressed.
%Figure~\ref{fig:constraint-collection} represents the algorithm that
%collects a set of statements $\alpha$ should be executed when the
%function $f$ exists. {\systemname} first builds
%a call graph $G$ of the smart contract, it then performs the breadth
%first search along the call graph to collect influenced constraints
%of all predecessors of $f$.
%The function $\mathrm{getConstraints}$ returns the assertion statements
%$\alpha$ generated by \sourcecode{visit} function of each
%assignment statements of $f$. The function $predecessor$ takes a
%function $f'$ and call graph $G$ as input and returns a set of
%functions that call function $f'$.
% a set of constraints whose state variable has been updated by the
% assignment statements in $f$.
% Figure~\ref{fig:constraint-collection} presents the algorithm that
% translates a set of constraints $\kappa$ into a list of statements.
% If a constraint contains a simple arithmetic expression, {\systemname}
% creates an function call that calls the $\mathrm{assert}$ function.
% The $\mathrm{assert}(e)$ function is a utility function that
% reverts the transaction if the expression $e$ is not
% satisfied.
% The forall statement includes a
% function call that
% as well as a function call that
% calls \sourcecode{assert} function.
%{\systemname} adds the statements returned by the \sourcecode{collectAssertions}
%function at the exit points of each public function. Remember the constraints
%should only be checked when the transaction finishes but the function will check
%assertions every time it exists. In order to solve this issue, {\systemname}
%maintains a state variable $d$ to track the call depth of the current
%function call. $d$ increases when at the entry point of each function and
%decreases when the function exits. Added assertions will only be executed when
%the function exits and $d$ is zero.
\begin{displaymath}
\mathit{const}\in \mathrm{Int}\hspace{10mm}x, y\in \mathrm{FreeVar}
\hspace{10mm}v\in \mathrm{Var}
\end{displaymath}
\vspace{-6mm}
\begin{alignat*}{2}
e, e_1, e_2&\in \mathrm{Expr} := \mathit{const} \;|\;v \;|\;
v\llbracket x_1\rrbracket\llbracket x_2\rrbracket\llbracket\ldots\rrbracket \;|\; e_1 \; \mathbf{aop} \; e_2 \\
c, c_1, c_2& \in \mathrm{CondExpr} := e_1\; \mathbf{cop}\; e_2 \;|\;
e_1 == x \;|\; c_1 \wedge c_2 \\
r&\in \mathrm{Rule} := v=\text{Map } x_1,x_2,\ldots\; \text{Sum } e \\
&\qquad\qquad\qquad\;\;\; \text{Over } y_1, y_2, \ldots\; \text{Where } c;\;|\\
&\qquad\qquad\;\;\; \text{ForAll } x_1,x_2,\ldots\, \text{Assert } e;\;|\; r_1 r_2
\end{alignat*}
\begin{displaymath}
c\in \mathrm{Int} \hspace{10mm}
v, v_1\in \mathrm{StateVar}\hspace{10mm}
t, t_1\in \mathrm{TempVar}
\end{displaymath}
\vspace{-6mm}
\begin{alignat*}{2}
a, a_1&\in \mathrm{Address} := v \;|\; v\llbracket{e_1}\rrbracket\llbracket{e_2}\rrbracket\llbracket{\ldots}\rrbracket\\
e, e_1, e_2&\in \mathrm{Exp} := c \;|\;t \;|\; e_1 \;\mathbf{op}\; e_2 \\
s, s_1, s_2&\in \mathrm{Statement} := t = e; \;|\; s_1 s_2 \;|\; t = \text{load } a; \;|\;\text{store } a, \; e; \; | \;\\
&\quad\quad\quad\quad\quad\quad\quad \text{if } \; e \; \{s_1\} \;|\; \text{for } \; t_1, t_2, \ldots \; \text{ in } v \; \{ s_1 \} \; | \; \\
&\quad\quad\quad\quad\quad\quad\quad \text{assert } \; e; \;
\end{alignat*}
\SetEndCharOfAlgoLine{}
\Input{Program $P$ as a list of statements and a list of invariant rules $R$}
\Output{The instrumented program as a list of statements}
$P' \leftarrow P$\;
\For {$r \in R$} {
\If {$r = ``v = \text{Map }\vv{x}\text{ Sum } e \text{ Over }\vv{y} \text{ Where } c;"$} {
Assume $v$ is fresh. Insert a declaration of $v$ in $P'$.\;
\For {$s = ``\text{store } a, \_;" \in P$} {
$\mathcal{B} \leftarrow \mathrm{BindExpr}(a, e) \cup \mathrm{BindExpr}(a, c)$\;
$b \leftarrow \mathrm{BindCond}(a, c)$\;
$\mathit{pre} \leftarrow ``\text{if }c \; \{ \;
t = \text{load }v\llbracket\vv{x}\rrbracket;$
$t' = t - e;
\text{store }v\llbracket\vv{x}\rrbracket, t';\}"$\;
$\mathit{pre} \leftarrow \mathrm{Rewrite}(\mathit{pre}, \mathcal{B}, b)$\;
$\mathit{post} \leftarrow ``\text{if }c \; \{ \;
t = \text{load }v\llbracket\vv{x}\rrbracket;$
$t' = t + e;
\text{store }v\llbracket\vv{x}\rrbracket, t';\}"$\;
$\mathit{post} \leftarrow \mathrm{Rewrite}(\mathit{post}, \mathcal{B}, b)$\;
Insert $\mathit{pre}$ before $s$ and insert $\mathit{post}$ after $s$ in $P'$\;
}
}
\ElseIf {$r=``\text{ForAll }\vv{x} \text{ Assert } c;"$} {
Declare a fresh map $\alpha$ in $P'$ corresponding to $r$\;
\For {$s = ``\text{store } a, \_" \in P$} {
$\mathcal{B} \leftarrow \mathrm{BindExpr}(a, c)$\;
$\mathit{pre} \leftarrow ``\alpha\llbracket \vv{x} \rrbracket = 1"$\;
$\mathit{pre} \leftarrow \mathrm{Rewrite}(\mathit{pre}, \mathcal{B}, \langle \bot, \bot \rangle)$\;
Insert $\mathit{pre}$ before $s$ in $P'$\;
}
}
$P \leftarrow P'$\;
}
\For {$r=``\text{ForAll } \vv{x} \text{ Assert } c;" \in R$} {
$\alpha \leftarrow \text{The defined map that corresponds to }r$\;
$s' \leftarrow ``\text{for } \vv{x} \text{ in } \alpha \; \{ \; \text{assert }c; \; \} \;"$\;
Insert $s'$ at the end of $P'$\;
}
\Return $P'$\;
\small
\begin{mathpar}
\inferrule{
\mathit{const} \in \text{Int}
}{
\mathrm{BindExpr}(a, \mathit{const}) = \emptyset
}\and
\inferrule{
a = v
}{
\mathrm{BindExpr}(a, v) = \{\emptyset\}
}\and
\inferrule{
a = v' \\
v' \neq v
}{
\mathrm{BindExpr}(a, v) = \emptyset
}\and
\inferrule{
a = v'\llbracket \ldots\rrbracket \\
e = v\llbracket \ldots\rrbracket \\
v' \neq v
}{
\mathrm{BindExpr}(a, v) = \emptyset
}\and
\inferrule{
a = v\llbracket x_1\rrbracket \llbracket \ldots \rrbracket \llbracket x_k \rrbracket \\
e = v\llbracket e_1\rrbracket \llbracket \ldots \rrbracket \llbracket e_k \rrbracket
}{
\mathrm{BindExpr}(a, v) = \{\{\langle x_1, e_1\rangle, \ldots, \langle x_k, e_k\rangle\}\}
}\and
\inferrule{
e = e_1 \; \mathbf{ aop } \; e_2
}{
\mathrm{BindExpr}(a, e) = \mathrm{BindExpr}(a, e_1) \cup \mathrm{BindExpr}(a, e_2)
}\and
\inferrule{
c = e_1 \; \mathbf{ cop } \; e_2
}{
\mathrm{BindExpr}(a, c) = \mathrm{BindExpr}(a, e_1) \cup \mathrm{BindExpr}(a, e_2) \\
\mathrm{BindCond}(a, c) = \emptyset
}\and
\inferrule{
c = ``e_1 == x" \\ e_1 \text{ contains } x
}{
\mathrm{BindExpr}(a, c) = \mathrm{BindExpr}(a, e_1) \\
\mathrm{BindCond}(a, c) = \langle \bot, \bot \rangle
}\and
\inferrule{
c = ``e_1 == x" \\ e_1 \text{ does not contain } x
}{
\mathrm{BindExpr}(a, c) = \mathrm{BindExpr}(a, e_1) \\
\mathrm{BindCond}(a, c) = \langle x, e_1 \rangle
}\and
\inferrule{
c = ``c_1 \wedge c_2" \\ \mathrm{BindCond}(a, c_1) \neq \langle \bot, \bot \rangle
}
{
\mathrm{BindExpr}(a, c) = \mathrm{BindExpr}(a, c_1) \cup \mathrm{BindExpr}(a, c_2) \\
\mathrm{BindCond}(a, c) = \mathrm{BindCond}(a, c_1)
}\and
\inferrule{
c = ``c_1 \wedge c_2" \\ \mathrm{BindCond}(a, c_1) = \langle \bot, \bot \rangle
}
{
\mathrm{BindExpr}(a, c) = \mathrm{BindExpr}(a, c_1) \cup \mathrm{BindExpr}(a, c_2) \\
\mathrm{BindCond}(a, c) = \mathrm{BindCond}(a, c_2)
}
\end{mathpar}
\SetEndCharOfAlgoLine{}
\Input{The original statement $s$, a set of binding maps $\mathcal{B}$ extracted from expressions, and a binding $b$ extracted from conditions.}
\Output{The rewritten statement respecting the bindings.}
$s' \leftarrow \emptyset$\;
\For {$B \in \mathcal{B}$} {
$s'' \leftarrow s$\;
$B' \leftarrow B \cup \{b\}$\;
\For {$x \in \text{FreeVar}, \text{where }$x$\text{ appears in }s$} {
\If {$x$ appears in $B'$ multiple times as $\langle x, e_1 \rangle, \ldots \langle x, e_k \rangle$} {
$s'' \leftarrow ``\text{if } \;e_1 == e_2 \wedge \ldots \wedge e_1 == e_k \; \{ s'' \}"$\;
$B' \leftarrow B' - \{\langle x, e_2 \rangle, \ldots, \langle x, e_k \rangle\}$\;
}
\ElseIf {$x$ does not appear in $B'$} {
Create a fresh variable $t$\;
Find $v$ in $s$, where $x$ is used as its index\;
$s'' \leftarrow ``\text{for } \; t \text{ in } v \; \{ s'' \}"$\;
$B' \leftarrow B' \cup \{\langle x, t \rangle\}$\;
}
}
\If {$b=\langle x', e'\rangle \land x' \neq \bot$} {
$s'' \leftarrow s''[x'/e']$\;
$B' \leftarrow B' - \{b\}$\;
}
\For {$\langle x, e \rangle \in B'$} {
$s'' \leftarrow s''[x/e]$\;
}
$s' \leftarrow s' s''$\;
}
\Return $s'$\;
\section{Implementation}\label{sec:impl}
We implement {\systemname} for Solidity smart contracts. We use
Antlr~\cite{antlr} and the Solidity parser~\cite{solidity-parser} to parse standard
specifications and Solidity programs. {\systemname} extends the language
described in Section~\ref{sec:design} to support all Solidity features
including contract function calls.
\subsection{Function Calls}\label{sec:impl:call}
Because state variables are often updated sequentially in a
transaction, and the invariant may be temporarily violated during the middle of
the transaction, {\systemname} should only check the constraints at the end of
each transaction. For function calls, simply inserting those checks
at the end of each function may cause those checks to be triggered multiple
times during a transaction and result in false positives. To this end,
{\systemname} declares an additional global state variable to track the current
function call stack depth of the execution. The instrumented constraint checks
will only execute if it is the entry function of the transaction (i.e., the
stack depth is one).
{\systemname} uses Surya~\cite{surya} to build the call graph of the smart
contract. With the call graph information, {\systemname} can obtain the set of
functions that are reachable from an entry function. For each function,
{\systemname} prunes away instrumented checks for constraints whose status will
never change if the function is the entry function. Specially, smart contracts
in Ethereum can call functions defined in other smart contracts. To guarantee
correctness, {\systemname} over estimates that the inter-contract calls
will call back any function defined inside the contract.
%This implies that {\systemname} needs to create statements to check all
%constraints for functions that has inter-contract function calls. Moreover,
%{\systemname} uses state variables instead of global memory mentioned in
%Section~\ref{sec:impl:global-memory} to store arrays for ``ForAll'' expressions
%because memory are not shared between inter-contract calls.
\subsection{Global Memory}\label{sec:impl:global-memory}
\begin{figure}[t]
\inputminted{JavaScript}{./code/global-memory.sol}
\caption{Inline assembly to initialize or load a global array.}
\label{code:global-memory}
\end{figure}
{\systemname} uses global memory arrays to store free variable bindings for
\sourcecode{ForAll} constraint rules (line 10-11, 14-15, and 19-20 in
Figure~\ref{code:vote_secured}). It uses the global memory rather than the
intra-procedure volatile memory or the blockchain state because 1) a
transaction may contain multiple functions and the instrumented code of these
functions all need to access these arrays and 2) accessing global memory is
cheaper than accessing the blockchain state.
Since the global memory array is not natively supported by Solidity,
{\systemname} uses inline assembly to allocate the in-memory array as well as
assigning the start location of the array to an array pointer.
Figure~\ref{code:global-memory} presents the generated global array of
\sourcecode{x\_arr} in Figure~\ref{code:vote_secured}. \sourcecode{x\_slot} is
a state variable stores the start location of \sourcecode{x\_arr} and
\sourcecode{x\_arr} is the array pointer. {\systemname} only initializes
\sourcecode{x\_arr} when the transaction starts and sets the \sourcecode{x\_arr}
to the value of \sourcecode{x\_slot} directly if the call depth is not zero.
{\systemname} further uses \sourcecode{mload} and \sourcecode{mstore}
instructions to load and store data from/to array.
%The memory is shared across
%multiple functions, which prevents {\systemname} from modifying function
%signatures. Using memory is more efficient than persistent storage because
%loading/storing values from/to memory only requires a single instruction.
%Similar to the issue mentioned in Section~\ref{sec:variable-cache},
%{\systemname} generates lots of dynamic array operations to store free
%variables bindings for the \sourcecode{forall} expression (line 10-11, 14-15,
%and 19-20 in Figure~\ref{code:vote_secured}). This is because only state
%variables can be shared across functions. One native solution is to pass arrays
%as a function parameter, which requires {\systemname} to modify the function
%signature. To implement this, {\systemname} needs to duplicate each function.
%One function is the same as the origin function. The other function takes a few
%more parameters as the input which are the arrays. However, it will increase
%the size of the smart contract dramatically, and may cause side effects of the
%smart contract.
%{\systemname} solves the problem by creating a global array inside memory every
%time the transaction starts. Since the global array is not natively supported
%by Solidity, {\systemname} uses inline assembly to allocate the in-memory array
%as well as assigning the start location of the array to an array pointer.
%Figure~\ref{code:global-memory} presents the generated global array of
%\sourcecode{x\_arr} in Figure~\ref{code:vote_secured}. \sourcecode{x\_slot} is
%a state variable stores the start location of \sourcecode{x\_arr} and
%\sourcecode{x\_arr} is the array pointer. {\systemname} only initialize
%\sourcecode{x\_arr} when the transaction starts and set the \sourcecode{x\_arr}
%to the value of \sourcecode{x\_slot} directly if the call depth is not zero.
%{\systemname} further uses \sourcecode{mload} and \sourcecode{mstore}
%instructions to load and store data from/to array. The memory is shared across
%multiple functions, which prevents {\systemname} from modifying function
%signatures. Using memory is more efficient than persistent storage because
%loading/storing values from/to memory only requires a single instruction.
\subsection{State Variable Caches}\label{sec:variable-cache}
As an optimization, {\systemname} uses stack or volatile memory in Solidity to
cache state variable values. Our second observation in
Section~\ref{sec:observation} indicates that blockchain state load/store
operations are very expensive, involving disk I/O, cryptographic computations, and
multiple EVM instructions. On the other hand, loading/storing values from/to
stack or memory only requires a single instruction.
%The overhead introduced by state variable operations is amplified
%after the smart contract is instrumented because state variables are created
%for both \sourcecode{sum} and \sourcecode{forall} aggregates.
{\systemname} performs static analysis to determine whether the same
blockchain state value is accessed multiple times in a function. For every such
value, {\systemname} creates a temporary variable to cache it. If multiple
functions can access the state value, {\systemname} will create the temporary
variable in the global memory and will use the technique similar to
Section~\ref{sec:impl:global-memory} to enable all functions to access it.
Otherwise, {\systemname} creates the temporary variable in the stack. At the
end of the function, {\systemname} instruments code to write back cached values
to the state variable. This enables the optimized code to only execute one state load
operation and one state store operation for such a state value. Note that the
optimized code is equivalent to the original code because in Ethereum, all
transactions are executed sequentially, i.e., the blockchain state can only be
read/written by a single transaction at one time.
%State variable operations of dynamic allocated variables such as mapping and
%dynamic array variables are expensive in Solidity smart contracts. To access a
%dynamic allocated mapping variable, Solidity compiler first pushes a global
%slot index and the mapping index of the variable to the stack. It then stores
%the stack values to the memory so that the crypto hash function could load the
%data from the memory and compute the storage address of the variable. The
%latest implementation of Solidity compiler\footnote{v0.5.9} generates 11
%instructions for a single state variable operation. On the other hand,
%loading/storing values from/to stack or memory only requires a single
%instruction. The overhead introduced by state variable operations is amplified
%after the smart contract is instrumented because state variables are created
%for both \sourcecode{sum} and \sourcecode{forall} aggregates.
%In order to mitigate the overhead introduced by state variable operations.
%{\systemname} takes benefits of the design of Ethereum blockchain system,
%that all transactions are executed sequentially, the persistent storage can
%only be read/written by a single transaction at one time. This allows
%{\systemname} to cache state variables to stack and memory and
%state variable operations are redirected to cache variables. {\systemname}
%performs this optimization conservatively and stores cache variables
%back to storage right after operation finishes, which avoids the race condition
%when the state variable is updated by other functions.
\begin{figure}[t]
\inputminted{JavaScript}{./code/examples/vote_state_opt.sol}
\caption{Vote function with state variable caches.}
\label{code:var-cache}
\end{figure}
\sloppypar{
Figure~\ref{code:var-cache} presents the code after the state variable cache
optimization of lines 14-21 from \sourcecode{vote} in
Figure~\ref{code:vote_secured}. {\systemname} creates two cache variables
\sourcecode{opt\_13} and \sourcecode{opt\_14} for state variable
\sourcecode{ballots[issueId][msg.sender]} and
\sourcecode{weights[issueId][msg.sender]} (line 1-2). And the operations of
those two state variables are replaced by cache variables. Note that not all
state variables can be cached. For example, {\systemname} does not cache the
state variable \sourcecode{sum\_votes[issueId][opt\_13]} in line 6 because
\sourcecode{opt\_13} is updated in line 7 and the state variable in line 10 is
represents a different state variable. {\systemname} then stores
\sourcecode{opt\_13} back to \sourcecode{ballots[issueId][msg.sender]}.
\sourcecode{opt\_14} is not stored because its value is not updated.
}
% and cache
% variables are stored back to storage after the operations finish.
% The system later stores those cached variables to persistent storage after
% execution finishes.
% Figure~\ref{fig:cache} shows the statements of sum expression
% after cache optimization. $tmp$ is a temporary variables allocated on the stack,
% which stores the value of $v_{\vv{\mu_1}[M]A_2[M]}$. For the rest operations,
% the contract reads/writes the values from/to $tmp$, which avoids accessing
% persistent storage multiple times. {\systemname} creates a temporary variable
% for dynamic allocated storage variable $v$.
\section{Evaluation}\label{sec:results}
We next evaluate {\systemname} on three representative standards:
ERC20~\cite{erc20} for the fungible token standard, ERC721~\cite{erc721} for the
non-fungible token standard, and ERC1202~\cite{erc1202} for the voting standard.
The goal of this evaluation is to measure the overhead introduced by runtime
validation and to understand the effectiveness of the {\systemname}
instrumentation optimizations. All experiments were performed on an AWS EC2
m5.xlarge virtual machine, which has 4 cores and 16GB RAM. We downloaded and
modified Parity v2.6.0~\cite{parity} as the Ethereum client to run our
experiments.
% Since the block generation speed is not determinable in current Ethereum blockchain
% system, we download and modified Parity~\cite{parity}, the most efficient
% Ethereum blockchain system, so that we can pack a specific number of blocks
% at a fixed speed.
\subsection{Methodology}\label{sec:results:methodology}
\noindent\textbf{Benchmark Contracts:} We collected 10 popular ERC20 and ERC721
smart contracts from EtherScan~\cite{etherscan}. To evaluate the effectiveness
of {\systemname}, we also include BecToken (an ERC20 contract) and DozerDoll
(an ERC721 contract), two contracts that we successfully collect their history
transactions from Ethereum. We further include the ERC1202 example we described
in Section~\ref{sec:example} in our benchmark set.
Note that BECToken implements a customized function,
\sourcecode{batchTransfer}, which has an integer overflow error and violates
the total supply invariant specified by ERC-20 standard. This error was
exploited in 2018 and the market cap of BECToken was evaporated in
days~\cite{bec}. The ERC1202 example has vulnerabilities which we described in
Section~\ref{sec:example}. In our experiments, {\systemname} successfully
nullify errors in both of these contracts. We validate that the instrumented
contracts reject our crafted malicious transactions.
\noindent\textbf{Standard Specifications:} We specify invariants for ERC20,
ERC721, and ERC1202 respectively using the language described in
Section~\ref{sec:design}. ERC1202 is a smart contract standard for implementing
a voting contract. The example in the ERC1202 standard draft unfortunately
contains logic errors. See Section~\ref{sec:example} for details.
%The existing standard only specifies a list of
%interfaces that should be implemented, and defines a few constraints verbally.
%For example, the ERC1202 standard requires that for all issues, the weighted vote
%counts of each option should equal to the sum of weights of voters who voted for that
%option. Since, the weight of each voter, vote of each voter, and weighted vote
%counts of each option are all stored in state variables in the example voting
%contract, we further look into the implementation of the smart contract to find
%corresponding state variables.
\begin{figure}[t]
\inputminted{JavaScript}{./code/examples/bec.txt}
\caption{Standard for ERC20.}
\label{code:erc20}
\end{figure}
\begin{figure}[t]
\inputminted{JavaScript}{./code/examples/kc.txt}
\caption{Standard for ERC721.}
\label{code:erc721}
\end{figure}
\noindent\textbf{ERC20:}
ERC20 is an important smart contract standard that defines the contract
interface and specification of implementing fungible digital assets.
Figure~\ref{code:erc20} shows the invariant for ERC20 standard.
\sourcecode{balances} and \sourcecode{totalSupply} are two state variables in
BECToken that store the balance of each address and the total supply of the
token. The invariant specifies that the sum of account balances is equal to
total supply.
\noindent\textbf{ERC721:} Similar to ERC20, ERC721 is a smart contract standard
of implementing non-fungible digital assets. Figure~\ref{code:erc721} shows
our invariant for the ERC721 standard. \sourcecode{sum\_tokenCount} and
\sourcecode{sum\_ownersToken} are two intermediate variables created by the invariant
to track the state of the contract. \sourcecode{sum\_tokenCount} stores the
number of minted tokens, which is the number of tokens whose owner is not 0, and
\sourcecode{sum\_ownersToken} stores the number of tokens owned by each
address. The invariant specifies that \sourcecode{sum\_tokenCount} equals to the
length of \sourcecode{\_allTokens}, and the number of tokens owned by each user
equals to the values stored in \sourcecode{\_ownedTokensCount}.
\sourcecode{\_allTokens} and \sourcecode{\_ownedTokensCount} are two state
variables declared in ERC721 smart contracts.
%\noindent\textbf{ERC1202:} ERC1202
%is a smart contract standard for implementing a voting contract.
%See Section~\ref{sec:example} for details.
%Figure~\ref{code:erc1202} shows constraints for ERC1202 standard, which
%specifies that the sum of votes for each option equals to the sum of weights of
%users whose vote is that option. ERC1202Example is an example voting contract
%provided by the authors of ERC1202. As described in Section~\ref{sec:example},
%there is an implementation error in the \sourcecode{vote} function which allows
%a user to vote the option multiple times and the {\systemname} protects the
%voting contract from such attacks by adding runtime checks.
\noindent\textbf{Benchmark Trace Generation:}
We crawled the Ethereum blockchain and collected the real transaction history
of BecToken and DozerDoll. We chose BecToken because its history contains
attacks. We chose DozerDoll because it is an ERC721 token, and it has a long
transaction history for our experiments. Note that the collected history
transactions depend on the blockchain state (e.g., the token balance of
accounts), so we cannot reproduce them directly. To address this issue, we
first create a mapping that maps real world addresses to local addresses that
are managed by the Parity client. For each transaction, we replaced the
addresses of the transaction sender and receiver, as well as addresses in
transaction data.
For the remaining contracts, we developed a script to automatically generate random
transaction traces that exercise core functionalities of ERC20, ERC721, and
ERC1202. For ERC20 and ERC721, the generated trace contains mainly
\sourcecode{transfer} transactions. For ERC1202, the generated trace contains
transactions that call \sourcecode{createIssue} and \sourcecode{vote} functions
repeatedly. Each \sourcecode{createIssue} transaction is accompanied by five
\sourcecode{vote} transactions created by different voters respectively.
\noindent\textbf{Experiments with PoW Consensus:}
We apply {\systemname} to instrument all of the 23 benchmark contracts. We then
run Parity 2.6.0 to start a single node Ethereum network to measure the
overhead of instrumented contracts. For BecToken and DozerToken, we use the
collected Ethereum history trace. For the ERC1202 example contract and other
contracts, we use the generated trace. To run a contract on a transaction
trace, we initialize the network with the first 5,052,259 blocks downloaded
from Ethereum main net. We then feed the transactions in the trace into the
network.
In this experiment, we deploy the same smart contract to the blockchain
multiple times and take the average results. To address the randomness of the
PoW consensus process, we modified Parity client so that Parity generates new
blocks at a fixed speed of 1 block per ten seconds, which is the generation
speed upper bound Ethereum ever reaches with its difficulty adjustment
mechanism. Note the gas usage for each transaction is set to the gas usage of
executing the original smart contract, which allows Parity to pack the same
number of transactions for both the instrumented and the original smart
contract. We set the block gas limit to 8,000,000. We monitor the CPU usage and disk
IOs of the Parity client for 500 blocks (\textasciitilde 1.4 hours). Because
the consensus is the performance bottleneck and there is no throughput
difference between the original contracts and the instrumented contracts, we
measure the resource consumption as the instrumentation overhead in this set of
experiments.
%In this experiment, we deploy the same smart contract to the blockchain
%multiple times and take the average results.
%For each transaction, we duplicate the transaction
%and send different transactions to different smart contracts until the sum of
%gas usage of those transactions exceeds 10,000,000, which is the block
%gas limit of the current Ethereum main net~\cite{gas_limit}.
%Note the gas usage for each transaction is set to the gas usage of executing
%the original smart contract, which allows Parity to pack the same number of
%transactions for both the instrumented and the original smart contract.
%Next,
%we submit those transactions to the Parity client, where the transactions are
%executed, packed into a block, and stored in persistent storage in succession.
%We also modified Parity client so that Parity generates new blocks at a fixed
%speed of 1 block per ten seconds. We monitor the CPU usage and disk IOs of the
%Parity client for 500 blocks (\textasciitilde 1.4 hours).
\noindent\textbf{Experiments without PoW Consensus:}
We modified the Parity client to remove the proof of work consensus, but
preserved all required computations and storage operations for the transaction
execution. To evaluate the potential overhead of {\systemname} when the
consensus is no longer the performance bottleneck, we apply {\systemname} to
instrument all benchmark contracts and run the modified Parity client to
measure the overhead. To evaluate the {\systemname} instrumentation
optimizations, we also run naively instrumented contracts that iteratively
check invariants at the end of transactions for comparison. Specifically, we
compare the transaction throughput of the original contracts and the
instrumented contracts. Note that similar to the previous set of experiments,
we initialize the Parity client with the first 5,052,259 blocks from the
Ethereum main net.
%\noindent\textbf{Benchmark Selection:}
%We produced 6 benchmarks in total, 3 benchmarks for BECToken, 2 benchmarks
%for DozerDoll, and 1 benchmark for ERC1202Example. Two benchmarks
%are real world transactions downloaded from Ethereum blockchain system.
%We first create a mapping that maps real world addresses to local addresses
%that managed by Parity client. For each transaction, we replaced the address
%of transaction sender and receiver, as well as addresses in transaction data.
%The rest four benchmarks include synthesized transactions which call the
%most important functions of each contract.
%\begin{itemize}
% \item \textbf{BEC-REP} contains real world transactions sent to BECToken.
% The first 2,000 transactions contain 820 \sourcecode{transfer} transactions,
% 1143 \sourcecode{batchTransfer} transactions, 3 \sourcecode{approve}
% transactions, and 34 reverted transactions.
% \item \textbf{BEC-TRAN} contains transactions that call
% \sourcecode{transfer} function.
% \item \textbf{BEC-BAT} contains transactions that call
% \sourcecode{batchTransfer} function.
% \item \textbf{DOZ-REP} contains real world transactions sent to DozerDoll.
% The first 2,000 transactions contain 17 \sourcecode{transferAll} transactions, 1982
% \sourcecode{mintUniqueTokenTo} transactions, and 1 invalid transaction.
% \item \textbf{DOZ-TRAN} contains transactions that calls
% \sourcecode{mintUniqueTokenTo} and \sourcecode{transfer} function
% repeatedly.
% \item\textbf{VOTE} contains transactions that calls \sourcecode{createIssue}
% and \sourcecode{vote} function repeatedly. Each \sourcecode{createIssue}
% transaction is accompanied by five \sourcecode{vote} transactions create
% by different voter respectively.
%\end{itemize}
%Figure~\ref{fig:func} presents the summary of each functions used in the experiment.
%The first and the second columns describe the contract name and the function name
%respectively.
%For the third to the fifth columns, each column describes an attribute of
%the function. \textbf{DynVar} represents that the function updates a
%dynamic allocated state variable that is used in the standard;
%\textbf{MuArr} represents that the
%function requires an array to stores all possible $\vv{\mu}$ bindings for a
%\sourcecode{forall} expression in the standard;
%\textbf{Call} represents the function calls other functions.
\if 0
\begin{figure*}[t]
\begin{center}
\begin{tabular}{ |c|c|c|c|c|c|c|c| }
\hline
\textbf{Contract}& \textbf{Function} & \textbf{DynVar} & \textbf{MuArr}& \textbf{Call} \\
\hline
BEC & \sourcecode{transfer}& x & & \\
\cline{2-5}
& \sourcecode{batchTransfer}& x & & \\
\cline{2-5}
& \sourcecode{approve}& & & \\
\hline
VOTE & \sourcecode{createIssue}& x & x & \\
\cline{2-5}
& \sourcecode{vote}& x & x & \\
\hline
DOZ& \sourcecode{mintUniqueTokenTo}& x & x & x \\
\cline{2-5}
& \sourcecode{transfer}& x & x & x \\
\cline{2-5}
& \sourcecode{transferAll}& x & x & x \\
\hline
\end{tabular}
\end{center}
\caption{Summary of each function.}
\label{fig:func}
\end{figure*}
\fi
\noindent\textbf{\textbf{}}
%\noindent\textbf{Blockchain Configuration:}
%We use {\systemname} to generate both optimized
%and non-optimized instrumented smart contracts in order to measure the
%effectiveness of optimizations.
%We modified Parity client
%which preserves all required computations and storage operations but
%removes consensus verifications as well as proof of works. This allows
%us to monitor the performance of Parity client of processing arbitrary
%transactions. Besides, experiments are carried under two different
%blockchain settings:
%\begin{itemize}
% \item \textbf{Empty} is an empty blockchain and only contains the
% genesis block.
% \item \textbf{Main Net} contains the first 5,052,259 blocks
% downloaded from Ethereum main net.
%\end{itemize}
\begin{figure*}[t]
\begin{center}
\begin{tabular}{ |c|c|c|c|c|c|c|c|c|c|c|c|c| }
\hline
& & \textbf{BEC} & \textbf{USDT} & \textbf{ZRX} & \textbf{THETA} & \textbf{INB}
& \textbf{HEDG} & \textbf{DAI} & \textbf{EKT} & \textbf{XIN} & \textbf{HOT} & \textbf{SWP} \\
\hline
\textbf{CPU}& \textbf{S}& 3.11& 3.31& 3.12& 3.11& 3.04& 3.34& 3.13& 3.13& 3.09& 3.29& 3.32 \\
\cline{2-13}
\textbf{(\%)}& \textbf{O}& 3.11& 2.99& 3.02& 3.10& 3.02& 3.14& 3.09& 2.92& 3.08& 3.04& 3.12 \\
\hline
\textbf{Disk}& \textbf{S}& 96.8 & 97.4& 96.4& 96.3& 96.7& 97.0& 96.5& 96.6& 96.2& 96.6& 96.7 \\
\cline{2-13}
\textbf{(KB/s)}& \textbf{O}& 96.6 & 96.6& 96.1& 96.2& 96.5& 96.8& 96.3& 96.1& 96.1& 96.2& 96.6 \\
% \textbf{Average CPU}& \textbf{S} & 0.912\% & 1.642\% & 1.491\%
% & 1.423\%& 0.818\%& 0.952\%\\
% \cline{2-8}
% \textbf{Usage}& \textbf{S-N} & 1.072\% & 1.642\% & 1.656\%
% & 1.525\%& 0.850\%& 1.013\%\\
% \cline{2-8}
% & \textbf{O} & 0.896\% & 1.642\% & 1.457\%
% & 1.319\%& 0.799\%& 0.933\%\\
\hline
\end{tabular}
\end{center}
\begin{center}
\begin{tabular}{ |c|c|c|c|c|c|c|c|c|c|c|c|c|c| }
\hline
& & \textbf{DOZ} & \textbf{MCHH} & \textbf{CC} & \textbf{CLV} & \textbf{LAND} & \textbf{CARDS}
& \textbf{KB} & \textbf{TRINK} & \textbf{BKC} & \textbf{PACKS} & \textbf{EGG} & \textbf{VOTE}\\
\hline
\textbf{CPU}& \textbf{S}& 1.97& 1.99& 1.98& 1.95& 1.89& 1.92& 1.89& 1.90& 1.94& 1.93& 2.04& 2.81 \\
\cline{2-14}
\textbf{(\%)}& \textbf{O}& 1.83& 1.80& 1.91& 1.94& 1.81& 1.77& 1.83& 1.79& 1.91& 1.86& 1.82& 2.51 \\
\hline
\textbf{Disk}& \textbf{S}& 85.7 & 77.5& 73.9& 77.9& 77.7& 76.2& 75.9& 76.9& 80.6& 74.6& 76.4& 83.4 \\
\cline{2-14}
\textbf{(KB/s)}& \textbf{O}& 74.5 & 68.2& 72.2& 69.5& 68.8& 69.5& 66.6& 67.9& 75.3& 70.5& 69.6& 71.1 \\
\hline
\end{tabular}
\end{center}
\caption{Resources usage for Parity client. ``S'' corresponds to {\systemname} results. ``O'' corresponds to original contract result.}
\label{fig:cpu}
\end{figure*}
\if 0
\begin{figure*}[t]
\begin{center}
\begin{tabular}{ |c|c|c|c|c|c|c|c| }
\hline &
& \textbf{BEC-REP} & \textbf{BEC-TRAN}& \textbf{BEC-BAT}
& \textbf{VOTE} & \textbf{DOZ-REP}& \textbf{DOZ-TRAN} \\
\hline
\textbf{Average CPU}& \textbf{S}& 0.846\%& 1.973\%& 1.743\%& 1.564\%& 0.860\%& 1.248\%\\
\cline{2-8}
\textbf{Usage}& \textbf{S-N}& 0.943\%& 1.954\%& 2.061\%& 1.765\%& 0.981\%& 1.274\%\\
\cline{2-8}
\textbf{(Empty)}& \textbf{O}& 0.879\%& 1.909\%& 1.681\%& 1.429\%& 0.859\%& 1.125\%\\
\hline
\textbf{Data Writes}& \textbf{S}& 0.14 & 0.16 & 0.12 & 0.25 & 0.18 & 0.16 \\
\cline{2-8}
\textbf{(GB)}& \textbf{S-N}& 0.14 & 0.16 & 0.12 & 0.24 & 0.18 & 0.16 \\
\cline{2-8}
\textbf{(Empty)}& \textbf{O}& 0.13 & 0.14 & 0.12 & 0.18 & 0.14 & 0.14 \\
\hline
\hline
\textbf{Average CPU}& \textbf{S}& 1.534\%& 3.373\%& 2.938\%& 2.810\%& 1.661\%& 2.298\%\\
\cline{2-8}
\textbf{Usage}& \textbf{S-N}& 1.515\%& 3.550\%& 2.954\%& 3.054\%& 1.685\%& 2.252\%\\
\cline{2-8}
\textbf{(Main Net)}& \textbf{O}& 1.446\%& 3.142\%& 2.895\%& 2.508\%& 1.681\%& 2.110\%\\
\hline
\textbf{Data Writes}& \textbf{S}& 0.21 & 0.29 & 0.27 & 0.41 & 0.29 & 0.26 \\
\cline{2-8}
\textbf{(GB)} & \textbf{S-N}& 0.21 & 0.29 & 0.27 & 0.41 & 0.29 & 0.26 \\
\cline{2-8}
\textbf{(Main Net)}& \textbf{O}& 0.21 & 0.29 & 0.26 & 0.35 & 0.27 & 0.24 \\
% \textbf{Average CPU}& \textbf{S} & 0.912\% & 1.642\% & 1.491\%
% & 1.423\%& 0.818\%& 0.952\%\\
% \cline{2-8}
% \textbf{Usage}& \textbf{S-N} & 1.072\% & 1.642\% & 1.656\%
% & 1.525\%& 0.850\%& 1.013\%\\
% \cline{2-8}
% & \textbf{O} & 0.896\% & 1.642\% & 1.457\%
% & 1.319\%& 0.799\%& 0.933\%\\
\hline
\end{tabular}
\end{center}
\caption{Resource usage for top ERC20, ERC721, ERC1202 contracts on the Parity client.}
\label{fig:cpu}
\end{figure*}
\fi
\if 0
\begin{figure*}[t]
\begin{center}
\begin{tabular}{ |c|c|c|c|c|c|c|c| }
\hline &
& \textbf{BEC-REP} & \textbf{BEC-TRAN}& \textbf{BEC-BAT}
& \textbf{VOTE} & \textbf{DOZ-REP}& \textbf{DOZ-TRAN} \\
\hline
\textbf{Instant Seal}& \textbf{S} & 1382 & 3037 & 2146
& 1027 & 751 & 900\\
\cline{2-8}
\textbf{(Empty)}& \textbf{S-N} & 1311 & 2995 & 1809
& 625 & 502& 750\\
\cline{2-8}
\textbf{}& \textbf{O} & 1398 & 3147 & 2261
& 1410 & 837 & 1114\\
\hline
\textbf{Batch Packing}& \textbf{S}& 1768 & 3050 & 1104 & 1705 & 901 & 1483 \\
\cline{2-8}
\textbf{(Empty)}& \textbf{S-N}& 1610 & 2992 & 1010 & 1093 & 899 & 1183 \\
\cline{2-8}
& \textbf{O}& 1786 & 3647 & 1189 & 2460 & 955 & 1869 \\
\hline
& \textbf{S}& 860 & 1489 & 631 & 1132 & 611 & 1077 \\
\cline{2-8}
\textbf{Batch Packing} & \textbf{S-N}& 832 & 1485 & 596 & 677 & 579 & 904 \\
\cline{2-8}
\textbf{(Main Net)}& \textbf{O}& 905 & 2181 & 715 & 1439 & 667 & 1184 \\
\cline{2-8}
& \textbf{B (1000 blocks)}& 46 & 27 & 3 & 24 & 190 & 173 \\
\hline
\end{tabular}
\end{center}
\caption{Number of transactions can be processed by parity client per second.}
\label{fig:tps}
\end{figure*}
\fi
% \begin{figure*}[t]
% \begin{center}
% \begin{tabular}{ |c|c|c|c|c|c|c|c|c|c|c|c| }
% \hline
% & \textbf{Tether} & \textbf{ZRX}& \textbf{Theta}
% & \textbf{INB} & \textbf{Hedg}& \textbf{DAI} & \textbf{EKT} & \textbf{XIN} & \textbf{HOT} & \textbf{Swipe} \\
% \hline
% \textbf{S} &
% 945 & 1729 & 1871 & 1562 & 1362 & 1359 & 1493 & 1865 & 1770 &1300\\
% \hline
% \textbf{S-N} &
% 982& 1740 &1852 &1558 &1338 &1341& 1536& 1853 & 1730& 1309\\
% \hline
% \textbf{O} &
% 1245& 2234& 2363& 2088 & 2118 & 2094& 2260 &2509 & 2505 & 1938\\
% \hline
% \hline
% & \textbf{MCHH} & \textbf{CryptantCrab}& \textbf{Clover}
% & \textbf{Land} & \textbf{Cards}& \textbf{KB} & \textbf{Trinket} & \textbf{Packs} & \textbf{BKC} & \textbf{EGG} \\
% \hline
% \textbf{S} &
% 1782& 1944 & 1742& 1892 & 1813 & 1801 & 1879 & 1767 & 1919 & 1845 \\
% \hline
% \textbf{S-N} &
% 1614 & 1561 & 1597 & 1561 & 1711 & 1693 & 1624 & 1525 & 1719 & 1616 \\
% \hline
% \textbf{O} &
% 2257 & 2326 & 2062 & 2346 & 2307 & 2361 & 2324 & 2119 & 2472 & 2261\\
% \hline
% \end{tabular}
% \end{center}
% \caption{Number of transactions can be processed by parity client per second for real world smart
% contracts.}
% \label{fig:real-data}
% \end{figure*}
\pgfplotstableread[row sep=\\,col sep=&]{
interval & carT & carD & carR \\
BEC & 1.24 & 68.3 & 68.1 \\
USDT & 1.86 & 78.9 & 75.9 \\
ZRX & 0.986 & 77.9 & 77.4 \\
THETA & 0.967 & 78.4 & 79.2 \\
INB & 1.24 & 74.6 & 74.8 \\
HEDG & 1.21 & 63.2 & 64.3 \\
DAI & 1.11 & 64.0 & 64.9 \\
EKT & 1.03 & 68.0 & 66.1 \\
XIN & 0.984 & 73.9 & 74.3 \\
HOT & 1.03 & 69.1 & 70.7 \\
SWP & 1.04 & 67.5 & 67.1 \\
}\erctwenty
\pgfplotstableread[row sep=\\,col sep=&]{
interval & carT & carD & carR \\
DOZ & 14.6 & 76.4 & 90.1 \\
MCHH & 8.37 & 71.5 & 79.0 \\
CC & 13.3 & 67.1 & 83.6 \\
CLV & 9.16 & 77.4 & 84.5 \\
LAND & 7.8 & 66.5 & 80.6 \\
CARDS & 7.56 & 74.2 & 78.6 \\
KB & 8.26 & 71.7 & 76.3 \\
TRINK & 8.21 & 69.9 & 80.9 \\
BKC & 7.93 & 69.5 & 77.6 \\
PACKS & 8.73 & 72.0 & 83.4 \\
EGG & 8.14 & 71.5 & 81.6 \\
VOTE & 1.67 & 47.0 & 78.7 \\
}\ercseven
\begin{figure*}[t]
\begin{tikzpicture}
\begin{axis}[
ybar,
bar width=.15cm,
width=\textwidth,
height=.18\textwidth,
x tick label style = {text width=1cm,align=center},
legend style={at={(0.5,1.2)},
anchor=north,legend columns=-1},
symbolic x coords={BEC,USDT,ZRX,THETA,INB,HEDG,DAI,EKT,XIN,HOT,SWP},
xticklabels={BEC 2181,USDT 1235,ZRX 2636,THETA 2791,INB 2098,HEDG 2153,DAI 2260,EKT 2629,XIN 2745,HOT 2728,SWP 1762},
xtick=data,
%nodes near coords,
%nodes near coords align={vertical},
ymin=0,ymax=100,
ylabel={\% of original tx},
]
\addplot table[x=interval,y=carT]{\erctwenty};
%\addplot table[x=interval,y=carD]{\erctwenty};
\addplot table[x=interval,y=carR]{\erctwenty};
\legend{Baseline, Solythesis}
\end{axis}
\end{tikzpicture}
\begin{tikzpicture}
\begin{axis}[
ybar,
bar width=.15cm,
width=\textwidth,
height=.18\textwidth,
x tick label style = {text width=1cm,align=center},
legend style={at={(0.5,1.2)},
anchor=north,legend columns=-1},
symbolic x coords={DOZ,MCHH,CC,CLV,LAND,CARDS,KB,TRINK,BKC,PACKS,EGG,VOTE},
xticklabels={DOZ 1184,MCHH 2257,CC 2326,CLV 2062,LAND 2346,CARDS 2307,KB 2361,TRINK 2324,BKC 2472,PACKS 2119,EGG 2261,VOTE 1439},
xtick=data,
%nodes near coords,
%nodes near coords align={vertical},
ymin=0,ymax=100,
ylabel={\% of original tx},
]
\addplot table[x=interval,y=carT]{\ercseven};
%\addplot table[x=interval,y=carD]{\ercseven};
\addplot table[x=interval,y=carR]{\ercseven};
\legend{Baseline, Solythesis}
\end{axis}
\end{tikzpicture}
\caption{Overhead Comparison with respect to original contract for top ERC20, ERC721 and ERC1202 contracts.}
\label{fig:baseline-ERC}
\end{figure*}
% \begin{figure*}[t]
% \begin{center}
% \begin{tabular}{ |c|c|c|c|c| }
% \hline
% & \textbf{SSD-12500} & \textbf{SSD-300}& \textbf{SSD-750} & \textbf{HDD}\\
% micros/op & \textbf{SSD-12500} & 68.098& 80.940\\
% MB/s& \textbf{SSD-12500} & 3.6 & 3.8\\
% \hline
% \end{tabular}
% \end{center}
% \caption{Number of transactions can be processed by parity client per second.}
% \label{fig:tps}
% \end{figure*}
\subsection{Results with Consensus}
%Figure~\ref{fig:cpu} and Figure~\ref{fig:tps} show the experiment result.
%There is a column in the table for each benchmark.
% For each experiment, we measure the performance of instrumented smart contracts
% (\textbf{S}), instrumented smart contracts without optimization (\textbf{S-N}),
% and the origin smart contract (\textbf{O}) respectively.
% The first column describes the name of benchmark
% and for the rest columns, each column represents a type of smart contract.
% \textbf{Secured} are smart contracts with instrumentation.
% \textbf{Secured(no opt)} are smart contract with instrumentation but
% without optimization. \textbf{Origin} represents the origin smart contracts.
%\subsubsection{Resources Consumption}\label{sec:results:cpu}
Figure~\ref{fig:cpu} shows the resources consumed by Parity for all benchmark
contracts. For each experiment, we measure the performance of the instrumented
smart contracts (\textbf{S}) and the original smart contract (\textbf{O})
respectively. Rows 2-3 present the average CPU usage of Parity. We observe that
the CPU usage of Parity is lower than 10\% for 95\% of time and the average CPU
usage of Parity is lower than 4\% for all benchmarks. Rows 4-5 present the average data written to the
disk per second by Parity.
Our results show that for all contracts, the transaction execution consumes only
a very small portion of the CPU and disk resources. The overhead introduced by
the {\systemname} instrumentation is negligible considering the current
capacity of CPU and disk storage devices and the cost of solving proof of work.
Note that the instrumented ERC1202 VOTE contract consumes sightly more (12 KB/s)
disk write bandwidth because the ERC1202 standard uses a map variable to track
the states for different issues and options, and this map variable is updated
multiple times in \sourcecode{vote} and \sourcecode{createIssue}. This result
validates our previous observation again that the transaction execution is not
the bottle neck of the Ethereum blockchain system. Thus, adding runtime
validation will not downgrade the performance of Ethereum, but improves the
security significantly.
%Besides, the average CPU usage of Parity client is not directly
%related to the complexity of executed smart contracts. This is because the
%block size is limited by gas and the total amount of instructions can be
%executed of each block is limited.
% Row 5-7 presents the total amount of data written to disk by Parity
% client.
% Futhermore, we observe that
% executing secured smart contract requires less CPU resources than
% executing secured smart contract without optimization, which reveals
% that our optimization is effective.
\if 0
\begin{figure*}[t]
\begin{center}
\begin{tabular}{ |c|c|c|c|c|c|c|c| }
\hline
& & \textbf{BEC-REP} & \textbf{BEC-TRAN}& \textbf{BEC-BAT}
& \textbf{VOTE} & \textbf{DOZ-REP}& \textbf{DOZ-TRAN} \\
\hline
& \textbf{S}& 7& 3& 7& 5& 17& 14\\
\cline{2-8}
\textbf{STORE}& \textbf{S-N}& 7& 3& 7& 15& 18& 15\\
\cline{2-8}
& \textbf{O}& 6& 2& 6& 3& 12& 8\\
\hline
& \textbf{S}& 9& 5& 9& 7& 10& 11\\
\cline{2-8}
\textbf{LOAD}& \textbf{S-N}& 9& 5& 9& 14& 12& 14\\
\cline{2-8}
& \textbf{O}& 7& 3& 7& 3& 6& 6\\
\hline
\end{tabular}
\end{center}
\caption{Number of instructions.}
\label{fig:instruction}
\end{figure*}
\fi
\subsection{Results without Consensus}
To understand the overhead of the {\systemname} instrumentation under fast
consensus protocols, we run experiments on Parity when we turn off the
consensus layer. We also compare the instrumentation overhead of {\systemname}
with the baseline instrumentation algorithm (which naively performs iterative
checks at the end of each transaction call) to evaluate the effectiveness of
our optimizations.
Figure~\ref{fig:baseline-ERC} presents our experimental results. X axis
corresponds to different smart contracts. The label in the X axis include both
the smart contract name and the TPS of the original contract. Y axis
corresponds to the transaction throughput in the number of transactions
processed by Parity per second (TPS). The Y axis is normalized to the TPS of
the original smart contracts. Red bars in Figure~\ref{fig:baseline-ERC}
correspond to the throughput results of {\systemname}, while blue bars
correspond to the results of the baseline algorithm.
Our results show that even in the extreme cases where the consensus is no
longer the performance bottleneck at all, the instrumentation overhead of
{\systemname} would still be acceptable. The average TPS slowdown caused by the
{\systemname} instrumentation in this set of experiments is 24\%. Our results
also highlight the importance of the delta update and delta check techniques in
{\systemname}. Without those optimizations, the naive instrumentation brings
two orders of magnitude of slowdown in the transaction throughput.
\subsection{Discussion and Future Directions}
\label{sec:results:discussion}
Our experimental results demonstrate that runtime validation is much more
affordable in smart contracts than it is in many other domains. Because of the
performance bottlenecks at the consensus layer and the storage layer,
lightweight runtime instrumentations can have small or even negligible
overhead. Our results reveal several future research directions on how to make
secure and efficient smart contracts and blockchain platforms.
\noindent \textbf{New Languages with Runtime Validation:} To secure smart
contracts, people are designing new smart contract languages that can eliminate
certain classes of errors at compile time, at the cost of limiting
language expressiveness~\cite{move, scilla, obsidian}. Our results imply that making the difficult
trade-off between correctness and expressiveness may not be necessary.
One possible future direction is to design new languages that can better
utilize rigorous runtime validation to enforce the correctness and security.
\noindent \textbf{Static Analysis and Verification:} Developing static analysis
and verification techniques to secure smart contracts is both an active
research topic and an industrial trend~\cite{securify, npchecker, solar, oyente, manticore, mythril,
ethracer, zeus, kevm, verisolid, evmstar, certik, quantstamp}. Like similar techniques in
traditional programs, static analysis techniques often have inaccurate results,
while verification techniques typically require human intervention. Because of
the inexpensive cost, runtime validation can act as backup techniques to cover
scenarios that static analysis techniques fail to fully analyze or that
verification techniques cannot fully prove.
\noindent \textbf{Runtime Validation in Blockchain VM:} {\systemname}
implements runtime validation via Solidity source code instrumentation. We can
further reduce the overhead if we implement some of the instrumented runtime
checks in the blockchain virtual machine, although this would require a hard
fork for existing blockchains like Ethereum.
\noindent \textbf{New Gas Mechanism:} Each EVM instruction charges gas and the
fee of an Ethereum smart contract transaction is determined by the total gas the
transaction consumes. In our experiments, the average gas overhead of the
instrumented contracts is 77.8\%, which is significantly higher than the actual
resource consumption overhead (which is negligible). One possible explanation
is that the gas schedule in Ethereum does not correctly reflect the execution
cost of each EVM instruction. The gas overhead would cause the users of the
instrumented contracts to pay additional transaction fees. In light of our
results, we believe Ethereum and future blockchain systems should adopt a more
flexible gas mechanism to facilitate runtime validation techniques.
%To understand how much improvement the optimization described in
%Section~\ref{sec:impl} has on the performance of the instrumented
%smart contract, we use the export and import functionalities of
%Parity which allows Parity to export and import blockchain data.
%We further record the transaction number can be processed by
%Parity of importing different types of blockchain data.
% we disable the proof of work of Parity so that
% it is able to generate blocks instantly without waiting for the
% result of proof of work.
% it
% generates blocks every time it receives a new transaction. Therefore,
% Parity is able to process transactions instantly without waiting
% for the proof of work result.
%\noindent\textbf{Instant Seal (Empty):} In this experiment, Parity imports
%transaction data where a block contains a single transaction.
%The second to the fourth rows show the number of transactions can
%be processed by Parity client for different smart contracts.
%The optimized smart contract has a better performance than the non-optimized
%one for all benchmarks. The performance of optimized smart contracts
%for VOTE and DOZ-REP improves 64\% and 50\% respectively because both
%\sourcecode{mintUniqueTokenTo} and \sourcecode{vote} functions involve
%multiple state variable operations which are cached by our optimization
%algorithm. Besides, the \sourcecode{mintUniqueTokenTo} function calls other
%internal functions of the smart contract. The global array created by {\systemname}
%avoid the secured smart contract to use state variables to maintain state variable
%bindings. The performance of optimized smart contracts for BEC-REP and BEC-TRAN only
%improves 1\% and 5\% the \sourcecode{transfer} in BECToken function is simple and even
%without optimization, the performance of instrumented smart contract is
%close to the performance of the origin contract. Our experiment shows that
%the optimization mentioned in Section~\ref{sec:impl} is effective for
%sophisticated functions and can improve the
%performance of instrumented smart contracts significantly.
%\noindent\textbf{Batch Packing (Empty):} In this experiment, we follow
%the same
%configurations as Section~\ref{sec:results:cpu}, where a transaction
%of smart contract is duplicated multiple times and sent to different
%smart contracts until the sum of gas of those transactions exceeds 8,000,000.
%Besides, the gas usage for each transaction is set to executing the transaction
%using the origin smart contract. We measure the number of transactions
%can be processes by Parity for different benchmarks when the blockchain is
%empty. Parity is able to process more than 1000 transactions per second
%for all benchmarks which is far more than the current ethereum
%main net which is only able to process 8 transactions per second.
%\noindent\textbf{Batch Packing (Main Net):} In this experiment, we follow
%the same configuration as Section~\ref{sec:results:cpu} and append new
%blocks to the blockchain with 5,052,259 existing blocks. The results show
%that the size of blockchain does influence performance of Parity.
% The fifth to the seventh rows show the number of transactions can be imported
% by Parity client of different smart contracts. Similar to
% \textbf{Transaction Processing \rom{1}}, Parity is able to process more transactions
% sent to the instrumented smart contracts then to the instrumented smart contracts
% without optimization. Note Parity is able to
%\subsubsection{Distinct Storage Access} Figure~\ref{fig:instruction}
%presents the average number of distinct storage read (\textbf{LOAD}) and
%distinct storage write (\textbf{STORE}) performed by Ethereum virtual
%machine to execute a transaction from benchmarks described in
%Section~\ref{sec:results:methodology}.
% All optimized functions except
% \sourcecode{mintUniqueTokenTo} require less gas and instructions than
% non-optimized functions, which shows the effectiveness of our optimization
% mentioned in Section~\ref{sec:impl}. The non-optimized
% \sourcecode{mintUniqueTokenTo} function require less gas than the optimized
% one because the \sourcecode{mintUniqueTokenTo} contains multiple
% inter-function calls. In order to create a global array mentioned in
% Section~\ref{sec:impl:global-memory}, {\systemname} inserts inline
% assemblies at the beginning of each function. The non-optimized smart
% contracts do not require such code and use state variables directly.
% % executed for the origin smart contract (\textbf{Origin}), instrumented
% % There is a row in the table for each smart contract function. The first and
% % the second columns show the contract name and function name respectively.
% % For the rest 9 columns, every three columns represent the origin smart contract,
% % instrumented smart contract, and instrumented smart contract respectively.
% % We further record the number of storage store
% % instructions (\textbf{ST}), storage load instructions (\textbf{LD}), and total
% % number of instructions (\textbf{SUM}).
\section{Related Work}\label{sec:related}
%We discuss related work in smart contract security and secure compilation.
\noindent\textbf{Smart Contract Security:} There is a rich body of work on
detecting vulnerable smart contracts with different techniques such as symbolic
execution~\cite{maian, solar, oyente, manticore, mythril, ethracer, zeus,verx,
npchecker}, fuzzing~\cite{fuzzing, contract-fuzzing}, domain specific static
analysis~\cite{securify}, and formal verification~\cite{kevm, verisolid,
evmstar, k-verification}. Oyente~\cite{oyente} detect transaction-order
dependency attacks, reentrance attacks, and mishandled exception attacks using
symbolic execution. Verx~\cite{verx} uses delayed abstraction to detect and
verify temporal safety properties automatically. \citeauthor{fuzzing} present a
new fuzzing technique that learns from symbolic execution traces to achieve
both high coverage and high speed~\cite{fuzzing}. Securify presents a domain
specific formal verification technique that translates Solidity smart contract
into Datalog and verifies security properties such as restricted storage writes
and ether transfers~\cite{securify}.
K-framework is a rewrite-based semantic framework that allows developers to
specify semantics of programming language formally~\cite{k-framework}.
KEVM~\cite{kevm} defines the semantic of EVM in $\mathbb{K}$ and verifies the
smart contract against user defined specifications. IELE~\cite{iele} presents a
smart contract virtual machine with a formal specification described in
$\mathbb{K}$ which achieves similar performance as EVM and provides
verifiability.
{\systemname} differs from these previous static analysis, fuzzing, and
symbolic execution approaches in that it inserts runtime checks to enforce user
specified invariants. Unlike these approaches, {\systemname} does not suffer
from false positives and false negatives. Comparing to most formal verification
approaches, {\systemname} is fully automated and does not require human
intervention. Securify is an automated verification tool using SMT solvers, but
it may not scale to complicated contracts due to the potential SMT expression
explosion problem. Also unlike {\systemname} it cannot support sophisticated
constraints like quantifiers.
%Theses tools formalize the
%semantics of either Solidity language or EVM instructions and
%summarize the behavior of smart contracts or compiled EVM bytecode.
%However due to the nature of static analysis, all of these tools
%suffer from false positives and benign errors.
%Moreover, the time required to analyze a smart contract increases
%exponentially as the complexity of smart contract increases, which
%discourages smart contract developers from using such tools.
%{\systemname} is free from false positives since it rejects
%transactions on the flow based on the current state of the smart
%contract.
%The time for smart contract instrumentation is linear with
%respect to the size of smart contract because {\systemname} simply applies
%a fixed set of rewrite rules to the smart contract.
%Once compiled, the
%constraints inside the standard is enforced and any transaction that
%violates the standard specification will be reverted.
\noindent\textbf{New Language Design:}
Many new programming languages have been proposed recently to improve the smart
contract security. Scilla~\cite{scilla} is a low level smart contract language
with a refined type system which is easy to be verified. Move~\cite{move}
introduces resources types and uses linear logic to enforced access control
policies for digital assets. Obsidian~\cite{obsidian} uses typestate and linear
type to enforce static checks. The trend of these new languages is to sacrifice
expressiveness (e.g., no longer turing-complete) to gain correctness or
security guarantees. Interestingly, our results reveal an alternative path. ---
one possible future direction is to design new languages that can better
utilize rigorous runtime validation to enforce the correctness and security.
%However, none of those languages introduce
%runtime validation. Logic errors such as allowing a user to vote multiple times
%could still be missed by those static checkers.
\noindent\textbf{Secure Compilation:} The security community has been focusing
on secure compilation for a long while. However, such tools are not immediately
applicable to smart contracts because the computation model between EVM and
traditional computer system is quite different. Many existing work focus on
memory safety~\cite{hextype, softboundcets}, side-channel
attacks~\cite{ctwasm}, and error isolation~\cite{isolation}. ContractLarva
presents a runtime verification technique that enforces the execution path of
Ethereum smart contracts to stop vulnerabilities that an attacker invokes a
contract constructor maliciously. Unlike ContractLarva, {\systemname} supports
user defined invariants and works for a much wider scope.
%To the best of our
%knowledge, {\systemname} is the first secure compilation tool that works on
%Solidity to enforce user defined invariants.
%, which are rarely considered in
%smart contract security. Besides, none of the above works consider embedding standard
%specification in programs and raising exceptions when the specification
%is violated.
\noindent\textbf{Runtime Checks:} Performing runtime checks is a useful
technique to improve the software security. \citeauthor{control-flow} propose a
framework that enforces the control-flow integrity to mitigate memory
attacks~\cite{control-flow}. \citeauthor{memsafe} enforce both spatial and
temporal memory safety of C programs without introducing high overhead by
modelling temporal errors as spatial errors and removing redundant
checks~\cite{memsafe}. Similarly, Frama-C generates runtime memory monitor
automatically to check E-ACSL specifications~\cite{frama-c}.
\citeauthor{anomaly-detection} describe that patterns in data that do not
conform to expected behavior can help the system to detect intrusions, frauds
and faults~\cite{anomaly-detection}. \citeauthor{diehard}, for example,
implements a runtime system which executes multiple replicas of the same
application simultaneously and detects memory errors dynamically
~\cite{diehard}. {\systemname} inserts runtime checks at the Solidity level.
Modifying the EVM implementation to perform runtime checks may further reduce
the overhead, but it would require a blockchain hard-fork.
%Adopting such tools to detect errors in
%smart contract is not applicable since most of those tools focus on memory
%safety and cannot detect standard violation errors at all.
\section{Conclusion}\label{sec:conclusion}
Runtime validation is an effective and efficient approach to secure smart
contracts. Our results show that because the transaction execution is not the
performance bottleneck in Ethereum, the overhead of runtime validation, which
is often too expensive for other domains, is in fact negligible for smart
contracts.
%%% -*-BibTeX-*-
%%% Do NOT edit. File created by BibTeX with style
%%% ACM-Reference-Format-Journals [18-Jan-2012].
\begin{thebibliography}{48}
%%% ====================================================================
%%% NOTE TO THE USER: you can override these defaults by providing
%%% customized versions of any of these macros before the \bibliography
%%% command. Each of them MUST provide its own final punctuation,
%%% except for \shownote{}, \showDOI{}, and \showURL{}. The latter two
%%% do not use final punctuation, in order to avoid confusing it with
%%% the Web address.
%%%
%%% To suppress output of a particular field, define its macro to expand
%%% to an empty string, or better, \unskip, like this:
%%%
%%% \newcommand{\showDOI}[1]{\unskip} % LaTeX syntax
%%%
%%% \def \showDOI #1{\unskip} % plain TeX syntax
%%%
%%% ====================================================================
\ifx \showCODEN \undefined \def \showCODEN #1{\unskip} \fi
\ifx \showDOI \undefined \def \showDOI #1{#1}\fi
\ifx \showISBNx \undefined \def \showISBNx #1{\unskip} \fi
\ifx \showISBNxiii \undefined \def \showISBNxiii #1{\unskip} \fi
\ifx \showISSN \undefined \def \showISSN #1{\unskip} \fi
\ifx \showLCCN \undefined \def \showLCCN #1{\unskip} \fi
\ifx \shownote \undefined \def \shownote #1{#1} \fi
\ifx \showarticletitle \undefined \def \showarticletitle #1{#1} \fi
\ifx \showURL \undefined \def \showURL {\relax} \fi
% The following commands are used for tagged output and should be
% invisible to TeX
\providecommand\bibfield[2]{#2}
\providecommand\bibinfo[2]{#2}
\providecommand\natexlab[1]{#1}
\providecommand\showeprint[2][]{arXiv:#2}
\bibitem[\protect\citeauthoryear{??}{ant}{[n. d.]}]%
{antlr}
\bibinfo{year}{[n. d.]}\natexlab{}.
\newblock \bibinfo{title}{ANTLR: ANother Tool for Language Recognition}.
\newblock \bibinfo{howpublished}{\url{https://www.antlr.org/}}.
\newblock
\bibitem[\protect\citeauthoryear{??}{bec}{[n. d.]}]%
{bec_contract}
\bibinfo{year}{[n. d.]}\natexlab{}.
\newblock \bibinfo{title}{Beauty Chain: The world's first blockchain platform
dedicated to the beauty ecosystem.}
\newblock \bibinfo{howpublished}{\url{http://www.beauty.io/}}.
\newblock
\bibitem[\protect\citeauthoryear{??}{cer}{[n. d.]}]%
{certik}
\bibinfo{year}{[n. d.]}\natexlab{}.
\newblock \bibinfo{title}{Certik: World's most advanced formal verification
technology for smart contracts}.
\newblock \bibinfo{howpublished}{\url{https://www.certik.org/}}.
\newblock
\bibitem[\protect\citeauthoryear{??}{doz}{[n. d.]}]%
{doz_contract}
\bibinfo{year}{[n. d.]}\natexlab{}.
\newblock \bibinfo{title}{CryptoDozer}.
\newblock \bibinfo{howpublished}{\url{https://cryptodozer.io/}}.
\newblock
\bibitem[\protect\citeauthoryear{??}{erc}{[n. d.]a}]%
{erc20}
\bibinfo{year}{[n. d.]}\natexlab{a}.
\newblock \bibinfo{title}{EIP 1202: Token Standard}.
\newblock \bibinfo{howpublished}{\url{https://eips.ethereum.org/EIPS/eip-20}}.
\newblock
\bibitem[\protect\citeauthoryear{??}{erc}{[n. d.]b}]%
{erc1202}
\bibinfo{year}{[n. d.]}\natexlab{b}.
\newblock \bibinfo{title}{EIP 1202: Voting Standard}.
\newblock
\bibinfo{howpublished}{\url{https://eips.ethereum.org/EIPS/eip-1202}}.
\newblock
\bibitem[\protect\citeauthoryear{??}{erc}{[n. d.]c}]%
{erc721}
\bibinfo{year}{[n. d.]}\natexlab{c}.
\newblock \bibinfo{title}{EIP 721: Non-Fungible Token Standard}.
\newblock \bibinfo{howpublished}{\url{https://eips.ethereum.org/EIPS/eip-721}}.
\newblock
\bibitem[\protect\citeauthoryear{??}{eth}{[n. d.]}]%
{etherscan}
\bibinfo{year}{[n. d.]}\natexlab{}.
\newblock \bibinfo{title}{Ethereum (ETH) Blockchain Explorer}.
\newblock \bibinfo{howpublished}{\url{https://etherscan.io/}}.
\newblock
\bibitem[\protect\citeauthoryear{??}{gas}{[n. d.]}]%
{gas_limit}
\bibinfo{year}{[n. d.]}\natexlab{}.
\newblock \bibinfo{title}{Ethereum Gas Limit History}.
\newblock \bibinfo{howpublished}{\url{https://etherscan.io/chart/gaslimit}}.
\newblock
\bibitem[\protect\citeauthoryear{??}{par}{[n. d.]}]%
{parity}
\bibinfo{year}{[n. d.]}\natexlab{}.
\newblock \bibinfo{title}{Parity: The fastest and most advanced Ethereum
client}.
\newblock \bibinfo{howpublished}{\url{https://www.parity.io/ethereum/}}.
\newblock
\bibitem[\protect\citeauthoryear{??}{qua}{[n. d.]}]%
{quantstamp}
\bibinfo{year}{[n. d.]}\natexlab{}.
\newblock \bibinfo{title}{Quantstamp: Leaders in blockchain security and
solutions}.
\newblock \bibinfo{howpublished}{\url{https://quantstamp.com/}}.
\newblock
\bibitem[\protect\citeauthoryear{??}{sol}{[n. d.]}]%
{solidity-parser}
\bibinfo{year}{[n. d.]}\natexlab{}.
\newblock \bibinfo{title}{solidity-parser-antlr}.
\newblock
\bibinfo{howpublished}{\url{https://github.com/federicobond/solidity-parser-antlr}}.
\newblock
\bibitem[\protect\citeauthoryear{??}{sur}{[n. d.]}]%
{surya}
\bibinfo{year}{[n. d.]}\natexlab{}.
\newblock \bibinfo{title}{Surya, The Sun God: A Solidity Inspector}.
\newblock \bibinfo{howpublished}{\url{https://github.com/ConsenSys/surya}}.
\newblock
\bibitem[\protect\citeauthoryear{Abadi, Budiu, Erlingsson, and Ligatti}{Abadi
et~al\mbox{.}}{2005}]%
{control-flow}
\bibfield{author}{\bibinfo{person}{Martin Abadi}, \bibinfo{person}{Mihai
Budiu}, \bibinfo{person}{Ulfar Erlingsson}, {and} \bibinfo{person}{Jay
Ligatti}.} \bibinfo{year}{2005}\natexlab{}.
\newblock \showarticletitle{Control-flow Integrity}. In
\bibinfo{booktitle}{\emph{Proceedings of the 12th ACM Conference on Computer
and Communications Security}} \emph{(\bibinfo{series}{CCS '05})}.
\bibinfo{publisher}{ACM}, \bibinfo{address}{New York, NY, USA},
\bibinfo{pages}{340--353}.
\newblock
\showISBNx{1-59593-226-7}
\urldef\tempurl%
\url{https://doi.org/10.1145/1102120.1102165}
\showDOI{\tempurl}
\bibitem[\protect\citeauthoryear{Berger and Zorn}{Berger and Zorn}{2006}]%
{diehard}
\bibfield{author}{\bibinfo{person}{Emery~D. Berger} {and}
\bibinfo{person}{Benjamin~G. Zorn}.} \bibinfo{year}{2006}\natexlab{}.
\newblock \showarticletitle{DieHard: Probabilistic Memory Safety for Unsafe
Languages}. In \bibinfo{booktitle}{\emph{Proceedings of the 27th ACM SIGPLAN
Conference on Programming Language Design and Implementation}}
\emph{(\bibinfo{series}{PLDI '06})}. \bibinfo{publisher}{ACM},
\bibinfo{address}{New York, NY, USA}, \bibinfo{pages}{158--168}.
\newblock
\showISBNx{1-59593-320-4}
\urldef\tempurl%
\url{https://doi.org/10.1145/1133981.1134000}
\showDOI{\tempurl}
\bibitem[\protect\citeauthoryear{Bhargavan, Delignat-Lavaud, Fournet,
Gollamudi, Gonthier, Kobeissi, Kulatova, Rastogi, Sibut-Pinote, Swamy, and
Zanella-B{\'e}guelin}{Bhargavan et~al\mbox{.}}{2016}]%
{evmstar}
\bibfield{author}{\bibinfo{person}{Karthikeyan Bhargavan},
\bibinfo{person}{Antoine Delignat-Lavaud}, \bibinfo{person}{Cedric Fournet},
\bibinfo{person}{Anitha Gollamudi}, \bibinfo{person}{Georges Gonthier},
\bibinfo{person}{Nadim Kobeissi}, \bibinfo{person}{Natalia Kulatova},
\bibinfo{person}{Aseem Rastogi}, \bibinfo{person}{Thomas Sibut-Pinote},
\bibinfo{person}{Nikhil Swamy}, {and} \bibinfo{person}{Santiago
Zanella-B{\'e}guelin}.} \bibinfo{year}{2016}\natexlab{}.
\newblock \showarticletitle{Formal Verification of Smart Contracts: Short
Paper}. In \bibinfo{booktitle}{\emph{Proceedings of the 2016 ACM Workshop on
Programming Languages and Analysis for Security}}
\emph{(\bibinfo{series}{PLAS '16})}. \bibinfo{publisher}{ACM},
\bibinfo{address}{New York, NY, USA}, \bibinfo{pages}{91--96}.
\newblock
\showISBNx{978-1-4503-4574-3}
\urldef\tempurl%
\url{https://doi.org/10.1145/2993600.2993611}
\showDOI{\tempurl}
\bibitem[\protect\citeauthoryear{Biggs}{Biggs}{2018}]%
{bec}
\bibfield{author}{\bibinfo{person}{John Biggs}.}
\bibinfo{year}{2018}\natexlab{}.
\newblock \bibinfo{title}{Overflow error shuts down token trading}.
\newblock
\bibinfo{howpublished}{\url{https://techcrunch.com/2018/04/25/overflow-error-shuts-down-token-trading/}}.
\newblock
\bibitem[\protect\citeauthoryear{Blackshear, Dill, Gao, Maurer, Nowacki, Pott,
Qadeer, Rain, Russi, Sezer, Zakian, and Zhou}{Blackshear
et~al\mbox{.}}{2019}]%
{move}
\bibfield{author}{\bibinfo{person}{Sam Blackshear}, \bibinfo{person}{Evan
Chengand David~L. Dill}, \bibinfo{person}{Victor Gao}, \bibinfo{person}{Ben
Maurer}, \bibinfo{person}{Todd Nowacki}, \bibinfo{person}{Alistair Pott},
\bibinfo{person}{Shaz Qadeer}, \bibinfo{person}{Rain}, \bibinfo{person}{Dario
Russi}, \bibinfo{person}{Stephane Sezer}, \bibinfo{person}{Tim Zakian}, {and}
\bibinfo{person}{Runtian Zhou}.} \bibinfo{year}{2019}\natexlab{}.
\newblock \bibinfo{booktitle}{\emph{Move: A Language With Programmable
Resources}}.
\newblock \bibinfo{type}{{T}echnical {R}eport}.
\newblock
\urldef\tempurl%
\url{https://developers.libra.org/docs/assets/papers/libra-move-a-language-with-programmable-resources.pdf}
\showURL{%
\tempurl}
\bibitem[\protect\citeauthoryear{Chandola, Banerjee, and Kumar}{Chandola
et~al\mbox{.}}{2009}]%
{anomaly-detection}
\bibfield{author}{\bibinfo{person}{Varun Chandola}, \bibinfo{person}{Arindam
Banerjee}, {and} \bibinfo{person}{Vipin Kumar}.}
\bibinfo{year}{2009}\natexlab{}.
\newblock \showarticletitle{Anomaly Detection: A Survey}.
\newblock \bibinfo{journal}{\emph{ACM Comput. Surv.}} \bibinfo{volume}{41},
\bibinfo{number}{3}, Article \bibinfo{articleno}{15},
\bibinfo{numpages}{58}~pages.
\newblock
\showISSN{0360-0300}
\urldef\tempurl%
\url{https://doi.org/10.1145/1541880.1541882}
\showDOI{\tempurl}
\bibitem[\protect\citeauthoryear{Chen, Park, and Ro{\c{s}}u}{Chen
et~al\mbox{.}}{2018}]%
{k-verification}
\bibfield{author}{\bibinfo{person}{Xiaohong Chen}, \bibinfo{person}{Daejun
Park}, {and} \bibinfo{person}{Grigore Ro{\c{s}}u}.}
\bibinfo{year}{2018}\natexlab{}.
\newblock \showarticletitle{A Language-Independent Approach to Smart Contract
Verification}. In \bibinfo{booktitle}{\emph{Leveraging Applications of Formal
Methods, Verification and Validation. Industrial Practice}},
\bibfield{editor}{\bibinfo{person}{Tiziana Margaria} {and}
\bibinfo{person}{Bernhard Steffen}} (Eds.). \bibinfo{publisher}{Springer
International Publishing}, \bibinfo{address}{Cham},
\bibinfo{pages}{405--413}.
\newblock
\showISBNx{978-3-030-03427-6}
\bibitem[\protect\citeauthoryear{Coblenz, Oei, Etzel, Koronkevich, Baker,
Bloem, Myers, Sunshine, and Aldrich}{Coblenz et~al\mbox{.}}{2019}]%
{obsidian}
\bibfield{author}{\bibinfo{person}{Michael~J. Coblenz}, \bibinfo{person}{Reed
Oei}, \bibinfo{person}{Tyler Etzel}, \bibinfo{person}{Paulette Koronkevich},
\bibinfo{person}{Miles Baker}, \bibinfo{person}{Yannick Bloem},
\bibinfo{person}{Brad~A. Myers}, \bibinfo{person}{Joshua Sunshine}, {and}
\bibinfo{person}{Jonathan Aldrich}.} \bibinfo{year}{2019}\natexlab{}.
\newblock \showarticletitle{Obsidian: Typestate and Assets for Safer Blockchain
Programming}.
\newblock \bibinfo{journal}{\emph{ArXiv}} \bibinfo{volume}{abs/1909.03523}
(\bibinfo{year}{2019}).
\newblock
\bibitem[\protect\citeauthoryear{Daian}{Daian}{2016}]%
{dao}
\bibfield{author}{\bibinfo{person}{Phil Daian}.}
\bibinfo{year}{2016}\natexlab{}.
\newblock \bibinfo{title}{Analysis of the DAO exploit}.
\newblock
\bibinfo{howpublished}{\url{http://hackingdistributed.com/2016/06/18/analysis-of-the-dao-exploit/}}.
\newblock
\bibitem[\protect\citeauthoryear{He, Balunovi\'{c}, Ambroladze, Tsankov, and
Vechev}{He et~al\mbox{.}}{2019}]%
{fuzzing}
\bibfield{author}{\bibinfo{person}{Jingxuan He}, \bibinfo{person}{Mislav
Balunovi\'{c}}, \bibinfo{person}{Nodar Ambroladze}, \bibinfo{person}{Petar
Tsankov}, {and} \bibinfo{person}{Martin Vechev}.}
\bibinfo{year}{2019}\natexlab{}.
\newblock \showarticletitle{Learning to Fuzz from Symbolic Execution with
Application to Smart Contracts}. In \bibinfo{booktitle}{\emph{Proceedings of
the 2019 ACM SIGSAC Conference on Computer and Communications Security}}
\emph{(\bibinfo{series}{CCS '19})}. \bibinfo{publisher}{ACM},
\bibinfo{address}{New York, NY, USA}, \bibinfo{pages}{531--548}.
\newblock
\showISBNx{978-1-4503-6747-9}
\urldef\tempurl%
\url{https://doi.org/10.1145/3319535.3363230}
\showDOI{\tempurl}
\bibitem[\protect\citeauthoryear{Hildenbrandt, Saxena, Rodrigues, Zhu, Daian,
Guth, Moore, Park, Zhang, Stefanescu, and Rosu}{Hildenbrandt
et~al\mbox{.}}{2018}]%
{kevm}
\bibfield{author}{\bibinfo{person}{E. Hildenbrandt}, \bibinfo{person}{M.
Saxena}, \bibinfo{person}{N. Rodrigues}, \bibinfo{person}{X. Zhu},
\bibinfo{person}{P. Daian}, \bibinfo{person}{D. Guth}, \bibinfo{person}{B.
Moore}, \bibinfo{person}{D. Park}, \bibinfo{person}{Y. Zhang},
\bibinfo{person}{A. Stefanescu}, {and} \bibinfo{person}{G. Rosu}.}
\bibinfo{year}{2018}\natexlab{}.
\newblock \showarticletitle{KEVM: A Complete Formal Semantics of the Ethereum
Virtual Machine}. In \bibinfo{booktitle}{\emph{2018 IEEE 31st Computer
Security Foundations Symposium (CSF)}}. \bibinfo{pages}{204--217}.
\newblock
\showISSN{2374-8303}
\urldef\tempurl%
\url{https://doi.org/10.1109/CSF.2018.00022}
\showDOI{\tempurl}
\bibitem[\protect\citeauthoryear{Jeon, Biswas, Carr, Lee, and Payer}{Jeon
et~al\mbox{.}}{2017}]%
{hextype}
\bibfield{author}{\bibinfo{person}{Yuseok Jeon}, \bibinfo{person}{Priyam
Biswas}, \bibinfo{person}{Scott Carr}, \bibinfo{person}{Byoungyoung Lee},
{and} \bibinfo{person}{Mathias Payer}.} \bibinfo{year}{2017}\natexlab{}.
\newblock \showarticletitle{HexType: Efficient Detection of Type Confusion
Errors for C++}. In \bibinfo{booktitle}{\emph{Proceedings of the 2017 ACM
SIGSAC Conference on Computer and Communications Security}}
\emph{(\bibinfo{series}{CCS '17})}. \bibinfo{publisher}{ACM},
\bibinfo{address}{New York, NY, USA}, \bibinfo{pages}{2373--2387}.
\newblock
\showISBNx{978-1-4503-4946-8}
\urldef\tempurl%
\url{https://doi.org/10.1145/3133956.3134062}
\showDOI{\tempurl}
\bibitem[\protect\citeauthoryear{Jiang, Liu, and Chan}{Jiang
et~al\mbox{.}}{2018}]%
{contract-fuzzing}
\bibfield{author}{\bibinfo{person}{Bo Jiang}, \bibinfo{person}{Ye Liu}, {and}
\bibinfo{person}{W.~K. Chan}.} \bibinfo{year}{2018}\natexlab{}.
\newblock \showarticletitle{ContractFuzzer: Fuzzing Smart Contracts for
Vulnerability Detection}. In \bibinfo{booktitle}{\emph{Proceedings of the
33rd ACM/IEEE International Conference on Automated Software Engineering}}
\emph{(\bibinfo{series}{ASE 2018})}. \bibinfo{publisher}{ACM},
\bibinfo{address}{New York, NY, USA}, \bibinfo{pages}{259--269}.
\newblock
\showISBNx{978-1-4503-5937-5}
\urldef\tempurl%
\url{https://doi.org/10.1145/3238147.3238177}
\showDOI{\tempurl}
\bibitem[\protect\citeauthoryear{Kalra, Goel, Dhawan, and Sharma}{Kalra
et~al\mbox{.}}{2018}]%
{zeus}
\bibfield{author}{\bibinfo{person}{Sukrit Kalra}, \bibinfo{person}{Seep Goel},
\bibinfo{person}{Mohan Dhawan}, {and} \bibinfo{person}{Subodh Sharma}.}
\bibinfo{year}{2018}\natexlab{}.
\newblock \showarticletitle{Zeus: Analyzing safety of smart contracts}. NDSS.
\newblock
\bibitem[\protect\citeauthoryear{Kasampalis, Guth, Moore,
Șerb{\u{a}}nuț{\u{a}}, Zhang, Filaretti, Șerb{\u{a}}nuț{\u{a}}, Johnson,
and Ro{\c{s}}u}{Kasampalis et~al\mbox{.}}{2019}]%
{iele}
\bibfield{author}{\bibinfo{person}{Theodoros Kasampalis},
\bibinfo{person}{Dwight Guth}, \bibinfo{person}{Brandon Moore},
\bibinfo{person}{Traian~Florin Șerb{\u{a}}nuț{\u{a}}}, \bibinfo{person}{Yi
Zhang}, \bibinfo{person}{Daniele Filaretti}, \bibinfo{person}{Virgil
Șerb{\u{a}}nuț{\u{a}}}, \bibinfo{person}{Ralph Johnson}, {and}
\bibinfo{person}{Grigore Ro{\c{s}}u}.} \bibinfo{year}{2019}\natexlab{}.
\newblock \showarticletitle{IELE: A Rigorously Designed Language and Tool
Ecosystem for the Blockchain}. In \bibinfo{booktitle}{\emph{Formal Methods --
The Next 30 Years}}, \bibfield{editor}{\bibinfo{person}{Maurice~H. ter Beek},
\bibinfo{person}{Annabelle McIver}, {and} \bibinfo{person}{Jos{\'e}~N.
Oliveira}} (Eds.). \bibinfo{publisher}{Springer International Publishing},
\bibinfo{address}{Cham}, \bibinfo{pages}{593--610}.
\newblock
\showISBNx{978-3-030-30942-8}
\bibitem[\protect\citeauthoryear{Kolluri, Nikolic, Sergey, Hobor, and
Saxena}{Kolluri et~al\mbox{.}}{2018}]%
{ethracer}
\bibfield{author}{\bibinfo{person}{Aashish Kolluri}, \bibinfo{person}{Ivica
Nikolic}, \bibinfo{person}{Ilya Sergey}, \bibinfo{person}{Aquinas Hobor},
{and} \bibinfo{person}{Prateek Saxena}.} \bibinfo{year}{2018}\natexlab{}.
\newblock \showarticletitle{Exploiting The Laws of Order in Smart Contracts}.
\newblock \bibinfo{journal}{\emph{CoRR}} \bibinfo{volume}{abs/1810.11605}
(\bibinfo{year}{2018}).
\newblock
\showeprint[arxiv]{1810.11605}
\urldef\tempurl%
\url{http://arxiv.org/abs/1810.11605}
\showURL{%
\tempurl}
\bibitem[\protect\citeauthoryear{Kosmatov, Petiot, and Signoles}{Kosmatov
et~al\mbox{.}}{2013}]%
{frama-c}
\bibfield{author}{\bibinfo{person}{Nikolai Kosmatov},
\bibinfo{person}{Guillaume Petiot}, {and} \bibinfo{person}{Julien Signoles}.}
\bibinfo{year}{2013}\natexlab{}.
\newblock \showarticletitle{An Optimized Memory Monitoring for Runtime
Assertion Checking of C Programs}. In \bibinfo{booktitle}{\emph{Runtime
Verification}}, \bibfield{editor}{\bibinfo{person}{Axel Legay} {and}
\bibinfo{person}{Saddek Bensalem}} (Eds.). \bibinfo{publisher}{Springer
Berlin Heidelberg}, \bibinfo{address}{Berlin, Heidelberg},
\bibinfo{pages}{167--182}.
\newblock
\showISBNx{978-3-642-40787-1}
\bibitem[\protect\citeauthoryear{Li and Long}{Li and Long}{2018}]%
{solar}
\bibfield{author}{\bibinfo{person}{Ao Li} {and} \bibinfo{person}{Fan Long}.}
\bibinfo{year}{2018}\natexlab{}.
\newblock \showarticletitle{Detecting Standard Violation Errors in Smart
Contracts}.
\newblock \bibinfo{journal}{\emph{CoRR}} \bibinfo{volume}{abs/1812.07702}
(\bibinfo{year}{2018}).
\newblock
\showeprint[arxiv]{1812.07702}
\urldef\tempurl%
\url{http://arxiv.org/abs/1812.07702}
\showURL{%
\tempurl}
\bibitem[\protect\citeauthoryear{Luu, Chu, Olickel, Saxena, and Hobor}{Luu
et~al\mbox{.}}{2016}]%
{oyente}
\bibfield{author}{\bibinfo{person}{Loi Luu}, \bibinfo{person}{Duc-Hiep Chu},
\bibinfo{person}{Hrishi Olickel}, \bibinfo{person}{Prateek Saxena}, {and}
\bibinfo{person}{Aquinas Hobor}.} \bibinfo{year}{2016}\natexlab{}.
\newblock \showarticletitle{Making Smart Contracts Smarter}. In
\bibinfo{booktitle}{\emph{Proceedings of the 2016 ACM SIGSAC Conference on
Computer and Communications Security}} \emph{(\bibinfo{series}{CCS '16})}.
\bibinfo{publisher}{ACM}, \bibinfo{address}{New York, NY, USA},
\bibinfo{pages}{254--269}.
\newblock
\showISBNx{978-1-4503-4139-4}
\urldef\tempurl%
\url{https://doi.org/10.1145/2976749.2978309}
\showDOI{\tempurl}
\bibitem[\protect\citeauthoryear{Mavridou, Laszka, Stachtiari, and
Dubey}{Mavridou et~al\mbox{.}}{2019}]%
{verisolid}
\bibfield{author}{\bibinfo{person}{Anastasia Mavridou}, \bibinfo{person}{Aron
Laszka}, \bibinfo{person}{Emmanouela Stachtiari}, {and}
\bibinfo{person}{Abhishek Dubey}.} \bibinfo{year}{2019}\natexlab{}.
\newblock \showarticletitle{VeriSolid: Correct-by-Design Smart Contracts for
Ethereum}.
\newblock \bibinfo{journal}{\emph{CoRR}} \bibinfo{volume}{abs/1901.01292}
(\bibinfo{year}{2019}).
\newblock
\showeprint[arxiv]{1901.01292}
\urldef\tempurl%
\url{http://arxiv.org/abs/1901.01292}
\showURL{%
\tempurl}
\bibitem[\protect\citeauthoryear{Mueller}{Mueller}{[n. d.]}]%
{mythril}
\bibfield{author}{\bibinfo{person}{Bernhard Mueller}.} \bibinfo{year}{[n.
d.]}\natexlab{}.
\newblock \bibinfo{title}{Mythril Classic: Security analysis tool for Ethereum
smart contracts}.
\newblock
\bibinfo{howpublished}{\url{https://github.com/ConsenSys/mythril-classic}}.
\newblock
\bibitem[\protect\citeauthoryear{Nagarakatte, Martin, and
Zdancewic}{Nagarakatte et~al\mbox{.}}{2015}]%
{softboundcets}
\bibfield{author}{\bibinfo{person}{Santosh Nagarakatte}, \bibinfo{person}{Milo
M.~K. Martin}, {and} \bibinfo{person}{Steve Zdancewic}.}
\bibinfo{year}{2015}\natexlab{}.
\newblock \showarticletitle{{Everything You Want to Know About Pointer-Based
Checking}}. In \bibinfo{booktitle}{\emph{1st Summit on Advances in
Programming Languages (SNAPL 2015)}} \emph{(\bibinfo{series}{Leibniz
International Proceedings in Informatics (LIPIcs)})},
\bibfield{editor}{\bibinfo{person}{Thomas Ball}, \bibinfo{person}{Rastislav
Bodik}, \bibinfo{person}{Shriram Krishnamurthi}, \bibinfo{person}{Benjamin~S.
Lerner}, {and} \bibinfo{person}{Greg Morrisett}} (Eds.),
Vol.~\bibinfo{volume}{32}. \bibinfo{publisher}{Schloss
Dagstuhl--Leibniz-Zentrum fuer Informatik}, \bibinfo{address}{Dagstuhl,
Germany}, \bibinfo{pages}{190--208}.
\newblock
\showISBNx{978-3-939897-80-4}
\showISSN{1868-8969}
\urldef\tempurl%
\url{https://doi.org/10.4230/LIPIcs.SNAPL.2015.190}
\showDOI{\tempurl}
\bibitem[\protect\citeauthoryear{Nakamoto}{Nakamoto}{[n. d.]}]%
{Bitcoin}
\bibfield{author}{\bibinfo{person}{Satoshi Nakamoto}.} \bibinfo{year}{[n.
d.]}\natexlab{}.
\newblock \bibinfo{title}{Bitcoin: A peer-to-peer electronic cash system,”
http://bitcoin.org/bitcoin.pdf}.
\newblock
\newblock
\bibitem[\protect\citeauthoryear{Nikolic, Kolluri, Sergey, Saxena, and
Hobor}{Nikolic et~al\mbox{.}}{2018}]%
{maian}
\bibfield{author}{\bibinfo{person}{Ivica Nikolic}, \bibinfo{person}{Aashish
Kolluri}, \bibinfo{person}{Ilya Sergey}, \bibinfo{person}{Prateek Saxena},
{and} \bibinfo{person}{Aquinas Hobor}.} \bibinfo{year}{2018}\natexlab{}.
\newblock \showarticletitle{Finding The Greedy, Prodigal, and Suicidal
Contracts at Scale}.
\newblock \bibinfo{journal}{\emph{CoRR}} \bibinfo{volume}{abs/1802.06038}
(\bibinfo{year}{2018}).
\newblock
\showeprint[arxiv]{1802.06038}
\urldef\tempurl%
\url{http://arxiv.org/abs/1802.06038}
\showURL{%
\tempurl}
\bibitem[\protect\citeauthoryear{of~Bits}{of~Bits}{[n. d.]}]%
{manticore}
\bibfield{author}{\bibinfo{person}{Trail of Bits}.} \bibinfo{year}{[n.
d.]}\natexlab{}.
\newblock \bibinfo{title}{Manticore: Symbolic Execution for Humans}.
\newblock
\bibinfo{howpublished}{\url{https://github.com/trailofbits/manticore}}.
\newblock
\bibitem[\protect\citeauthoryear{Permenev, Dimitrov, Tsankov, Drachsler-Cohen,
and Vechev}{Permenev et~al\mbox{.}}{[n. d.]}]%
{verx}
\bibfield{author}{\bibinfo{person}{Anton Permenev}, \bibinfo{person}{Dimitar
Dimitrov}, \bibinfo{person}{Petar Tsankov}, \bibinfo{person}{Dana
Drachsler-Cohen}, {and} \bibinfo{person}{Martin Vechev}.} \bibinfo{year}{[n.
d.]}\natexlab{}.
\newblock \showarticletitle{VerX: Safety Verification of Smart Contracts}.
\newblock (\bibinfo{year}{[n. d.]}).
\newblock
\bibitem[\protect\citeauthoryear{Rosu}{Rosu}{2017}]%
{k-framework}
\bibfield{author}{\bibinfo{person}{G. Rosu}.} \bibinfo{year}{2017}\natexlab{}.
\newblock \bibinfo{booktitle}{\emph{K: A semantic framework for programming
languages and formal analysis tools}}.
\newblock \bibinfo{pages}{186--206}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.3233/978-1-61499-810-5-186}
\showDOI{\tempurl}
\bibitem[\protect\citeauthoryear{Sergey, Nagaraj, Johannsen, Kumar, Trunov, and
Hao}{Sergey et~al\mbox{.}}{2019}]%
{scilla}
\bibfield{author}{\bibinfo{person}{Ilya Sergey}, \bibinfo{person}{Vaivaswatha
Nagaraj}, \bibinfo{person}{Jacob Johannsen}, \bibinfo{person}{Amrit Kumar},
\bibinfo{person}{Anton Trunov}, {and} \bibinfo{person}{Ken Chan~Guan Hao}.}
\bibinfo{year}{2019}\natexlab{}.
\newblock \showarticletitle{Safer Smart Contract Programming with Scilla}.
\newblock \bibinfo{journal}{\emph{Proc. ACM Program. Lang.}}
\bibinfo{volume}{3}, \bibinfo{number}{OOPSLA}, Article
\bibinfo{articleno}{185} (\bibinfo{date}{Oct.} \bibinfo{year}{2019}),
\bibinfo{numpages}{30}~pages.
\newblock
\showISSN{2475-1421}
\urldef\tempurl%
\url{https://doi.org/10.1145/3360611}
\showDOI{\tempurl}
\bibitem[\protect\citeauthoryear{{Simpson} and {Barua}}{{Simpson} and
{Barua}}{2010}]%
{memsafe}
\bibfield{author}{\bibinfo{person}{M.~S. {Simpson}} {and}
\bibinfo{person}{R.~K. {Barua}}.} \bibinfo{year}{2010}\natexlab{}.
\newblock \showarticletitle{MemSafe: Ensuring the Spatial and Temporal Memory
Safety of C at Runtime}. In \bibinfo{booktitle}{\emph{2010 10th IEEE Working
Conference on Source Code Analysis and Manipulation}}.
\bibinfo{pages}{199--208}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1109/SCAM.2010.15}
\showDOI{\tempurl}
\bibitem[\protect\citeauthoryear{Sompolinsky and Zohar}{Sompolinsky and
Zohar}{2015}]%
{GHOST}
\bibfield{author}{\bibinfo{person}{Yonatan Sompolinsky} {and}
\bibinfo{person}{Aviv Zohar}.} \bibinfo{year}{2015}\natexlab{}.
\newblock \showarticletitle{Secure High-Rate Transaction Processing in
Bitcoin}. In \bibinfo{booktitle}{\emph{Financial Cryptography and Data
Security}}, \bibfield{editor}{\bibinfo{person}{Rainer B{\"o}hme} {and}
\bibinfo{person}{Tatsuaki Okamoto}} (Eds.). \bibinfo{publisher}{Springer
Berlin Heidelberg}, \bibinfo{address}{Berlin, Heidelberg},
\bibinfo{pages}{507--527}.
\newblock
\showISBNx{978-3-662-47854-7}
\bibitem[\protect\citeauthoryear{Tsankov, Dan, Drachsler-Cohen, Gervais,
Bunzli, and Vechev}{Tsankov et~al\mbox{.}}{2018}]%
{securify}
\bibfield{author}{\bibinfo{person}{Petar Tsankov}, \bibinfo{person}{Andrei
Dan}, \bibinfo{person}{Dana Drachsler-Cohen}, \bibinfo{person}{Arthur
Gervais}, \bibinfo{person}{Florian Bunzli}, {and} \bibinfo{person}{Martin
Vechev}.} \bibinfo{year}{2018}\natexlab{}.
\newblock \showarticletitle{Securify: Practical Security Analysis of Smart
Contracts}. In \bibinfo{booktitle}{\emph{Proceedings of the 2018 ACM SIGSAC
Conference on Computer and Communications Security}}
\emph{(\bibinfo{series}{CCS '18})}. \bibinfo{publisher}{ACM},
\bibinfo{address}{New York, NY, USA}, \bibinfo{pages}{67--82}.
\newblock
\showISBNx{978-1-4503-5693-0}
\urldef\tempurl%
\url{https://doi.org/10.1145/3243734.3243780}
\showDOI{\tempurl}
\bibitem[\protect\citeauthoryear{Wahbe, Lucco, Anderson, and Graham}{Wahbe
et~al\mbox{.}}{1993}]%
{isolation}
\bibfield{author}{\bibinfo{person}{Robert Wahbe}, \bibinfo{person}{Steven
Lucco}, \bibinfo{person}{Thomas~E. Anderson}, {and} \bibinfo{person}{Susan~L.
Graham}.} \bibinfo{year}{1993}\natexlab{}.
\newblock \showarticletitle{Efficient Software-based Fault Isolation}.
\newblock \bibinfo{journal}{\emph{SIGOPS Oper. Syst. Rev.}}
\bibinfo{volume}{27}, \bibinfo{number}{5} (\bibinfo{date}{Dec.}
\bibinfo{year}{1993}), \bibinfo{pages}{203--216}.
\newblock
\showISSN{0163-5980}
\urldef\tempurl%
\url{https://doi.org/10.1145/173668.168635}
\showDOI{\tempurl}
\bibitem[\protect\citeauthoryear{Wang, Zhang, and Su}{Wang
et~al\mbox{.}}{2019}]%
{npchecker}
\bibfield{author}{\bibinfo{person}{Shuai Wang}, \bibinfo{person}{Chengyu
Zhang}, {and} \bibinfo{person}{Zhendong Su}.}
\bibinfo{year}{2019}\natexlab{}.
\newblock \showarticletitle{Detecting Nondeterministic Payment Bugs in Ethereum
Smart Contracts}.
\newblock \bibinfo{journal}{\emph{Proc. ACM Program. Lang.}}
\bibinfo{volume}{3}, \bibinfo{number}{OOPSLA}, Article
\bibinfo{articleno}{189} (\bibinfo{date}{Oct.} \bibinfo{year}{2019}),
\bibinfo{numpages}{29}~pages.
\newblock
\showISSN{2475-1421}
\urldef\tempurl%
\url{https://doi.org/10.1145/3360615}
\showDOI{\tempurl}
\bibitem[\protect\citeauthoryear{Watt, Renner, Popescu, Cauligi, and
Stefan}{Watt et~al\mbox{.}}{2019}]%
{ctwasm}
\bibfield{author}{\bibinfo{person}{Conrad Watt}, \bibinfo{person}{John Renner},
\bibinfo{person}{Natalie Popescu}, \bibinfo{person}{Sunjay Cauligi}, {and}
\bibinfo{person}{Deian Stefan}.} \bibinfo{year}{2019}\natexlab{}.
\newblock \showarticletitle{CT-wasm: Type-driven Secure Cryptography for the
Web Ecosystem}.
\newblock \bibinfo{journal}{\emph{Proc. ACM Program. Lang.}}
\bibinfo{volume}{3}, \bibinfo{number}{POPL}, Article \bibinfo{articleno}{77}
(\bibinfo{date}{Jan.} \bibinfo{year}{2019}), \bibinfo{numpages}{29}~pages.
\newblock
\showISSN{2475-1421}
\urldef\tempurl%
\url{https://doi.org/10.1145/3290390}
\showDOI{\tempurl}
\bibitem[\protect\citeauthoryear{Wood}{Wood}{2014}]%
{ethereum}
\bibfield{author}{\bibinfo{person}{Gavin Wood}.}
\bibinfo{year}{2014}\natexlab{}.
\newblock \showarticletitle{Ethereum: A secure decentralised generalised
transaction ledger}.
\newblock \bibinfo{journal}{\emph{Ethereum project yellow paper}}
\bibinfo{volume}{151} (\bibinfo{year}{2014}), \bibinfo{pages}{1--32}.
\newblock
\end{thebibliography}