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: .. code-block:: solidity 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: .. code-block:: solidity 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: .. code-block:: javascript 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: .. code-block:: solidity // 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: .. code-block:: solidity // 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: .. code-block:: solidity // 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: .. code-block:: solidity 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: .. code-block:: solidity // 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: .. code-block:: solidity // 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: .. code-block:: solidity // 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``.