Protect Your Project Today
Strengthen your project with the largest web3 security provider.
A CertiK security expert will review your request and follow up shortly.

ERC-20 Properties For Formal Verification

Technical Blogs ·Technical Insights ·
ERC-20 Properties For Formal Verification

Technical Description

The model also formalizes a simplified execution environment of the Ethereum blockchain and a verification harness that performs the initialization of the contract and all possible interactions with the contract. Initially, the contract state is initialized non-deterministically (i.e. by arbitrary values) and over-approximates the reachable state space of the contract throughout any actual deployment on chain. All valid results thus carry over to the contract's behavior in arbitrary states after it has been deployed.

Assumptions and Simplifications

The following assumptions and simplifications apply to our model:

  • Gas consumption is not taken into account, i.e. we assume that executions do not terminate prematurely because they run out of gas.
  • The contract's state variables are non-deterministically initialized before invocation of any function. That ignores contract invariants and may lead to false positives. It is, however, a safe over-approximation.
  • The verification engine reasons about unbounded integers. Machine arithmetic is modeled using modular arithmetic based on the bit-width of the underlying numeric Solidity type. This ensures that over- and underflow characteristics are faithfully represented.
  • Certain low-level calls and inline assembly are not supported and may lead to a contract not being formally verified.
  • We model the semantics of the Solidity source code and not the semantics of the EVM bytecode in a compiled contract.

Formalism for Property Specification

All properties are expressed in linear temporal logic (LTL). For that matter, we treat each invocation of and each return from a public or an external function as a discrete time step. Our analysis reasons about the contract's state upon entering and upon leaving public or external functions.

Apart from the Boolean connectives and the modal operators "always" (written []) and "eventually" (written <>), we use the following predicates as atomic propositions. They are evaluated on the contract's state whenever a discrete time step occurs:

  • started(f, [cond]) Indicates an invocation of contract function f within a state satisfying formula cond.
  • willSucceed(f, [cond]) Indicates an invocation of contract function f within a state satisfying formula cond and considers only those executions that do not revert.
  • finished(f, [cond]) Indicates that execution returns from contract function f in a state satisfying formula cond. Here, formula cond may refer to the contract's state variables and to the value they had upon entering the function (using the old function).
  • reverted(f, [cond]) Indicates that execution of contract function f was interrupted by an exception in a contract state satisfying formula cond.

The verification performed in this audit operates on a harness that non-deterministically invokes a function of the contract's public or external interface. All formulas are analyzed w.r.t. the trace that corresponds to this function invocation.

Description of the Analyzed ERC-20 Properties

The specifications are designed such that they capture the desired and admissible behaviors of the ERC-20 functions transfer, transferFrom, approve, allowance, balanceOf, and totalSupply. In the following, we list those property specifications.

Properties related to function transfer

erc20-transfer-revert-zero

Function transfer Prevents Transfers to the Zero Address. Any call of the form transfer(recipient, amount) must fail if the recipient address is the zero address. Specification:

[](started(contract.transfer(to, value), to == address(0)) ==>
  <>(reverted(contract.transfer) || finished(contract.transfer(to, value), return
    == false)))

erc20-transfer-succeed-normal

Function transfer Succeeds on Admissible Non-self Transfers. All invocations of the form transfer(recipient, amount) must succeed and return true if

  • the recipient address is not the zero address,
  • amount does not exceed the balance of address msg.sender,
  • transferring amount to the recipient address does not lead to an overflow of the recipient's balance, and
  • the supplied gas suffices to complete the call. Specification:
[](started(contract.transfer(to, value), to != address(0) && to != msg.sender &&
    value >= 0 && value <= _balances[msg.sender] && _balances[to] + value <
    0x10000000000000000000000000000000000000000000000000000000000000000 &&
    _balances[to] >= 0 && _balances[msg.sender] <
    0x10000000000000000000000000000000000000000000000000000000000000000) ==>
  <>(finished(contract.transfer(to, value), return == true)))

erc20-transfer-succeed-self

Function transfer Succeeds on Admissible Self Transfers. All self-transfers, i.e. invocations of the form transfer(recipient, amount) where the recipient address equals the address in msg.sender must succeed and return true if

  • the value in amount does not exceed the balance of msg.sender and
  • the supplied gas suffices to complete the call. Specification:
[](started(contract.transfer(to, value), to != address(0) && to == msg.sender &&
    value >= 0 && value <= _balances[msg.sender] && _balances[msg.sender] >= 0 &&
    _balances[msg.sender] <
    0x10000000000000000000000000000000000000000000000000000000000000000) ==>
  <>(finished(contract.transfer(to, value), return == true)))

erc20-transfer-correct-amount

Function transfer Transfers the Correct Amount in Non-self Transfers. All non-reverting invocations of transfer(recipient, amount) that return true must subtract the value in amount from the balance of msg.sender and add the same value to the balance of the recipient address. Specification:

[](willSucceed(contract.transfer(to, value), to != msg.sender && _balances[to] >= 0
    && value >= 0 && _balances[to] + value <
    0x10000000000000000000000000000000000000000000000000000000000000000 &&
    _balances[msg.sender] >= 0 && _balances[msg.sender] <
    0x10000000000000000000000000000000000000000000000000000000000000000) ==>
  <>(finished(contract.transfer(to, value), return == true ==>
      _balances[msg.sender] == old(_balances[msg.sender]) - value && _balances[to]
      == old(_balances[to]) + value)))

erc20-transfer-correct-amount-self

Function transfer Transfers the Correct Amount in Self Transfers. All non-reverting invocations of transfer(recipient, amount) that return true and where the recipient address equals msg.sender (i.e. self-transfers) must not change the balance of address msg.sender. Specification:

[](willSucceed(contract.transfer(to, value), to == msg.sender && _balances[to] >= 0
    && _balances[to] <
    0x10000000000000000000000000000000000000000000000000000000000000000) ==>
  <>(finished(contract.transfer(to, value), return == true ==> _balances[to] ==
      old(_balances[to]))))

erc20-transfer-change-state

Function transfer Has No Unexpected State Changes. All non-reverting invocations of transfer(recipient, amount) that return true must only modify the balance entries of the msg.sender and the recipient addresses. Specification:

[](willSucceed(contract.transfer(to, value), p1 != msg.sender && p1 != to) ==>
  <>(finished(contract.transfer(to, value), return == true ==> (_totalSupply ==
        old(_totalSupply) && _allowances == old(_allowances) && _balances[p1] ==
        old(_balances[p1]) && other_state_variables ==
        old(other_state_variables)))))

erc20-transfer-exceed-balance

Function transfer Fails if Requested Amount Exceeds Available Balance. Any transfer of an amount of tokens that exceeds the balance of msg.sender must fail. Specification:

[](started(contract.transfer(to, value), value > _balances[msg.sender] &&
    _balances[msg.sender] >= 0 && value <
    0x10000000000000000000000000000000000000000000000000000000000000000) ==>
  <>(reverted(contract.transfer) || finished(contract.transfer(to, value), return
      == false)))

erc20-transfer-recipient-overflow

Function transfer Prevents Overflows in the Recipient's Balance. Any invocation of transfer(recipient, amount) must fail if it causes the balance of the recipient address to overflow. Specification:

[](started(contract.transfer(to, value), to != msg.sender && _balances[to] + value
    >= 0x10000000000000000000000000000000000000000000000000000000000000000 &&
    _balances[to] >= 0 && _balances[to] <
    0x10000000000000000000000000000000000000000000000000000000000000000 &&
    _balances[msg.sender] <
    0x10000000000000000000000000000000000000000000000000000000000000000 && value >
    0 && value <= _balances[msg.sender]) ==> <>(reverted(contract.transfer) ||
    finished(contract.transfer(to, value), return == false) ||
    finished(contract.transfer(to, value), _balances[to] > old(_balances[to]) +
      value -
      0x10000000000000000000000000000000000000000000000000000000000000000)))

erc20-transfer-false

If Function transfer Returns false, the Contract State Has Not Been Changed. If the transfer function in contract contract fails by returning false, it must undo all state changes it incurred before returning to the caller. Specification:

[](willSucceed(contract.transfer(to, value)) ==> <>(finished(contract.transfer(to,
        value), return == false ==> (_balances == old(_balances) && _totalSupply ==
        old(_totalSupply) && _allowances == old(_allowances) &&
        other_state_variables == old(other_state_variables)))))

erc20-transfer-never-return-false

Function transfer Never Returns false. The transfer function must never return false to signal a failure. Specification:

[](!(finished(contract.transfer, return == false)))

Properties related to function transferFrom

erc20-transferfrom-revert-from-zero

Function transferFrom Fails for Transfers From the Zero Address. All calls of the form transferFrom(from, dest, amount) where the from address is zero, must fail. Specification:

[](started(contract.transferFrom(from, to, value), from == address(0)) ==>
  <>(reverted(contract.transferFrom) || finished(contract.transferFrom, return ==
      false)))

erc20-transferfrom-revert-to-zero

Function transferFrom Fails for Transfers To the Zero Address. All calls of the form transferFrom(from, dest, amount) where the dest address is zero, must fail. Specification:

[](started(contract.transferFrom(from, to, value), to == address(0)) ==>
  <>(reverted(contract.transferFrom) || finished(contract.transferFrom, return ==
      false)))

erc20-transferfrom-succeed-normal

Function transferFrom Succeeds on Admissible Non-self Transfers. All invocations of transferFrom(from, dest, amount) must succeed and return true if

  • the value of amount does not exceed the balance of address from,
  • the value of amount does not exceed the allowance of msg.sender for address from,
  • transferring a value of amount to the address in dest does not lead to an overflow of the recipient's balance, and
  • the supplied gas suffices to complete the call. Specification:
[](started(contract.transferFrom(from, to, value), from != address(0) && to !=
    address(0) && from != to && value <= _balances[from] && value <=
    _allowances[from][msg.sender] && _balances[to] + value <
    0x10000000000000000000000000000000000000000000000000000000000000000 && value >=
    0 && _balances[to] >= 0 && _balances[from] >= 0 && _balances[from] <
    0x10000000000000000000000000000000000000000000000000000000000000000 &&
    _allowances[from][msg.sender] >= 0 && _allowances[from][msg.sender] <
    0x10000000000000000000000000000000000000000000000000000000000000000) ==>
  <>(finished(contract.transferFrom(from, to, value), return == true)))

erc20-transferfrom-succeed-self

Function transferFrom Succeeds on Admissible Self Transfers. All invocations of transferFrom(from, dest, amount) where the dest address equals the from address (i.e. self-transfers) must succeed and return true if:

  • The value of amount does not exceed the balance of address from,
  • the value of amount does not exceed the allowance of msg.sender for address from, and
  • the supplied gas suffices to complete the call. Specification:
[](started(contract.transferFrom(from, to, value), from != address(0) && from == to
    && value <= _balances[from] && value <= _allowances[from][msg.sender] && value
    >= 0 && _balances[from] <
    0x10000000000000000000000000000000000000000000000000000000000000000 &&
    _allowances[from][msg.sender] <
    0x10000000000000000000000000000000000000000000000000000000000000000) ==>
  <>(finished(contract.transferFrom(from, to, value), return == true)))

erc20-transferfrom-correct-amount

Function transferFrom Transfers the Correct Amount in Non-self Transfers. All invocations of transferFrom(from, dest, amount) that succeed and that return true subtract the value in amount from the balance of address from and add the same value to the balance of address dest. Specification:

[](willSucceed(contract.transferFrom(from, to, value), from != to && value >= 0 &&
    _balances[from] >= 0 && _balances[from] <
    0x10000000000000000000000000000000000000000000000000000000000000000 &&
    _balances[to] >= 0 && _balances[to] + value <
    0x10000000000000000000000000000000000000000000000000000000000000000) ==>
  <>(finished(contract.transferFrom(from, to, value), return == true ==>
      _balances[from] == old(_balances[from]) - value && _balances[to] ==
      old(_balances[to] + value))))

erc20-transferfrom-correct-amount-self

Function transferFrom Performs Self Transfers Correctly. All non-reverting invocations of transferFrom(from, dest, amount) that return true and where the address in from equals the address in dest (i.e. self-transfers) do not change the balance entry of the from address (which equals dest). Specification:

[](willSucceed(contract.transferFrom(from, to, value), from == to && value >= 0 &&
    value < 0x10000000000000000000000000000000000000000000000000000000000000000 &&
    _balances[from] >= 0 && _balances[from] <
    0x10000000000000000000000000000000000000000000000000000000000000000) ==>
  <>(finished(contract.transferFrom(from, to, value), return == true ==>
      _balances[from] == old(_balances[from]))))

erc20-transferfrom-correct-allowance

Function transferFrom Updated the Allowance Correctly. All non-reverting invocations of transferFrom(from, dest, amount) that return true must decrease the allowance for address msg.sender over address from by the value in amount. Specification:

[](willSucceed(contract.transferFrom(from, to, value), value >= 0 && value <
    0x10000000000000000000000000000000000000000000000000000000000000000 &&
    _balances[from] >= 0 && _balances[from] <
    0x10000000000000000000000000000000000000000000000000000000000000000 &&
    _balances[to] >= 0 && _balances[to] <
    0x10000000000000000000000000000000000000000000000000000000000000000 &&
    _allowances[from][msg.sender] >= 0 && _allowances[from][msg.sender] <
    0x10000000000000000000000000000000000000000000000000000000000000000) ==>
  <>(finished(contract.transferFrom(from, to, value), return == true ==>
      ((_allowances[from][msg.sender] == old(_allowances[from][msg.sender]) -
      value) || (_allowances[from][msg.sender] ==
      old(_allowances[from][msg.sender]) && (from == msg.sender ||
        old(_allowances[from][msg.sender]) ==
        0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF))))))

erc20-transferfrom-change-state

Function transferFrom Has No Unexpected State Changes. All non-reverting invocations of transferFrom(from, dest, amount) that return true may only modify the following state variables:

  • The balance entry for the address in dest,
  • The balance entry for the address in from,
  • The allowance for the address in msg.sender for the address in from. Specification:
[](willSucceed(contract.transferFrom(from, to, amount), p1 != from && p1 != to &&
    (p2 != from || p3 != msg.sender)) ==> <>(finished(contract.transferFrom(from,
      to, amount), return == true ==> (_totalSupply == old(_totalSupply) &&
      _balances[p1] == old(_balances[p1]) && _allowances[p2][p3] ==
      old(_allowances[p2][p3]) && other_state_variables ==
      old(other_state_variables)))))

erc20-transferfrom-fail-exceed-balance

Function transferFrom Fails if the Requested Amount Exceeds the Available Balance. Any call of the form transferFrom(from, dest, amount) with a value for amount that exceeds the balance of address from must fail. Specification:

[](started(contract.transferFrom(from, to, value), value > _balances[from] &&
    _balances[from] >= 0 && _balances[from] <
    0x10000000000000000000000000000000000000000000000000000000000000000) ==>
  <>(reverted(contract.transferFrom) || finished(contract.transferFrom, return ==
      false)))

erc20-transferfrom-fail-exceed-allowance

Function transferFrom Fails if the Requested Amount Exceeds the Available Allowance. Any call of the form transferFrom(from, dest, amount) with a value for amount that exceeds the allowance of address msg.sender must fail. Specification:

[](started(contract.transferFrom(from, to, value), value >
    _allowances[from][msg.sender] && _allowances[from][msg.sender] >= 0 && value <
    0x10000000000000000000000000000000000000000000000000000000000000000) ==>
  <>(reverted(contract.transferFrom) || finished(contract.transferFrom(from, to,
        value), return == false) || finished(contract.transferFrom(from, to,
        value), return == true && (msg.sender == from ||
        _allowances[from][msg.sender] ==
        0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF))))

erc20-transferfrom-fail-recipient-overflow

Function transferFrom Prevents Overflows in the Recipient's Balance. Any call of transferFrom(from, dest, amount) with a value in amount whose transfer would cause an overflow of the balance of address dest must fail. Specification:

[](started(contract.transferFrom(from, to, value), from != to && _balances[to] +
    value >= 0x10000000000000000000000000000000000000000000000000000000000000000 &&
    value < 0x10000000000000000000000000000000000000000000000000000000000000000 &&
    _balances[to] >= 0 && _balances[to] <
    0x10000000000000000000000000000000000000000000000000000000000000000) ==>
  <>(reverted(contract.transferFrom) || finished(contract.transferFrom(from, to,
        value), return == false) || finished(contract.transferFrom(from, to,
        value), _balances[to] > old(_balances[to]) + value -
      0x10000000000000000000000000000000000000000000000000000000000000000)))

erc20-transferfrom-false

If Function transferFrom Returns false, the Contract's State Has Not Been Changed. If transferFrom returns false to signal a failure, it must undo all incurred state changes before returning to the caller. Specification:

[](willSucceed(contract.transferFrom(from, to, value)) ==>
  <>(finished(contract.transferFrom(from, to, value), return == false ==>
    (_balances == old(_balances) && _totalSupply == old(_totalSupply) &&
    _allowances == old(_allowances) && other_state_variables ==
    old(other_state_variables)))))

erc20-transferfrom-never-return-false

Function transferFrom Never Returns false. The transferFrom function must never return false. Specification:

[](!(finished(contract.transferFrom, return == false)))

Properties related to function totalSupply

erc20-totalsupply-succeed-always

Function totalSupply Always Succeeds. The function totalSupply must always succeeds, assuming that its execution does not run out of gas. Specification:

[](started(contract.totalSupply) ==> <>(finished(contract.totalSupply)))

erc20-totalsupply-correct-value

Function totalSupply Returns the Value of the Corresponding State Variable. The totalSupply function must return the value that is held in the corresponding state variable of contract contract. Specification:

[](willSucceed(contract.totalSupply) ==> <>(finished(contract.totalSupply, return
      == _totalSupply)))

erc20-totalsupply-change-state

Function totalSupply Does Not Change the Contract's State. The totalSupply function in contract contract must not change any state variables. Specification:

[](willSucceed(contract.totalSupply) ==> <>(finished(contract.totalSupply,
      _totalSupply == old(_totalSupply) && _balances == old(_balances) &&
      _allowances == old(_allowances) && other_state_variables ==
      old(other_state_variables))))

Properties related to function balanceOf

erc20-balanceof-succeed-always

Function balanceOf Always Succeeds. Function balanceOf must always succeed if it does not run out of gas. Specification:

[](started(contract.balanceOf) ==> <>(finished(contract.balanceOf)))

erc20-balanceof-correct-value

Function balanceOf Returns the Correct Value. Invocations of balanceOf(owner) must return the value that is held in the contract's balance mapping for address owner. Specification:

[](willSucceed(contract.balanceOf) ==> <>(finished(contract.balanceOf(owner),
      return == _balances[owner])))

erc20-balanceof-change-state

Function balanceOf Does Not Change the Contract's State. Function balanceOf must not change any of the contract's state variables. Specification:

[](willSucceed(contract.balanceOf) ==> <>(finished(contract.balanceOf(owner),
      _totalSupply == old(_totalSupply) && _balances == old(_balances) &&
      _allowances == old(_allowances) && other_state_variables ==
      old(other_state_variables))))

Properties related to function allowance

erc20-allowance-succeed-always

Function allowance Always Succeeds. Function allowance must always succeed, assuming that its execution does not run out of gas. Specification:

[](started(contract.allowance) ==> <>(finished(contract.allowance)))

erc20-allowance-correct-value

Function allowance Returns Correct Value. Invocations of allowance(owner, spender) must return the allowance that address spender has over tokens held by address owner. Specification:

[](willSucceed(contract.allowance(owner, spender)) ==>
  <>(finished(contract.allowance(owner, spender), return ==
    _allowances[owner][spender])))

erc20-allowance-change-state

Function allowance Does Not Change the Contract's State. Function allowance must not change any of the contract's state variables. Specification:

[](willSucceed(contract.allowance(owner, spender)) ==>
  <>(finished(contract.allowance(owner, spender), _totalSupply == old(_totalSupply)
    && _balances == old(_balances) && _allowances == old(_allowances) &&
    other_state_variables == old(other_state_variables))))

Properties related to function approve

erc20-approve-revert-zero

Function approve Prevents Giving Approvals For the Zero Address. All calls of the form approve(spender, amount) must fail if the address in spender is the zero address. Specification:

[](started(contract.approve(spender, value), spender == address(0)) ==>
  <>(reverted(contract.approve) || finished(contract.approve(spender, value),
    return == false)))

erc20-approve-succeed-normal

Function approve Succeeds for Admissible Inputs. All calls of the form approve(spender, amount) must succeed, if

  • the address in spender is not the zero address and
  • the execution does not run out of gas. Specification:
[](started(contract.approve(spender, value), spender != address(0)) ==>
  <>(finished(contract.approve(spender, value), return == true)))

erc20-approve-correct-amount

Function approve Updates the Approval Mapping Correctly. All non-reverting calls of the form approve(spender, amount) that return true must correctly update the allowance mapping according to the address msg.sender and the values of spender and amount. Specification:

[](willSucceed(contract.approve(spender, value), spender != address(0) && value >=
    0 && value <
    0x10000000000000000000000000000000000000000000000000000000000000000) ==>
  <>(finished(contract.approve(spender, value), return == true ==>
      _allowances[msg.sender][spender] == value)))

erc20-approve-change-state

Function approve Has No Unexpected State Changes. All calls of the form approve(spender, amount) must only update the allowance mapping according to the address msg.sender and the values of spender and amount and incur no other state changes. Specification:

[](willSucceed(contract.approve(spender, value), spender != address(0) && (p1 !=
      msg.sender || p2 != spender)) ==> <>(finished(contract.approve(spender,
        value), return == true ==> _totalSupply == old(_totalSupply) && _balances
      == old(_balances) && _allowances[p1][p2] == old(_allowances[p1][p2]) &&
      other_state_variables == old(other_state_variables))))

erc20-approve-false

If Function approve Returns false, the Contract's State Has Not Been Changed. If function approve returns false to signal a failure, it must undo all state changes that it incurred before returning to the caller. Specification:

[](willSucceed(contract.approve(spender, value)) ==>
  <>(finished(contract.approve(spender, value), return == false ==> (_balances ==
      old(_balances) && _totalSupply == old(_totalSupply) && _allowances ==
      old(_allowances) && other_state_variables == old(other_state_variables)))))

erc20-approve-never-return-false

Function approve Never Returns false. The function approve must never returns false. Specification:

[](!(finished(contract.approve, return == false)))

Related Blogs

CertiK Sponsors the First Theorem Proving Competition, Supported by OpenMath
News ·Announcements

CertiK Sponsors the First Theorem Proving Competition, Supported by OpenMath

The first Theorem Proving Competition, hosted by the China Computer Federation (CCF) officially launched. The competition is supported by OpenMath, the world’s first decentralized mathematical platform, with backing from Shentu Chain and CertiK.

Stablecoin Regulation and the GENIUS Act: A Case for Formal Verification
News ·Expert Insights

Stablecoin Regulation and the GENIUS Act: A Case for Formal Verification

As Web3 adoption continues to accelerate, many central banks and institutions are developing digital asset products, such as stablecoins, to support the stability of existing blockchain ecosystems while offering transparency, speed, and flexibility. However, such stablecoin innovations must win user trust, meet regulatory requirements, and integrate with existing Web3 systems in order to acquire mainstream adoption. In the context of rigorous compliance frameworks, formal verification is a promising methodology to help build reliable stablecoin contracts by verifying essential compliance requirements.

Advanced Formal Verification of ZKP: How ZK Memory Was Proven
Technical Blogs ·Technical Insights

Advanced Formal Verification of ZKP: How ZK Memory Was Proven

In this post, we will discuss some interesting technical points that arise along our journey of verifying the zkWasm memory subsystem. The memory is the most distinctive part of a zkVM, so handling this well is a crucial point relevant for all other zkVM verification projects as well.