Skip to content

Latest commit

 

History

History
189 lines (125 loc) · 13.7 KB

README.md

File metadata and controls

189 lines (125 loc) · 13.7 KB
Raw

2018-01-16

Formal Verification of HackerGold (HKG) ERC20 Token Contract

We present a formal verification of HackerGold (HKG) ERC20 token contract.

The HackerGold (HKG) token is an ERC20 token written in Solidity, which became well-known when a serious security vulnerability was discovered that even survived a security audit performed by Zeppelin. Specifically, the bug was due to a typographical error in the source code, using =+ instead of += for updating a receiver’s balance during a transfer, which would allow an attacker to reset an account balance. This security issue was resolved by deploying a new, fixed contract and reissuing the tokens.

We found that the HKG token implementation does not conform to the ERC20 standard, and deviates from the ERC20-K (and thus ERC20-EVM) specification as follows:

  • No totalSupply function: No totalSupply function is provided in the HKG token, which is not compliant to the ERC20 standard.

  • Returning false in failure: It returns false instead of throwing an exception in case of failure for both transfer and transferFrom. It does not violate the standard, as throwing an exception is recommended but not mandatory according to the ERC20 standard:

"The function SHOULD throw if the from account balance does not have enough tokens to spend."

  • Rejecting transfers of 0 value: It does not allow transferring 0 value (for both transfer and transferFrom), returning false immediately without logging any event. It is not compliant to the standard, as the standard explicitly states that:

"transfers of 0 values MUST be treated as normal transfers and fire the Transfer event."

This is a potential security vulnerability for any API clients assuming the ERC20-compliant behavior.

  • No overflow protection: It does not check arithmetic overflow, resulting in the receiver's balance wrapping around the 256-bit unsigned integer's maximum value in case of the overflow (for both transfer and transferFrom). It does not violate the standard, as the standard does not specify any requirement regarding it. However, it is questionable and potentially vulnerable, since it will result in loss of the funds in case of the overflow as the receiver's balance wraps around to a lower-than-expected value. We ask any API clients to be careful, having additional detection and protection mechanism for the arithmetic overflow, when using the HKG token.

Target Smart Contract

The target contract of our formal verification has the following Solidity source code, taken from the Github repository https://github.com/ether-camp/virtual-accelerator at commit 42258200:

We formally verified the full functional correctness of the following ERC20 functions:

Verification Artifacts

Solidity Source Code and Compiled EVM Bytecode

We took the source code, inlined the TokenInterface contract, and compiled it to the EVM bytecode using Remix Solidity IDE (version soljson-v0.4.19+commit.c4cbbb05).

The inlined source code of the contract is the following:

The EVM (runtime) bytecode generated by the Remix Solidity compiler is the following:

The Remix IDE-generated Gist link:

The (annotated) EVM assembly disassembled from the bytecode is the following:

Mechanized Specifications and Proofs

Due to its deviation from ERC20-K, we could not verify the HKG token against the original ERC20-EVM specification. In order to show that it is "correct" w.r.t. ERC20-K (thus ERC20-EVM) modulo the deviation, we modified the specification to capture the deviation and successfully verified it against the modified ERC20-EVM specification. Below are the changes made to the original ERC20-EVM specification:

  • To capture the absence of the totalSupply function, we wrote a new specification for totalSupply that throws an exception immediately when being called, as follows:

    [totalSupply]
k: #execute => #halt
callData: #abiCallData("totalSupply", .TypedArgs)
localMem: .Map => _:Map
gas: #gas({GASCAP}, 0, 0) => _
log: _
refund: _
storage: _:Map
requires:

    Note that the local memory could end up with some contents due to the function signature extraction process, for which some gas will be consumed. Other than that, nothing (log, refund, and storage) will be updated.

  • To capture the false return value, we changed the k and localMem parameters of the transfer-failure section, from:

    k: #execute => #halt
localMem: .Map => _:Map

    to:

    k: #execute => (RETURN RET_ADDR:Int 32 ~> _)
localMem: .Map => .Map[ RET_ADDR := #buf(32, 0) ] _:Map

    The modified parameter values specify that it returns false (denoted by 0) instead of throwing an exception. We changed the transferFrom-failure section similarly as the above.

  • To capture the rejection of transferring 0 value, we added the following additional requires conditions, one for the success cases:

    andBool VALUE >Int 0

    and its complement for the failure cases:

    orBool VALUE <=Int 0

    Note that the above complement, combined with the value range condition, implies VALUE ==Int 0.

  • To capture the arithmetic overflow behavior, we changed the storage parameter values, from:

    #hashedLocation({COMPILER}, {_BALANCES}, TO_ID) |-> (BAL_TO => BAL_TO +Int VALUE)

    to:

    #hashedLocation({COMPILER}, {_BALANCES}, TO_ID) |-> (BAL_TO => BAL_TO +Word VALUE)

    Note the difference between +Word and +Int. The +Word operation wraps around 2**256 − 1, the maximum unsigned 256-bit integer value, while the +Int operation is the mathematical integer addition (i.e., the arbitrary precision integer addition).

    Also, we dropped the requires conditions for the overflow, the one for the success cases:

    andBool BAL_TO +Int VALUE <Int (2 ^Int 256)

    and its complement for the failure cases:

    orBool BAL_TO +Int VALUE >=Int (2 ^Int 256)

The full changes made in ERC20-EVM are shown in here. The specifications of other functions except transfer and transferFrom are the same as the original ERC20-EVM.

We took the modified ERC20-EVM specification and instantiated it with the program-specific parameters shown below.

[pgm]
compiler: "Solidity"
_totalSupply: 0
_balances: 1
_allowances: 2
code: "0x60606040526004361061006d576000357c0100000000000000000000000000000000000000000000000000000000900463ffffffff168063095ea7b31461007257806323b872dd146100cc57806370a0823114610145578063a9059cbb14610192578063dd62ed3e146101ec575b600080fd5b341561007d57600080fd5b6100b2600480803573ffffffffffffffffffffffffffffffffffffffff16906020019091908035906020019091905050610258565b604051808215151515815260200191505060405180910390f35b34156100d757600080fd5b61012b600480803573ffffffffffffffffffffffffffffffffffffffff1690602001909190803573ffffffffffffffffffffffffffffffffffffffff1690602001909190803590602001909190505061034a565b604051808215151515815260200191505060405180910390f35b341561015057600080fd5b61017c600480803573ffffffffffffffffffffffffffffffffffffffff169060200190919050506105c6565b6040518082815260200191505060405180910390f35b341561019d57600080fd5b6101d2600480803573ffffffffffffffffffffffffffffffffffffffff1690602001909190803590602001909190505061060f565b604051808215151515815260200191505060405180910390f35b34156101f757600080fd5b610242600480803573ffffffffffffffffffffffffffffffffffffffff1690602001909190803573ffffffffffffffffffffffffffffffffffffffff16906020019091905050610778565b6040518082815260200191505060405180910390f35b600081600260003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060008573ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020819055508273ffffffffffffffffffffffffffffffffffffffff163373ffffffffffffffffffffffffffffffffffffffff167f8c5be1e5ebec7d5bd14f71427d1e84f3dd0314c0f7b2291e5b200ac8c7c3b925846040518082815260200191505060405180910390a36001905092915050565b600081600160008673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000205410158015610417575081600260008673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000205410155b80156104235750600082115b156105ba5781600160008673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000206000828254039250508190555081600160008573ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000206000828254019250508190555081600260008673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020600082825403925050819055508273ffffffffffffffffffffffffffffffffffffffff168473ffffffffffffffffffffffffffffffffffffffff167fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef846040518082815260200191505060405180910390a3600190506105bf565b600090505b9392505050565b6000600160008373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020549050919050565b600081600160003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002054101580156106605750600082115b1561076d5781600160003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000206000828254039250508190555081600160008573ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020600082825401925050819055508273ffffffffffffffffffffffffffffffffffffffff163373ffffffffffffffffffffffffffffffffffffffff167fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef846040518082815260200191505060405180910390a360019050610772565b600090505b92915050565b6000600260008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060008373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020549050929150505600a165627a7a723058206cb5284e8795f7d1c570318732bc1cb8add2222946156c0ba28c946531c4a2f50029"
gasCap: 100000

The resulting specification is the following:

The specification is written in eDSL, a domain-specific language for EVM specifications, which must be known in order to thoroughly understand our EVM-level specification. Refer to resources for background on our technology. The above file provides the eDSL specification template parameters. The full K reachability logic specification is automatically derived by instantiating a specification template with these template parameters.

Run the following command in the root directory of this repository to generate the full specification under the directory specs/hkg-erc20:

$ make hkg-erc20

Run the EVM verifier to prove that the specification is satisfied by (the compiled EVM bytecode of) the target functions. See these instructions for more details of running the verifier.

Resources

Disclaimer