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 value a, then a get in the Next state will yield a
If Since the set with a, no set was executed, then a get will yield a

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 by approve call by the lawyer, or approve is called by the lawyer and eventually followed by approve call by the buyer, then eventually the seller will call withdraw 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 previous withdraw that succeeded and the call is after the time to live
If following a successful withdraw an expire 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.

Yoramk Digital Life

Yoram Kornatzky