Developer Grant for Code-Level Verification in Motoko
A Motoko code verifier for building bug-free Web3 applications on the Internet Computer could help improve blockchain safety. DFINITY issues a grant and prototype Motoko verifier for ICP developers to explore further.
According to data from rekt.news, blockchain vulnerabilities are often exploited via smart contracts. Code audits — the most widely-used approach to quality assurance in high-stake Web3 projects — are insufficient, as they are limited to basic practices, such as manual code review and automatic code analyzers that cannot guarantee a blockchain’s safety against attacks, exploits or arbitrages. In fact, since September 2020, the industry has reported over $1.15 billion in asset losses among users of audited blockchain projects.
One way to prove or disprove the correctness of algorithms underlying smart contracts is through formal verification. Formal verification can be tricky. Verification experts at the DFINITY Foundation have been experimenting with techniques to specify and verify Motoko canister smart contracts on the Internet Computer (ICP). Their research resulted in creation of a Motoko code verifier — an early prototype developed to explore an approach to dramatically simplify the development of formally secure async code. As the Motoko code verifier has the potential to be very beneficial to ICP developers, especially those building high-stake applications in DeFi, DFINITY is making its prototype publicly available and issuing grants to developers interested in extending it for real-world Motoko canisters.
But first here is a preview of what was discovered in our research on verification-assisted development in Motoko.
Actors Can Hide Tricky Bugs
Smart contracts are like games with an unknown number of players. To ensure that a game is sensible, rules need to be specified in a way that is both formal, to avoid ambiguity, and concise, so that players can wrap their heads around the rules and play strategically. The rules also need to be verified to prove that implementation (i.e., executable code) actually respects the rules of the game. But formally verifying a system of rules is tricky. It constitutes mathematically proving that the rules of the game cannot be bypassed, even under the assumption that the players are coordinating adversaries, trying to exploit any vulnerabilities. Moreover, since the number of players is unknown upfront (serving an arbitrary number of users is typically the point of a Web3 application), we must resort to protecting against infinitely-many adversaries.
Why is Testing Insufficient?
Coming back from the game analogy, we noted that runtime validation techniques like testing cannot provide sufficient security guarantees for smart contracts. The reasons are well known: Testing validates only some execution scenarios, and typically only covers a tiny subset of all possible executions. Therefore, it is practically impossible to validate all execution scenarios of a smart contract simply by testing it.
Towards Formal Verification
Formal verification is a compile-time technique that validates all possible execution scenarios. The expressivity of Motoko’s asynchronous, actor-based paradigm (async) complicates verification. Other common smart contract languages, such as Solidity and Vyper, do not support async, making them easier to verify. However, this sync-only paradigm severely restricts their domain of use. The reason async complicates verification is because it involves dynamic interleaving of code execution that cannot be precisely predicted at compile time, which can make the behavior of async code counterintuitive even to the programmer who wrote it. The implicit assumptions made by programmers while writing async code are especially hard to communicate when multiple people are working on the same async smart contract. This often results in notorious bugs that can be exploited, such as in reentrancy attacks.
Despite all these challenges, recent progress in formal verification demonstrates that the right kind of tools can dramatically simplify the development of formally secure async code. Our prototype demonstrates this point for the Motoko language, but the core principles are language-independent, indicating that ICP developers, whatever their choice of language, could leverage automatic verification to build Web3 applications that are bug-free with regard to their specifications.
Case Study: Verifying Reentrancy Safety of ClaimReward
We demonstrate code-level verification based on the ClaimReward smart contract. While ClaimReward is just a demo canister, it exposes the problem that frequently occurs in real-world smart contracts. Some reentrancy attacks could be prevented by using append-only structures, e.g., ledgers. However, developers often prefer structures that support in-place mutations, in particular, because that can offer better performance. This technique allows verifying reentrancy safety in both of these cases, one function at a time.
Using this technique, programmers can implement smart contracts and specify their essential properties (i.e., what conditions would imply that there’s a bug?) using that same language — Motoko — while our tool, Motoko-san, automatically checks whether the implementation always respects the specification.
A practically limiting factor of any verification technique is its usability. One huge advantage of our technique is that it does not require the developer to learn how to use a new language or tool; reasoning is done by using only the concepts that Motoko already has. Motoko-san demonstrates compile-time automation and IDE integration, making the overall technique comparable, in terms of the learning curve, to using a type checker.
To Sum it up
Recent data shows that smart contracts passing human audits can still hide bugs, resulting in huge money losses for their users. Formal verification is needed to rule out such bugs.
It is essential to formally verify Web3 applications, which tend to promise a lot to their users in terms of security, privacy, and reliability. Unlike runtime techniques like testing, which validate only a subset of smart contract executions, formal verification validates all possible executions, ensuring that these promises are always met. What’s more, developers and users should be able to understand the formal specification of a smart contract. The code-level specification approach presented here meets this requirement.
Call to action
The Internet Computer — in particular, its Motoko programing language — is well-suited for building next-generation developer tooling, including automatic code-level verifiers. On that note, we are sharing Motoko-san with the community and announcing a grant opportunity for developers interested in building a more complete verifier based on our prototype.
Get the details and formal request for proposals here.
Finally, we look forward to reading what your thoughts are on code-level verification for Web3. Are you enthusiastic about the prospect or a formally verified public ecosystem of distributed apps? Or maybe you’re skeptical? Let’s continue this discussion in the ICP Forum.
Further reading
- A nice summary of pros and cons of using Motoko
- Motoko-san has been inspired by the paper Rich Specifications for Ethereum Smart Contract Verification — OOPSLA’21
- Motoko-san is powered by Viper
- Read more about DFINITY’s formal verification initiative
- Internet Computer motion proposal on Formal Verification
