Formal verification tools for Move smart contracts
Smart contracts are an area with very high-security requirements, and a small, inadvertent bug could very well lead to incalculable damage.
Not long ago the Raven Project broke a very low-level bug [1]: the community developer submitted a small patch with only a few lines of changes that needed to be checked for three cases, and he intentionally left out the third case, which was actually missing an “else”. The core developer accepted the patch without finding the bug, and eventually, the attacker used the vulnerability he submitted to issue 300 million Raven Coin.
There are numerous examples in the history of smart contract development, the most famous of which is The DAO attack, which directly led to the hard fork of Ether. The main reason for this security attack is that the transfer model used by The DAO project is to transfer funds to the user before modifying the user’s balance status, which allows the attacker to construct a malicious contract to recursively call the project’s transfer function while accepting the transfer, causing the user’s balance status to keep withdrawing the project’s funds without being changed.
Is there no better solution to deal with bugs in smart contracts than to enhance testing? There is a solution — Formal verification.
Formal verification is not a new technology, it has actually existed for 30 or 40 years and is mainly used in the military, aerospace, and other fields with high requirements for system security. It is a mathematical and logic-based approach that can effectively detect the existence of security vulnerabilities in a program by rigorously proving the correctness of the code by mathematical means before it is deployed. Compared with the traditional means of finding code vulnerabilities by manual means, formal verification can solve the defect that manual means cannot exhaust all possible inputs.
Note: The picture is from the internet, the exact source is not found, we would like to express our thanks to the author of the picture!
The security features of the Move language can be divided into three levels: the language level, the virtual machine level, and the tool level.
The language level has a Rust-like ownership system, a strong data abstraction with Module-script, and assets as first-class citizens; the virtual machine level has a Java-like bytecode verifier, and the tool level provides a formal verification tool based on Boogie.
Move’s formal verification tool, called Move Prover, is based on the idea of verifying that a program conforms to a specification by means of an automatic theorem-proving solver in the formal verification domain. Move defines its own specification language, called Move specification language, which describes how a program should run correctly through preconditions, postconditions, invariants, and so on. A Move to boogie compiler then converts the Move program and specification into a boogie program, an intermediate verification language with formal semantics.
Boogie was developed by Microsoft and it has two layers. First, it is an intermediate verification language with formal semantics, designed to build program verifiers for other languages. Several program verifiers have been built based on the Boogie language, the more famous ones include VCC and HAVOC verifiers for C language. Also, Boogie is the name of the tool. The tool accepts the Boogie language as input, generates verification conditions, and passes them to the automatic theorem proving solvers Z3 or CVC4. The default solver is Z3, which is an SMT (Satisfiability Modulo Theories ) solver. Satisfiability Modulo Theories belong to the category of logic and are simply understood to give a final result, either the input program meets the given specification or it does not. A specific path is given when it does not.
Here is an example in Figure 1.0 to see how to find hidden bugs in the program by Move prover. This arithmetic() method calculates the sum of two 64-bit unsigned integers x and y, then divides by x and returns the result. At first glance, there is nothing wrong with this method, but in fact, it hides two bugs, overflow, and division by zero. The spec fun of the same name at the bottom is a specification written in the Move specification language. It specifies all possible exception exit paths for arithmetic() through two aborts_if conditional statements. The first aborts_if describes an exit due to an overflow, and the second aborts_if describes an abnormal exit with a divisor of 0. Assuming you didn’t know at first that arithmetic() could possibly exit abnormally, and spec fun arithmetic doesn’t include any abort_if conditions, then you run move prover and the result will show that there are paths to exit abnormally that are not included in the specification, and will detail the paths to exit abnormally for both of the above. After seeing these hints, you know you need to modify the arithmetic() method to add judgments for overflow and division by 0.
Figure 1.0
Let’s look at another example in Figure 2.0. If you know anything about the Move language, you know that Move provides a special bytecode for moving resources. The following Move method moves a resource of type R out from under address a, and then repackages it under the sender’s address. This method has two exception exit paths, one path is that there is no R resource under address a, and the other path is that if the sender is not equal to a, there is already another R resource under the sender. If the sender is equal to a, there will be no problem because there is no problem moving R out from under the sender and back into the sender. If the sender is not equal to a, there will be a problem because the Move language specifies that only one resource of the same type can be stored under an address, and there is already a resource of type R under the sender, which creates a conflict. If the exit condition on lines 11 or 12 is removed, move prover reports that there is an exception exit path not covered by the specification. The developer can then modify the program to add these two conditional judgments based on the specific paths.
Figure 2.0
The two examples above give a general idea of how Move prover is used, and detailed instructions can be found in the documentation accompanying the Libra code [2]. As mentioned in the Move whitepaper, Move’s long-term goal is to build a culture of “correctness” where the first thing a user does to understand the functionality of a contract is to look at its specifications. Ideally, Move programmers would not use a contract that has not been formally validated. However, the challenges of trying to achieve this goal are significant. The formal validation tool requires the user to understand the logic of the program in detail and then communicate it to the validation system in the form of a specification; whether the validation tool is accurate and intuitive, whether the specification is modular and reusable, and whether the readability is good enough are all challenges for the formal validation tool. programming.
This article is written by Guangyuz Zhu (@guangyuz), a blockchain enthusiast and former JVM expert at Alibaba. He is now working at Westar Labs, doing research on smart contract programming language, security, and scalability.