2018-02-28
We present a formal verification of the Bihu KEY token operation contracts, upon request from the Bihu team represented by Dr. Bin Lu (Gulu) and Mr. Huafu Bao.
Bihu is a blockchain-based ID system, and KEY is the utility token for the Bihu ID system and community.
The smart contracts requested to be formally verified are the ones for operating the KEY token. The Solidity source code of those contracts and their informal specification are publicly available.
This directory contains the artifact of the Bihu contracts' formal verification, as a companion to the formal verification report:
Bihu Smart Contract Formal Verification
The target contracts of our formal verification are the following, where we took the Solidity source code from Bihu's Github repository, https://github.com/bihu-id/bihu-contracts, commit f9a7ab65:
More specifically, we formally verified the functional correctness of the following two functions:
We verified mathematically equivalent variants of each target function.
Due to time constraints (we only had two weeks to complete this verification project), we have not verified the external calls to key.balanceOf and key.transfer.
We took the modified source code, inlined the DSMath contract and the DSToken contract interface, and compiled it to the EVM bytecode using Remix Solidity IDE (of the version soljson-v0.4.20+commit.3155dd80).
The modified and inlined source code of (the contracts of) each target function:
The EVM (runtime) bytecode generated by the Remix Solidity compiler:
- collectToken/KeyRewardPool.modified.inlined.bytes
- forwardToHotWallet/WarmWallet.modified.inlined.bytes
The Remix IDE-generated Gist links:
- collectToken/KeyRewardPool.modified.inlined.gist: https://gist.github.com/anonymous/61b969d0f7af252a54f48f4b50f2c3f5
- forwardToHotWallet/WarmWallet.modified.inlined.gist: https://gist.github.com/anonymous/b7773008aa9dc75815f1c6ecfb7224a0
The (annotated) EVM assemblies disassembled from each bytecode:
The original, inlined source code of (the contracts of) each target function:
- collectToken/KeyRewardPool.inlined.sol [Gist link]
- forwardToHotWallet/WarmWallet.inlined.sol [Gist link]
Following our formal verification methodology described above, we formalized the high-level specification of the smart contracts based on the informal specification, and the Bihu team has confirmed that the specification correctly captured the intended behavior of their contract. Then, we refined the specification all the way down to the Ethereum Virtual Machine (EVM) level to capture the EVM-specific details. The EVM-level specification is fully mechanized within and automatically verified by our EVM verifier, a correct-by-construction deductive program verifier derived from KEVM and K-framework's reachability logic theorem prover.
The following are the mechanized EVM-level specifications of each target function:
- EVM specification of
collectToken: collectToken-spec.ini - EVM specification of
forwardToHotWallet: forwardToHotWallet-spec.ini
The specifications are written in eDSL, a domain-specific language for EVM specifications, which must be known in order to thoroughly understand our EVM-level specifications. Refer to resources for background on our technology. The above files provide the eDSL specification template parameters. The full K reachability logic specifications are automatically derived by instantiating a specification template with these template parameters.
Run the following command in the root directory of this repository, and it will generate the full specifications under the directory specs/bihu:
$ make bihu
Run the EVM verifier to prove that the specifications are satisfied by (the compiled EVM bytecode of) the target functions. See these instructions for more details of running the verifier.
Q: In WarmWallet.modified.inlined.sol, the paused boolean is declared. The bool type is equivalent with the uint8 type, but in the spec file (forwardToHotWallet-spec.ini), the storage location named PAUSED is verified as an uint256. Shouldn't it be
andBool 0 <=Int PAUSED andBool PAUSED <Int (2 ^Int 8)
instead?
Also, in a failure case, it looks like the storage slot is compared to a shifted value.
andBool PAUSED ==Int 1 <<Int (20 *Int 8)
A:
All storage locations have a size of 32 bytes, and multiple items of elementary types that need less than 32 bytes, such as bool or address could be packed into a single storage location only if they fit (Layout of State Variables in Storage).
In the contract, the paused boolean is declared right after the owner address, and since they both have a combined size of less than 32 bytes (20 from address and one from bool) they are both kept in the same storage slot, which in the spec file is referenced as PAUSED.
Therefore, in order to check that the boolean is true, the storage slot is compared with the value of 1 which is shifted 160 bits (representing the width of the address type) to the left. But this logic is valid only if the address is presumed to be 0.