pallet-verifier is 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.
FRAME pallets are modules used to build/compose Substrate-based blockchains.
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).
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).
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
}NOTE: the 64 bit target pointer width option is currently only supported on 64 bit host machines.
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 is implemented via a custom rustc driver callback.
Automatic "tractable" entry point generation is necessary because FRAME is inherently a generic framework,
as it makes extensive use of Rust generic types and traits, however, when performing
verification/abstract interpretation with MIRAI,
"it is not possible for a generic or higher order function to serve as an entry point", because
"it is necessary for MIRAI to resolve and analyze all functions that can be reached from an entry point"
(see also this and this).
So pallet-verifier automatically generates "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).
Annotations are implemented/added by overriding the optimized-mir query using a
custom provider that adds custom MIR passes
(e.g. a pass that finds all integer as conversions that are either narrowing or lossy, and adds overflow checks to them).
Annotations are necessary for either adding checks that aren't included by the default Rust compiler
(e.g. overflow checks for narrowing and/or lossy integer cast/as conversions - see also
this and this), or 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).
NOTE: Annotations require the mirai-annotations crate to be a dependency of the target
FRAME pallet that pallet-verifier is invoked on, however, it's improbable that this will be the case in the wild,
so pallet-verifier 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).
After entry point generation, the "tractable" entry points are passed to MIRAI for verification/ abstract interpretation. This is implemented by another custom rustc driver callback that uses MIRAI as a library, and determines which diagnostics to either "suppress" or "emit" based on our domain-specific knowledge.
NOTE: pallet-verifier leverages a custom FileLoader (see implementation)
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.