Bihu Smart Contract Formal Verification
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.
This directory contains the artifact of the Bihu contracts' formal verification, as a companion to the formal verification report:
Target Smart Contracts
More specifically, we formally verified the functional correctness of the following two functions:
Solidity Source Code and Compiled EVM Bytecode
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
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
The modified and inlined source code of (the contracts of) each target function:
The EVM (runtime) bytecode generated by the Remix Solidity compiler:
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]
Mechanized Specifications and Proofs
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
- EVM specification of
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
$ 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)
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)
All storage locations have a size of 32 bytes, and multiple items of elementary types that need less than 32 bytes, such as
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
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.