Quick start¶

In this section, we present a common example to illustrate how VerX is used to verify custom properties. We first present two smart contracts that implement a crowdsale scenario. Then, we present relevant kinds of requirements and show how they are specified in VerX.

Smart contracts¶

We consider a crowdsale that aims to collect 10,000 ether within 30 days after deployment. The crowdsale is considered successful if 10,000 ether is collected reached within the 30 days period, in which case the beneficiary can withdraw the funds. Otherwise, the crowdsale is considered failed, and users are allowed to claim a refund. The crowdsale uses an escrow to collect all funds invested during the crowdsale. Below, we present the implementation of the crowdsale and the escrow contracts in Solidity.

The crowdsale contract is implemented as follows:

contract Crowdsale {
  Escrow escrow;
  uint256 raised = 0;
  uint256 goal;
  uint256 closeTime = now + 30 days;

  constructor(address payable beneficiary, uint256 _goal) public {
    escrow = new Escrow(beneficiary);
    goal = _goal;
  }

  function invest() payable public {
    require(now <= closeTime);
    require(raised < goal);
    escrow.deposit.value(msg.value)(msg.sender);
    raised += msg.value;
  }

  function close() public {
    require(now > closeTime || raised >= goal);
    if (raised >= goal) {
      escrow.close();
    } else {
      escrow.refund();
    }
  }
}

Variable raised tracks the amount of raised funds and the escrow stores a reference ot the escrow contract (defined shortly). The crowdsale is created by initializing the beneficiary and the goal. It then offers two functions: invest() allows any user to invest in the crowdsale while the crowdsale is active (now <= closeTime) and the goal is not reached (raised < goal). This function deposits the invested ether at the escrow (via a call to function deposit of the escrow contract) and increments the variable raised with the investment amount. Function close() allows anyone to attempt to close the crowdsale if either the crowdsale has ended (now > closeTime) or the goal is reached (raised >= goal). This function change the escrow’s state either successfully, if enough funds have been collected, or enables refunds so that investors can claim back their funds.

The implementation of the escrow is as follows:

contract Escrow {
  mapping(address => uint256) deposits;
  enum State {OPEN, SUCCESS, REFUND}
  State state = State.OPEN;
  address owner;
  address payable beneficiary;

  constructor(address payable b) public {
    beneficiary = b;
    owner = msg.sender;
  }

  function deposit(address p) onlyOwner public payable {
    deposits[p] = deposits[p] + msg.value;
  }

  function withdraw() public {
    require(state == State.SUCCESS);
    beneficiary.transfer(address(this).balance);
  }

  function claimRefund(address payable p) public {
    require(state == State.REFUND);
    uint256 amount = deposits[p];
    deposits[p] = 0;
    p.transfer(amount);
  }

  modifier onlyOwner {
    require(owner == msg.sender);
    _;
  }

  function close() onlyOwner public {
    state = State.SUCCESS;
  }

  function refund() onlyOwner public {
    state = State.REFUND;
  }
}

The escrow stores the amount of funds invested by users in a mapping deposits. The escrow allows its owner to make deposits. The escrow’s state is used to define the stateful behavior of the escrow. For example, anyone can trigger a withdraw of the investments to the beneficiary, if the escrow is in state SUCCESS. Further, it allows anyone to claim a refund if the escrow is in state REFUND. The escrow’s state is controlled by its owner (in our case, the escrow’s owner is the crowdsale contract). The state is changed via functions close() and refund.

Deployment script¶

The deployment script specifies how the contracts will be deployed on the blockchain. This is needed to precisely define the contracts’ initial state. For our example, the deployment script is defined by a single line:

Crowdsale c = new Crowdsale(0xFeedBeeF, 10000 * 10**18);

This script defines the creation of a Crowdsale contract. The arguments define the beneficiary address 0xFeedBeeF and the goal of the crowsale, which is set to ten thousand ether. Note that the deployment of this crowdsale instance would also create an escrow instance (see the crowdsale’s constructor above).

Requirements¶

We now present important requirements and illustrate how they are formalized in VerX’s specification language. We split the requirements into different classes, such as access control and invariants over aggregates. For technical information of VerX’s specification language, please refer read the Specification language section.

Access control¶

Access control requirements stipulate which users can change critical parts of the contracts’ state or trigger security-sensitive functions.

State changes In our example, it is important to ensure that only the crowdsale contract can change the state of the escrow. This requirement is formalized as follows:

// only the crowdsale can change the state of the escrow
property only_crowdsale_calls_close {
  always((Escrow.state != prev(Escrow.state))
          ==> msg.sender == Crowdsale);
}

The quantifier always is used to define an invariant, that is a property that must hold over the entire lifetime of the contract. The expression Escrow.state returns the escrow’s state, while prev(Escrow.state) returns the previous state of the escrow, before the last transaction was processed. Therefore, (Escrow.state != prev(Escrow.state) holds whenever there was a transaction that changed the escrow’s state. The second condition, msg.sender == Crowdsale enforces that the sender of the last transaction was the crowdsale contract. Note that this property does not specify which function was invoked to change the escrow’s state. For our example, there are two such functions, close() and refund().

Critical functions Another common access control idiom is to specify which users may call certain functions of the contract. For example, one may require that only the crowdsale contract may invoke the deposit(address) function of the escrow:

// only the crowdsale can call function Escrow.deposit(address)
property only_crowdsale_can_call_deposit {
  always(
    (FUNCTION == Escrow.deposit(address))
     ==> (msg.sender == Crowdsale)
  );
}

Here, FUNCTION == Escrow.deposit(address) holds only if the last transaction invokes the escrow’s deposit function. Whenever this is the case, the property stipulates that the transaction sender must be the crowdsale contract, i.e. msg.sender == Crowdsale.

State-based requirements¶

State-based properties define at which states certain authorizations and invariants must hold. For example, the sum of all deposits at the escrow must equal the escrow’s balance when the escrow is in state OPEN and REFUND. This invariant is violated when the escrow is in state SUCCESS because the beneficiary may withdraw all the funds. This requirement is formalized as follows:

// the sum of deposits equals the escrow's balance when not in state SUCCESS
property sum_of_deposits_equal_balance {
  always(
    (Escrow.state != 1)
     ==> (SUM(Escrow.deposits) == BALANCE(Escrow))
  );
}

Function SUM(Escrow.deposits) returns the sum of all deposits stored at the mapping deposits and function BALANCE returns the ether balance of the escrow contract. The implication ==> specifies that the sum of deposits equals the escrow’s balance only when its state is not SUCCESS, specified as Escrow.state != 1.

As a second example, we consider the following requirement: Functions Escrow.withdraw() and Escrow.claimRefund(address) cannot both appear in the history of the contract. Intuitively, this requirement states that invoking function withdraw() forbids function claimRefund(address) to be invoked in the future, and vice versa. This requirement is formalized as follows:

property exclusive_claimsRefund_and_withdraw {
  always(!(once(FUNCTION == Escrow.withdraw())
           && once(FUNCTION = = Escrow.claimRefund(address)));
}

The expression once(FUNCTION == Escrow.withdraw()) uses the once quantifier and evaluates to true if the expression FUNCTION == Escrow.withdraw() holds at any points in the history of the contract (i.e., if function Escrow.withdraw() was invoked in the past). This property formalizes that Escrow.withdraw() and Escrow.claimRefund(addrses) cannot both appear in the history of the contract.

State transitions¶

Smart contracts often implement non-trivial state transitions that define how their state may evolve over time. Usually the contract’s state is stored in an explicitly stored, such as the state state variable in contract escrow. An example requirement for the escrow contract is to enforce that the the SUCCESS and REFUND states are forever, that is once the contract transitions to one of these states then it is locked into the corresponding state. This is formalized as follows:

// the escrow's CLOSED state is forever
property permanent_close {
  always(once(Escrow.state == 1) ==> (Escrow.state == 1)
}

The once(Escrow.state == 1) quantifier evaluates to true whenever Escrow.state == 1 was true at some point in the history of the contract. This property therefore enforcees that if at any point the state was changed to SUCCESS, then it is bound to remain at state SUCCESS.

Invariants over aggregates¶

Contracts often store state in mappings. Since Solidity does not allow contracts to iterate over the keys of a mapping, contracts often store state in auxiliary variables to track aggregate information. Invariants over these help establish their correctness. As we saw above, a common idiom is thus to ensure that these auxiliary variables correctly store the state. For instance, the following requirement:

// the sum of deposits equals the escrow's balance
property sum_of_deposits_equals_balance {
  always(SUM(Escrow.deposits) == BALANCE(Escrow));
}

formalizes the invariant that the sum of all deposits (stored at mapping deposits of contract Escrow) must always eausl the escrow’s balance. This invariant does not hold for our example (it is violated after the beneficiary has withdrawn the funds from the escrow).

Multi-contract invariants¶

Contracts often impose invariants over the bundle of contracts in the project. In our example there are two contracts – the escrow and the crowdsale. An important requirement is to enforce that the amount of raised funds exceeds the crowdsale’s goal if the escrow is in state SUCCESS. This is formalized as follows:

// escrow is in state success only if the amount of raised
// funds exceed the goal of the crowdsale
property success_implies_goal_is_reached {
  always((Escrow.state == 1) ==> (Crowdsale.goal <= Crowdsale.raised));
}

This invariant is multi-contract it defines a dependance between the values of Escrow.state and the condition Crowdsale.goal <= Crowdsale.raised.