Formal verification
Formal verification is the highest form of quality assurance for software. Given a specification of what the system should do, formal verification tools check whether this specification is satisfied by a model of the system. The unique advantage of formal verification is that it can not only find bugs but also formally prove their absence – including the absence of security bugs. This goes beyond what testing or manual audits can achieve.
The proof is always relative to the model and the specification. Any simplifications and assumptions in the model, or omissions in the specification, may hide bugs and attacks. On the other hand, verification can require a lot of effort, and model simplifications can make it significantly easier.
For a concrete example, when verifying the ckBTC minter canister, the DFINITY team used models that exclude the possibility of calling the update_balance canister method more than 2 times concurrently. This potentially misses attacks that require 3 or more concurrent calls to update_balance to trigger a bug. But we considered such bugs highly unlikely and, in return, we were able to run a fully automatic verification process, which was much cheaper than other verification methods.
There are many existing formal verification tools. While none of them take into account the specifics of ICP yet, many of them are general enough that they can be applied to canisters. In particular, the DFINITY team has made good use of the TLA+ toolkit to combat reentrancy bugs, a type of concurrency bug where one method of a particular canister is called while another one is still executing.
These bugs are particularly difficult to find, as they can involve unexpected interactions of code scattered throughout a canister, or even in different canisters. The number of such code interactions may be huge, and thus difficult for humans to detect. These interactions are usually difficult to test automatically and systematically, which TLA+ can do.
TLA+
The Temporal Logic of Actions (TLA+) is a language for specifying and verifying complex systems. TLA+ comes with a set of tools for lightweight formal verification in the form of so-called model checking. Through model checking, it exhaustively (within bounds, such as the aforementioned 2 concurrent calls bound) explores all possible concurrent interactions of a model of the code — exactly the domain that is difficult to test — and finds bugs.
Importantly, after building the model of the code, model checking runs with virtually no further human input, making it highly cost-effective. To illustrate with some made-up numbers: if the industry standard practices (such as testing and security reviews) eliminate 80% of the bugs, and “heavyweight” formal verification eliminates 99.99%, with TLA+ you can eliminate 90% with a fraction of the effort of the heavyweight verification.
We have used TLA+ to create the following models that can be interesting for dapp developers:
- NNS and SNS governance (focusing on interactions with the ledger canister).
- ICP ledger (focusing on block archival).
- ckBTC minter.
- SNS swap canister.
- People parties dapp.
To find out more on why and how you can apply TLA+ to your canisters and dapps, including an in-depth guide to modeling canisters, refer to our series of blog posts (1, 2, 3). You can also look at the DFINITY-produced TLA+ models for examples and techniques.