Verification of an Actor-Based Smart Contract Language
General Background
Motoko is a language used for developing distributed applications on the Dfinity Internet Computer [1]. It is an actor-based programming language with native support for asynchronous computation. Motoko programs are called canisters or canister smart contracts and are executed inside the Internet Computer, which is a kind of blockchain.
Like smart contracts on other blockchains (e.g., Ethereum), Motoko canisters are a great use case for formal verification: They are usually comparatively small programs, s.t. full verification is achievable without prohibitive effort, and, since bugs in them can potentially lead to financial losses for the involved parties, there is especially high interest in ensuring their correctness beyond the assurance that standard techniques like testing can provide. The latter is especially true for Motoko, whose actor-based design can allow for unexpected interleavings of code, which potentially lead to concurrency bugs that are difficult to find using testing.
Project Background
Dfinity recently released a very early prototype verifier for Motoko [2], based on the Viper verification infrastructure [3], that is integrated with the Motoko compiler. Their vision for the verifier is for it to be usable by non-experts, which means in particular to make specifications understandable in terms of existing Motoko concepts as much as possible. The current prototype handles only a small subset of the language, and does not fully address the challenges of verifying asynchronous code.
Dfinity has committed to supporting projects that extend the prototype to a full-fledged verification tool.
Goals
The goal of this project is to develop an overall methodology for accessible verification of actor-based programs and implement it in the existing prototype, which will then enable us to verify realistic Motoko contracts. In particular, this goal requires designing specification and verification techniques for asynchronous, actor- and message-based programs (these techniques may potentially be applicable to other languages as well), and to define a specification and verification methodology that does not rely on advanced specification concepts, but still allows for precise and scalable verification of complex properties.
More concretely, the goals are:
- designing an expressive specification and verification technique for actor-based, asynchronous programs
- designing an encoding from Motoko to the Viper intermediate language that allows for scalable verification (i.e., in particular, a handling of program state and function calls that is both scalable and easy to specify)
- implementing this encoding as an extension of the the current prototype (in OCaml)
- and evaluating the tool on a number of real-world contracts.
Useful Prerequisites
Previous experience with deductive verification tools (e.g. through the Program Verification course at ETH) is useful, but not necessarily required.
Contact
References
[2] external page https://github.com/dfinity/motoko/blob/master/src/viper/README.md