Reasoning on Smart Contracts with Temporal Logic
We propose using temporal logic to reason on Ethereum smart contracts. These are initial first steps in our research intended to start a discussion in the blockchain community.
Smart Contracts
The Ethereum blockchain has introduced smart contracts as a vehicle for trustless, secure and decentralized execution of contracts as a code.
Doing smart contract development for some time, you realize that you need to thoroughly test them for all possible contingencies. Smart contract test frameworks, enabling developers to write tests on smart contract behavior, and execute them, have been incorporated into smart contract development frameworks such as the Truffle.
Various smart contract analysis tools have been introduced, such as Mythril and Securify.
Reasoning on Smart Contracts
While writing tests and using analysis tools for smart contracts are useful, during and after development, the developer designing a collection of smart contracts, and incrementally developing them, need tools and methods with which to reason on the smart contract behavior.
Temporal Logic of Concurrent Programs
The need for formal tools with for reasoning on the execution of concurrent programs was clearly perceived many years ago. It became widely accepted that various forms of temporal logic, such as Linear Temporal Logic and Computation Tree Logic are useful for such reasoning.
Linear and Branching Temporal Logics presents a useful survey of the different approaches.
There are two predominant models for thinking about concurrent programs.
Linear Temporal Logic
Time starts at zero, proceeds in either discrete or continuous steps in a linear fashion. So time is a linear axis from zero to infinity.
A concurrent program, where different parts execute concurrently, and even more so with multiple concurrent programs executing in parallel, has many possible sequences of execution, depending on the relative time order at which different parts execute.
One can view each execution sequence of a set of programs as a linear time axis. So linear temporal logic reasons on all the possible execution sequences of a program, and tries to see what claims can be made that hold for all possible sequences of execution.
Branching Time Temporal Logic
As multiple concurrent programs execute different parts in parallel, looking forward from time zero, there are many possible future branching from each moment in time. So time is best viewed as a tree of possibilities. Each path from the root of the tree is a possible timeline, Where again, time can be either discrete or continuous.
This tree of possible executions includes all possible execution sequences, so a branching time temporal logic tries to see what claims hold for the whole tree.
Propositional vs First-Order Logic
It is clear that the state of execution of a program at each moment of time is a combination of the possible values of each variable in the program. So even for a simple program with multiple integer variables such as a smart contract,
a logic for describing program states has to be a first-order logic.
Yet research into reasoning on concurrent programs execution, such as Model Checking, the automatic verification of temporal logic formulas on program behavior, have discovered that many useful claims on program state can be expressed using propositional logic.
Subsequently, when we talk about claims, we consider propositional logic statements on program state.
Temporal Logic Operators
All forms of temporal logic for reasoning on concurrent programs include two major operators that go beyond propositional or first-order logic:
-
Eventually - a claim is going to hold in some moment in the future
-
Always - a claim is going to hold in all moments in the future
These two operators are usually augmented by two additional operators that mark one point in time and then consider what happened from there on or until that point:
-
Until - one claim is going to hold until another becomes true in the future
-
Since - since some claim became true in the past, another claim holds from that moment until the present moment
These operators can be applied to either:
-
Next moment of time - the Next operator
-
Any future or past moment of time - the Path operator
Liveness and Safety
The two prominent temporal operators of eventually and always natural correspond to two major distinct properties that the blockchain ecosystem speaks of:
-
Liveness - something will occur for sure
-
Safety - something will always hold
The Blockchain as a Model of Time
When considering the Ethereum blockchain, and more generally every blockchain, from the perspective of temporal logic, it is a sequential timeline of execution. The genesis block is the zero time of the timeline. An inter-related collection of smart contracts generate a linear discrete sequence of transactions according to where they are located in the sequence of blocks of the blockchain.
So when we want to reason on the execution of smart contracts, we have two make two choices:
-
Linear temporal logic vs branching time temporal logic
-
Discrete vs continuous time
Multiple Possible Timelines
The blockchain is a sequential timeline, produced as the result of the mining process. This process may yield from the perspective of a smart contract many possible timelines, depending on how transactions are placed in blocks and the order of blocks.
A smart contract does not know beforehand which timeline will actually be produced by the mining, yet nevertheless, a smart contract has to achieve its goals in all possible timelines.
Our Choice: Linear Temporal Logic
The basic nature of the blockchain as a sequence of blocks starting at the genesis block, where different sequences might be produced due to the characteristics of the mining process, points to linear temporal logic as the better choice. \
We want to make claims on the sequence of transactions that will occur in the blockchain, and these claims have to hold irrespective of the actual sequence that will be the result of the mining process.
Is Time Discrete or Continuous?
If you actually consider the block time, time is obviously continuous. Yet, if you look at the actual usage of time in smart contracts written in Solidity, you encounter comparisons that express claims one the present moment being before or after another moment of time. Combined with the sequential nature of the blockchain, we believe at this initial stage of research we should view time as discrete.
Using Linear Temporal Logic for Describing Smart Contracts
At this first stage, we want to start our exploration by expressing claims on smart contracts. These claims are intended to enable the developer in designing a smart contract and accompany its development. We do not argue at this state for Test-Drive Development (TDD) or verification.
As described above, we view time as linear and discrete with the genesis block placed at time zero. A claim has to hold for all possible timelines.
When reasoning on a smart contract, or a group of interrelated smart contracts, one can reduce the blockchain into a discrete timeline of blocks to be represented as a linear directed graph.
Each node is the state of the group of smart contracts after executing the transactions contained within a block.
So the first node is an empty state represented by the genesis block. Subsequently, each block of transactions is represented as an edge transforming a state into the next one which is the next node on the linear graph. This next node is the state of the smart contracts after executing the transactions in the block.
So when designing a smart contract, we do not reason about the whole state of the Ethereum but only the state of our group of smart contracts.
So let us demonstrate our approach by considering some examples.
A Basic Storage Smart Contract
contract BasicStorage {
uint storedData;
function set(uint x) {
storedData = x;
}
function get() constant returns (uint) {
return storedData;
}
}
Temporal Logic Statements for the Storage Contract
At this first article, we prefer to use informal English for the statements with burdening mathematical symbols.
-
If a
set
was executed with valuea
, then aget
in the Next state will yielda
-
If Since the
set
witha
, noset
was executed, then aget
will yielda
A Smart Contract for Real-Estate Purchase
The purchase contract is deployed by a lawyer handling the purchase. A buyer deposits funds in Ether to be transferred to the seller upon giving the keys to the apartment. There may be a sequence of deposit. If the required amount is not transferred up to predefined time, the buyer can withdraw the Ether. The funds can be withdrawn by a seller if the buyer and the lawyer approved.
contract Purchase {
address lawyer;
address buyer;
address seller;
uint256 amountDue;
uint256 startTime;
uint256 timeToLive;
bool approvedBuyer;
bool approvedLawyer;
constructor(address _buyer, address _seller, uint256 _amountDue, _uint256 timeToLive) public {
lawyer = msg.sender;
buyer = _buyer;
seller = _seller;
amountDue = _amountDue;
startTime = _timeToLive;
timeToLive = _timeToLive;
}
modifier canWithdraw() {
approvedBuyer && approvedLawyer;
_;
}
modifier didExpire() {
now > startTime + timeToLive;
_;
}
function approve() public {
if (msg.sender == buyer) {
approvedBuyer = true;
} else if (msg.sender == owner) {
approvedLawyer = true;
}
}
function() payable public {
}
function withdraw(uint256 _amount) canWithdraw() public returns(bool) {
require(_amount <= this.balance);
require(msg.sender == seller);
require(msg.sender.transfer(this.balance));
}
function expire() public didExpire() returns(bool) {
require(msg.sender == buyer);
require(this.balance > 0);
require(msg.sender.transfer(this.balance));
}
}
Temporal Logic Statements for the Real-Estate Contract
To make these statements, we make the reasonable assumption that the parties involved indeed intend to perform actions. That is, we assume the parties involved make progress.
-
If
approve
is called by the buyer and eventually followed byapprove
call by the lawyer, orapprove
is called by the lawyer and eventually followed byapprove
call by the buyer, then eventually the seller will callwithdraw
and succeed -
A
withdraw
will fail if since the contract deployment,approve
was not called by both the seller and the buyer -
An
expire
will succeed and return true, if there is no previouswithdraw
that succeeded and the call is after the time to live -
If following a successful
withdraw
anexpire
is called, it will fail
One can immediately observe for the real-estate purchase contract that since we are talking expiry times expressed using block time, we need to define propositions that specify the desirable conditions, namely, timeExpired
.
Conclusions
We proposed using temporal logic for reasoning on smart contracts and expressed a few simple statements. Our intent is to open a discussion in the community.
We intend to expand this research in several directions. These include automated contracts where for example in the case of a purchase the buyer can approve by itself the transfer of funds using a pre-image.
Beyond that, we are interested in applying the approach to payment channels.