Project Roadmap

[ehildenb]

W3F Grants Program: Functional correctness verification of core Substrate modules for Polkadot

Introduction

The W3F is looking for auditors of the PR (Polkadot Runtime), focusing on the subset of Substrate modules used to implement Polkadot: https://medium.com/polkadot-network/apply-to-audit-polkadots-runtime-86c988ced31b.

This includes modules from the Substrate Runtime Module Library (SRML) and some Polkadot specific modules.
The modules are written in Rust, and are compiled to Wasm.
Of particular interest are authorization/code-execution attacks and denial-of-service attacks on the modules themselves (and thus on Substrate and potentially the network).

An audit at the Rust level will focus on high-level security properties of the code, but will not catch any build-time errors introduced or low-level functional correctness bugs. We propose formally verifying the generated Wasm code to guard against these bugs and to provide the security auditors with a complete specification of the behaviors of the generated Wasm. The verification artifacts (K specifications) can be integrated directly into Polkadot’s CI system so that on changes to behavior action must be taken to either fix the code or update the specification.

Deliverables:

• K specifications of one core Substrate runtime module for Polkadot which is <100 lines of Rust.
• Integration of the K specifications into the Polkadot CI system.
• Transfer of knowledge on how to maintain and write K specifications to Polkadot developers.

Milestones:

1. Meet with Polkadot devs to learn about the core Polkadot modules and select one module which (i) is important from a security standpoint due to widespread use, (ii) is largely frozen in its intended behavior, and (iii) is ideally <100 lines of Rust source code. Agree on the behaviors that need to be specified (as semi-formal English spec).
2. Develop the K specification of the selected runtime module, weekly meetings (or more frequently) with Polkadot devs to keep them updated and have them learn how to maintain and write K specifications. Produce documentation describing the specification, including the high-level English specification and arguments that the K specification is a refinement of the English specification.
3. Integrate the developed specifications into the Polkadot CI system. Note that we will setup the CI integration, then we will discuss with the Polkadot devs how it should be enabled. It may be prudent to minimize maintenance overhead by updating the specification less frequently than every PR (instead updating it on a larger release cycle).

[ehildenb]

After discussions about the new proposed verification approach (#20), we have decided to amend milestone (2) to be more fine-grained. This is because instead of using the traditional approach for verification where we manually write specifications at the bytecode level, we are trying to develop a more automated approach where we generate the specifications at the bytecode level and prove that they are bisimilar to an abstract K specification.

Milestone (3) becomes pushed back to Milestone (5), and Milestone (2) gets split into three steps, to reflect our better knowledge of the new process.

1. Meet with Polkadot devs to learn about the core Polkadot modules and select one module which (i) is important from a security standpoint due to widespread use, (ii) is largely frozen in its intended behavior, and (iii) is ideally <100 lines of Rust source code. Agree on the behaviors that need to be specified (as semi-formal English spec).
2. Develop abstract K specifications at the Wasm level of the selected runtime module. These specifications will mimic the Rust data-structures directly as K terms. An example of this for the set_free_balance method can be found here: https://github.com/runtimeverification/polkadot-verification/blob/master/set-free-balance.md. RV will assist in developing the remaining high-level specs, but it's understood that Polkadot devs should take over this process. Call this specification SET-FREE-BALANCE-SPEC.
3. Generate the Wasm execution specifications of the bytecode:
   a. Generate execution traces of the Wasm code using the LLVM backend and a fuzzing frontend. This will produce sequences of rules in the order that they are executed, called SET-FREE-BALANCE-TRACE_i (subscripted by _i for the fact that there are many traces).
   b. Do common subsequence analysis on the SET-FREE-BALANCE-TRACE_i to find common subsequences of rules, and ask the Haskell backend to merge those rules together into rules which take larger steps. Initially we'll look for subsequences of length 2, but the parameter will be tunable. The new merged rules will be loaded back into the definition for either execution or proving.
   c. Regenerate traces using the new definition, and use that to prune out any erroneously added rules from the rule merging process (which may add too many rules).
   d. If the original semantics is KWasm, the new semantics after one iteration of (3.a ; 3.b ; 3.c) will be KWasm(SET-FREE-BALANCE-TRACE)_1, and after j iterations will be KWasm(SET-FREE-BALANCE-TRACE)_j. Call the final one KWasm(SET-FREE-BALANCE), to reflect that this is a partial evaluation of KWasm w.r.t. SET-FREE-BALANCE-TRACE. Iterate until we cannot merge any more rules.
4. Refinement proof from SET-FREE-BALANCE-SPEC to KWasm(SET-FREE-BALANCE). This will use K-EQ to show that the behaviors intended by the SET-FREE-BALANCE-SPEC are actually displayed by KWasm(SET-FREE-BALANCE).
5. Integrate the developed specifications into the Polkadot CI system. Note that we will setup the CI integration, then we will discuss with the Polkadot devs how it should be enabled. It may be prudent to minimize maintenance overhead by updating the specification less frequently than every PR (instead updating it on a larger release cycle).

And finally (optional):

6. Ensure completeness of the generated traces, by showing that KWasm(SET-FREE-BALANCE) covers all the possible behaviors of the actual Wasm code.