RFP-6: Automated Code-Level Verifier for Motoko

[aterga]

Overview

We believe that code-level verification would be extremely beneficial to all Web3 projects, particularly high-stake applications like DeFi. Late last year, a few formal verification experts from the DFINITY Foundation came together to prototype Motoko-san, a formal, automated, code-level verifier for the Motoko smart contract language.

Conceptually, Motoko-san enables developers to leverage automatic verification to build bug-free, Web3 applications in Motoko. The current implementation is sufficient for demonstration purposes, but not for real-world applications, as the set of supported language features is minimal.

We are now sharing Motoko-san with the community and announcing our willingness to support a team that would be interested to build a more complete verifier based on our prototype.

Prototype overview

Our verification technique is called deductive formal verification. It works by translating the source code (together with its formal code-level specifications) into the Viper intermediate verification language. The resulting Viper program is then sent to the ViperServer, that returns the raw verification results (in terms of Viper). Finally, these raw verification results are mapped back to Motoko and reported to the programmer.

The tool is implemented as part of the official Motoko compiler and is written in OCaml, which is well-suited for implementing translational code. We also released a prototype language server for Motoko-san (the corresponding extension is available via the VS Code marketplace). This language server allows for rapidly testing the verifier.

Areas for Proposals

We'd like to encourage individuals and teams to explore automated code-level verification of Internet Computer canister smart contracts. The Motoko-san prototype is a great starting point for such a project.

As a first step, we are looking for a design document presenting both the existing features of the tool and the planned extensions. We are particularly interested in the following extensions:

1. Support for all basic Motoko types (e.g., Nat) and control flow structures (e.g., pattern matching)
2. Support for Arrays and HashMaps.
3. Use Motoko-san to verify a security-critical canister, such as the threshold canister (the source code of this canister will become public in the next weeks).
   • See approximate list of missing features
4. Seamless integration with ViperServer. Currently, the tool serializes the Viper encoding and saves it into a text file, which is then picked up by ViperServer that needs to parse it again. It is possible to avoid this serialization/ deserialization step, e.g., by using a JNI interface in OCaml.

For more inspiration, please read the Motoko-san documentation.

Where to start

• Install the Motoko-san prototype and try it out in VS Code
• A great place learn more about the Viper intermediate verification language is the Viper tutorial
• A complete overview for how deductive verification works is covered in the Program Verification course from ETH Zurich. Course slides can be downloaded here.
• Motoko-san has been inspired by the paper Rich Specifications for Ethereum Smart Contract Verification - OOPSLA'21

How to apply?

Please submit your application at https://dfinity.org/grants. There you'll also find more information about the DFINITY Developer Grants program in general.

If you have any questions, please contact us in the 'grants' channel on the Developer Discord.

References

• A nice summary of pros and cons of using Motoko

[domwoe]

https://serokell.io/ has been nominated to work on this RFP.