Formal Verification of a Token Contract
Following on from my previous post on verifying an auction contract in Whiley, I thought it might be useful to look at a more challenging example. A token contract is a very common form of smart contract which allows someone to create and manage their own currency. On Ethereum, token contracts have been standardised in the under ERC20.
A very simple token contract maintains, for each account, a balance of tokens owned by that account. Account holders can transfer tokens to others, but only the contract owner can mint new tokens. The following defines the various components maintained by the contract:
// Account balances map<uint160,uint256> tokens // Total tokens in circulation uint256 total // Contract owner uint160 owner
Explicitly maintaining the total number of tokens in circulation may seem unnecessary (i.e. because it can be computed from the map). However, in the context of a smart contract it is useful to avoid such computation (as this can become prohibitively expensive).
Consider the following implementation of
transfer() which includes
an incomplete specification of what is required for it to execute
(otherwise it reverts) along with the properties that it ensures.
// Transfer some amount of tokens // from one account to another. method transfer(uint160 to, uint256 val) // (1) Ensure sufficient funds requires tokens[msg::sender] >= val // (2) Ensure sender balance decreased ensures tokens[msg::sender] == old(tokens[msg::sender]) - val // (3) Ensure target balance increased ensures tokens[to] == old(tokens[to]) + val: tokens[msg::sender] = tokens[msg::sender] - val tokens[to] = tokens[to] + val
As expected, the transfer cannot complete unless the account holder
has sufficient funds (item
(1) above). Likewise, upon completion,
the account sender’s balance must have decreased (item
accordingly, the destination account balance must have increased
(3)). The power of a formal verification tool like Whiley is
that we can statically check whether or not our implementation meets
this specification. In fact, attempting to verify the above in Whiley
will immediately raise some errors:
- (Integer Overflow). Our implementation above suffers from an integer overflow whereby the value sent overflows target’s balance. Such flaws are certainly exploitable (and have been in the past).
- (Logic Error). Our specification also suffers from a more
subtle form of logic error. The problem arises when
msg::sender == toas, in such case, items
(3)cannot simultaneously hold for the same account!
To resolve these issues and allow the method to pass verification, we must extend the specification with two more requirements:
// (4) Prevent overflow in target account requires tokens[to] + val <= MAX_UINT256 // (5) Cannot transfer to myself! requires msg::sender != to
The first of these requirements simply prevents an overflow from occuring, whilst the latter represents one way of fixing the specification (though not the only way).
The following illustrates our implementation of
mint() including its
// Mint new coins into target account method mint(uint160 to, uint256 val) // Only the owner can mint new coins requires msg::sender == owner // Prevent overflow in target account requires tokens[to] + val <= MAX_UINT256 // Prevent overflow of total requires (total + val) <= MAX_UINT256 // Ensure target balance increased ensures tokens[to] == old(tokens[to]) + val: tokens[to] = tokens[to] + val total = total + val
As before checks are required to protect against overflow, and also to
ensure that only
owner can mint new tokens.
An interesting observation is that the contract maintains an invariant over its storage state.
total matches the number of tokens distributed to
all account holders. Using Whiley, we can verify this invariant
Roughly speaking, to make this work we define
sum(map<uin160,uint256> tokens) as a property which sums the tokens from all accounts in the
map. Using our property, we can then extend the specification for
transfer() as follows (and similarly for
// Transfer some amount of tokens // from one account to another. method transfer(uint160 to, uint256 val) ... // (2) Invariant holds on entry requires sum(tokens) == total ... // (5) Invariant holds on exit ensures sum(tokens) == total: ...
What remains is to verify this property holds. In fact, this presents some challenges for the verifier used in Whiley, and requires some additional hints (in the form of lemmas).
We have demonstrated how a verification tool like Whiley can be used to verify key properties of our contracts hold. Since Whiley does not yet compile to Ethereum bytecode, this remains a proof-of-concept. Still, the value from doing this should hopefully be apparent!