Introducing pallet-verifier

I am proud to announce the successful completion of the Web3 Foundation grant for developing pallet-verifier - a tool for detecting common security vulnerabilities and insecure patterns in FRAME pallets using static program analysis techniques like data-flow analysis, abstract interpretation and symbolic execution.

Overview

At the highest level, pallet-verifier is a custom Rust compiler (rustc) driver which uses MIRAI as a backend for abstract interpretation (and in the future, also as a tag and taint analysis engine).

Additionally, for a seamless and familiar developer experience, pallet-verifier is distributed as a custom cargo sub-command (i.e. cargo verify-pallet).

Background

FRAME pallets are modules used to build/compose Substrate-based blockchains. They implement the business logic for specific use cases and features (e.g. handling account balances), enabling developers to easily create application-specific Substrate-based blockchain runtime environments from a modular set of components.

Current Capabilities

Currently, pallet-verifier focuses on detecting panics and arithmetic overflow/underflow (including overflow checks for narrowing and/or lossy integer cast/as conversions that aren't checked by the default Rust compiler - see also this and this) in dispatchable functions/extrinsics (and public associated functions of inherent and local trait implementations) of FRAME pallets. However, other classes of security vulnerabilities (e.g. insufficient or missing origin checks, bad randomness, insufficient unsigned transaction validation e.t.c) will also be targeted in the future.

Additionally, unlike linting tools which simply detect problematic syntactic patterns (e.g. clippy, dylint e.t.c), pallet-verifier (using MIRAI) goes beyond this by performing a flow, path and context-sentitive analysis (see also this and this) which evaluates the reachability of problematic code paths/program states before issuing warnings. As a concrete example, pallet-verifier will not issue a warning for the following code block, because the branch condition precludes an arithmetic overflow.

fn bounded_increment(x: u8, bound: u8) -> u8 {
    if x < bound {
        x + 1 // this cannot overflow because `bound <= u8::MAX`
    } else {
        bound
    }
}

Lastly, pallet-verifier assumes a 32 bit target pointer width by default (i.e. the same pointer width as the wasm32 and riscv32 targets), however, this can be overridden using the --pointer-width argument which accepts a value of either 32 or 64 (e.g. cargo verify-pallet --pointer-width 64). The target pointer width is especially relevant for integer cast/as conversions involving pointer-sized integer types (i.e. usize and isize). As a concrete example, the integer cast operation below is safe in 32 bit execution environments but can overflow in 64 bit execution environments

fn convert(val: usize) -> u32 {
    val as u32
}

Architecture

FRAME is a Rust-based DSL (Domain Specific Language), therefore, the source code representation that pallet-verifier analyzes is Rust's MIR (Mid-level Intermediate Representation). This is because MIR is "a radically simplified form of Rust that is [ideal] for certain flow-sensitive [analysis]" (see also this and this).

pallet-verifier consists of two binaries:

• A custom cargo subcommand which is the main user-facing component and is invoked via cargo verify-pallet. It's relatively straightforward, it mostly compiles dependencies using appropriate options and compiler flags, before invoking the custom rustc driver on the target crate (i.e. the FRAME pallet).
• A custom rustc driver which implements the core functionality of pallet-verifier. It's typically invoked by the cargo subcommand.

The custom rustc driver operates in two conceptual phases:

• An entry point generation and invariant annotation phase.
• A verification/abstract interpretation phase.

Entry point generation

"MIRAI is an abstract interpreter for the Rust compiler's mid-level intermediate representation (MIR)", and finding potential panics (abrupt terminations) is one of MIRAI's primary use cases. It does this by performing a path-sensitive analysis, meaning that given an entry point, MIRAI "will analyze all possible code paths that start from that entry point and determine if any of them can reach a program point where an abrupt runtime termination will happen".

However, "[since] it is necessary for MIRAI to resolve and analyze all functions that can be reached from an entry point, it is not possible for a generic or higher order function to serve as an entry point" (see also this and this).

This presents a challenge because FRAME is inherently a generic framework, as it makes extensive use of Rust generic types and traits.

pallet-verifier solves this by automatically generating "tractable" entry points as singular direct calls to dispatchable functions/extrinsics (and public associated functions of inherent and local trait implementations) using concrete types from unit tests as substitutions for generic types, while keeping the call arguments "abstract" (in contrast to unit tests, which use "concrete" call arguments, and may also exercise a single target function multiple times, leading to under-approximation of program semantics and/or inefficient use of resources during abstract interpretation).

Invariant annotations

MIRAI can also detect potential arithmetic overflow/underflow due to arithmetic operations, if either the rustc "overflow-checks" (i.e. -C overflow-checks=true|on|yes|y) or "debug-assertions" (i.e. -C debug-assertions=true|on|yes|y) flag is enabled. This is because rustc automatically adds instructions for dynamic overflow checking when the aforementioned flags are enabled.

However, there's one exception, because dynamic overflow checks are not added (see also) for as conversions (i.e. type cast operations) e.g.

fn convert_with_overflow(val: u16) -> u8 {
    val as u8
}

So pallet-verifier automatically adds annotations to verify that narrowing and/or lossy integer cast/as conversions don't overflow (i.e. integer as conversions where the range of the source type is not a subset of that of the destination type e.g. an as conversion from u16 to u8 or u8 to i8).

Additionally, pallet-verifier also adds annotations for declaring invariants that can't be inferred from source code alone, to improve the accuracy of the verifier and reduce false positives (e.g. iterator invariant annotations).

Lastly, inorder to automatically add annotations to the target FRAME pallet's MIR (e.g. overflow checks for narrowing and/or lossy integer cast/as conversions and iterator invariant annotations), pallet-verifier also typically needs to add the mirai-annotations crate as a dependency of the target crate that it's invoked on. So it detects when the mirai-annotations crate dependency is missing, automatically compiles it (see also) and "non-invasively" adds it as a dependency (i.e. without modifying the "actual" source code and/or Cargo.toml manifest of the target FRAME pallet).

Verification / Abstract Interpretation

After entry point generation, the "tractable" entry points are passed to MIRAI for verification/ abstract interpretation, after which pallet-verifier determines which diagnostics to either "suppress" or "emit" based on our domain-specific knowledge.

pallet-verifier leverages a custom FileLoader to "virtually" add "analysis-only" external crate declarations and module definitions (e.g. extern crate declarations for the mirai-annotations crate, and module definitions for generated "tractable" entry points and additional summaries/foreign contracts) to the target FRAME pallet without modifying its "actual" source code. The "virtual" FileLoader strategically adds our "analysis-only" external crate declarations and module definitions in a way that leverages rustc's excellent support for incremental compilation/analysis (see also this and this), meaning unrelated code is never recompiled during the verification/abstract intepretation phase.

Installation, Usage and Diving Deeper

Check out pallet-verifier's GitHub repository for installation and usage instructions, some additional architectural details, and inline source documentation e.t.c.

Conclusion

pallet-verifier is only at the very beginning of its development, so issues, bug reports, PRs and feature requests are welcome at the GitHub repository 🙂.

Acknowledgements

Special thanks to the Web3 Foundation for funding pallet-verifier's development via a generous grant.