DFINITY Foundation

Internet Computer Association

Build long term R&D efforts for Formal Verification (from which multiple projects will emerge)



# Objective

Use formal verification techniques to increase the confidence that the Internet Computer is secure and behaves as expected.


# Summary

The Internet Computer (IC) provides a secure environment for the canister smart contracts executing on it. But like any software stack, the IC can contain bugs, even with best practices such as testing and code reviews. Bugs can directly compromise the security of canisters, making the canisters unavailable, or losing or corrupting the data of canisters, e.g., changing the balances in the ledger canister. The open, permissionless nature of the IC means that such bugs can be triggered not only spontaneously, but also exploited by malicious actors. While disaster recovery procedures help fix such problems, they take time and may be insufficient in many cases, for example, if an attacker manages to steal ICP utility tokens or create them out of thin air. Formal verification dramatically reduces the risk of bugs in a system, including security vulnerabilities.

# Background

Formal verification is a general technique to improve the quality of software systems. It does this by specifying the desired system properties, and proving that a model of the system satisfies these properties. The specification and the satisfaction proof are done using rigorous mathematical techniques that are mechanized in software (so-called formal methods). The mathematical rigor ensures that the specification is unambiguous, and that the proof has no gaps.

Note that the risk of a bug or a vulnerability is not completely eliminated even with formal verification. For example, one could forget to include some desired properties in the specification. Also, the model could diverge from the actual system: for example, a model using (unbounded) natural numbers may miss arithmetic overflow problems that appear in a real system that uses 32-bit integers. However, by carefully defining the system model and the desired properties, the risk of undetected bugs is reduced considerably.

Within DFINITY, we have already successfully applied formal methods in small projects, finding bugs in critical parts of the stack that were missed in manual reviews and tests.

# Open Research Questions

Ideally, we would like to formally verify the entire IC stack. But formal verification is a slow and complex process, requiring expert input. Thus, we propose to start our verification effort by targeting some of the most critical components and mechanisms of the IC, such as:

* The canisters comprising the Network Nervous System (NNS) and the upcoming Service Nervous Systems (SNS)
* The subnet-based sharding mechanism implementation of the interface specification
* The split of replicas into layers (peer-to-peer, consensus, message routing, and execution), including the interface contracts of the layers
* The consensus algorithm and its implementation
* The message routing layer, including the state manager

As part of our research, we will weigh the probability and impact of bugs against the verification effort for each target, and prioritize and limit our efforts accordingly. This ratio will also depend on the verification technique applied, where different techniques might be more suitable for the different targets. The different techniques offer different trade-offs (in particular, the proximity of the system model to the source code versus verification effort), and may include:

* Static analysis, techniques for automatically verifying a fixed set of properties of source code
* Model checking, an automated technique to verify an abstract, simplified model of a target
* Automated test generation, a technique to derive tests for an implementation. This could be guided by an abstract model of the target (model-based testing), or by partial symbolic execution of the target code (concolic testing)
* Automated deductive verification, techniques for proving properties of the code of the target
* Interactive theorem proving, a general technique for mechanizing proofs of mathematical theorems

We will evaluate the state-of-the art techniques and their applicability to our targets. Applying them may require us to develop novel verification methodologies.

# Skills and Expertise

Formal methods expertise in different areas will be needed. The exact areas will depend on the verification tools and techniques we choose to apply, but also the verification targets we choose to pursue (e.g., we may require expertise in code verification, verification of distributed systems, or verification of security protocols). Within DFINITY, the work will largely be done by the members of the Formal Security team.

# Community Involvement

The research questions can be answered in collaboration with experts in academia and elsewhere. Any tooling developed for canister analysis could also be useful by other developers on the Internet Computer, to help analyze their own canisters. For example, a possible outcome of a verification project could be an annotation language to specify properties of canister methods, together with command-line tools for analysis, or even integration with an IDE. The development of such tools would present an opportunity for the community to get involved, helping prioritize the features of the tools and providing user feedback.

## What we are asking the community

* Review comments, ask questions, give feedback

* Vote accept or reject on NNS Motion


Developer forum: https://forum.dfinity.org/t/long-term-r-d-formal-verification-proposal/9397





Long Term R&D: Formal Verification