The RV Bounded Model Checker - A lightweight semantics-based tool
Smart contract failures can cost millions of dollars and can even lead to death of companies and of cryptocurrencies. Moreover, smart contracts are easier to attack by hackers than ordinary software, simply because they are public on the blockchain and anyone can invoke them from anywhere. Therefore, there is an unprecedented need to guarantee the correctness of code.
It is well-known that the only way to guarantee code correctness is through the use of rigorous formal methods, where the correctness of the smart contract is expressed mathematically as a formal property, the programming language or virtual machine is also expressed mathematically as a formal model, and the former is rigorously proved from the latter. Moreover, the correctness of smart contracts must be independently checkable, without having to trust their authors or any auditing authorities. Therefore, they must be provided with machine checkable correctness certificates.
We at Runtime Verification (RV) have developed a language-parametric, fully-fledged formal verification tool for smart contracts, based on matching μ logic, and incorporates the best techniques, algorithms, and mathematical foundations developed by the formal methods community. The tool is language-parametric, meaning that it can be quickly instantiated for any language (or virtual machine) by simply plugging-in a formal semantics of the language. Currently, we have instantiated it for EVM, and have used the EVM verifier to verify the full functional correctness of high-profile smart contracts, including ERC20 token contracts, Ethereum Casper FFG contract, and the DappHub MakerDAO contract.
The fully-fledged verifier, however, requires considerable effort and expertise to use. For example, devising and debugging formal specifications is a highly non-trivial task for non-experts. The task not only requires substantial knowledge of theorem proving and logic but also may require users to identify custom abstractions and corresponding lemmas to reason about certain program behaviors. Because of these reasons, our current formal verification tool is inherently interactive and only a few experts can use it effectively. Consequently, in spite of its semantics-based rigor, the use of our existing formal verification tool is quite limited outside our team, and we believe it is impractical to even attempt to use it in the early phase of contract development and/or on a daily basis, or by a small business that cannot afford a large formal verification effort.
To bring formal techniques into daily contract development, we are developing a fully automatic, lightweight formal verification tool for contract developers. The tool will be available to the community as a component of K's haskell backend). This tool is fully automatic, in that it will not require additional human effort other than providing the program and a set of properties to be verified. The properties can be predefined properties that are universal for any program, such as no overflow or division-by-zero, or other user-defined properties (e.g., assertions). Moreover, the tool will still provide the same full formal guarantee as the fully-fledged verifier with respect to some bound of execution steps.
Example property:
On all execution paths (AG), if division by zero happens, the program will eventually terminate (EF) in a revert state. Note: AG and EF are temporal operators intrduced by Computation Tree Logic (CTL), which are easily definable in matching μ logic (done in this LICS’19 paper).
Our tool will work as follows. Starting with a generic symbolic initial state, it will symbolically execute the entire program, which will attempt to give us all possible paths and (symbolic) states reachable in the program execution. Bugs will be reported whenever a state that violates any of the properties is reached. If the program has unbounded loops or recursion, however, the symbolic execution may not terminate without a human guide (i.e., annotating loop invariants). To make the tool fully automatic, loops will be unrolled up to a finite number of iterations, called a bound. In this case, the tool will explicitly report the unexplored iterations in which potential bugs may still exist!. Moreover, based on extensive experience we have accumulated while manually verifying smart contracts, we came up with a set of generic lemmas and abstractions which will speed up the state exploration.
In the context of smart contracts, our proof-of-concept tool implementing this BMC technique is extremely useful and effective. That is because smart contracts are usually small and terminating programs, which rarely have loops or recursion. Languages like Vyper even disallow recursive calls and infinite-length loops as part of the language design. Consequently, it is expected that in most cases our tool will go beyond just finding bugs. It will in fact be able to prove the functional correctness of most smart contracts, completely automatically.