Pallet-verifier updates thread

Tech Talk
,
1

Hello there! :waving_hand:

I’m David Semakula, the creator of 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.

I’ll be using this thread to share regular updates about new feature releases for the project (you can also use this project board for a high-level overview of currently planned features).

But first, some background/history and a re-introduction.

NOTE: You can skip ahead to the first update post if you’ve already read the introductory blog post (and/or the accompanying forum post).

Background

pallet-verifier was created in response to an RFP (Request for Proposal) from the Web3 Foundation and received initial funding from the Web3 Foundation’s technical Grants Program.

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). It’s also distributed as a custom cargo sub-command (i.e. cargo verify-pallet), to facilitate a seamless and familiar developer experience.

One key architectural property of pallet-verifier is that 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) 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
    }
}

Useful Resources

And with that, we’re ready for our first update post below :slightly_smiling_face:!

1 Like
2

Here’s what’s new (or notable) since pallet-verifier’s initial launch announcement:

Improved analysis of pallet storage operations

pallet-verifier now aliases return and closure arg places related to the underlying pallet storage type of FRAME storage operations, and propagates related invariants (e.g. iterator and slice related invariants for underlying collection types) to these places (where appropriate).

This kind of aliasing requires domain specific knowledge because the underlying sp_io::storage::* host function calls for accessing runtime storage are essentially “foreign functions”, so MIRAI can’t alias them automatically.

This aliasing and subsequent invariant propagation (including live-variable and borrowed-variable analyzes before propagation) greatly improves the verifier’s accuracy when analyzing storage operations.

A concrete example where this is useful is a multi-step storage operation, where first a storage value (whose underlying type is a collection) is read and the index of an item is retrieved from the returned collection in one statement, and then the index is used to mutate the collection in a later statement (see the pseudo-code below).

pub type Collection<T: Config> = StorageValue<_, Vec<..>, ValueQuery>;

// ... Define other stuff

pub fn do_whatever(origin: OriginFor<T>) -> DispatchResult {
  // Find index
  let index = Collection::<T>::get().binary_search_by(..)?;
  
  // ... Do stuff that doesn't mutate `Collection`
  
  // Mutate collection
  Collection::<T>::mutate(|c| c.remove(index));
}

Analysis of pallet hooks

pallet-verifier now analyzes all associated functions of local pallet hooks implementations.

By default, for only the integrity_test hook, pallet-verifier ignores panics arising from direct local calls to panicking macros (i.e. panic!, assert!, assert_eq!, unreachable! e.t.c - except the unimplemented! macro which is always reported), and local usages of Option::expect and Result::expect.

However, a CLI arg can apply this exception to a user specified list of hooks (i.e. --allow-hook-panics=<list of hooks>) as some (typically “low-level”) pallets tend to use assertions and panics in hooks to enforce system-wide invariants.

NOTE: Reachable Option::unwrap and Result::unwrap calls are currently always reported with the rationale that intentional panics should at the very least be properly documented (i.e. with an “expect” message).

Analysis of implementations of traits from pallet dependencies

Implementations of traits defined in other pallets included as dependencies are now also analyzed.

Analysis of implementations of traits from frame-support::traits::tokens

Implementations of traits from the frame-support::traits::tokens module (which defines “traits for working with tokens and their associated datastructures”) are now analyzed.

Updated nightly compiler toolchain

pallet-verifier now targets the nightly-2025-01-10 toolchain channel, which is the latest version supported by upstream MIRAI.

This update fixes a few core/std and compiler intrinsics related issues for projects using features from or targeting newer compiler versions.
So if you’ve run into any such issues over the last few weeks, they should now be resolved.

Various improvements to core infrastructure for automatic MIR annotation, entry point generation, and diagnostics filtering

It’s not feasible to enumerate all the improvements since the initial launch announcement, however, a few more notable high-level improvements include:

  • More precise integer cast overflow checks for enum discriminants
  • More robust entry point generation for cases with similarly named in-scope traits from different modules or crates
  • More precise analysis of iterator chains
  • Improved analysis/filtering of overflow warnings rooted in (slice) iterator! macro from core/std
  • Applying automatic iterator and slice MIR annotations to match guards
  • Propagating iterator and slice invariants to Result and Option adaptor input closures

In general, more precise analysis of iterator and loop constructs by automatically generating MIR annotations for iterator/loop invariants is a constant theme for improving pallet-verifier’s precision/accuracy and soundness, because these constructs are one of the most common causes of false positives in the abstract interpreter.

At a higher level, the automatic MIR annotation, entry point generation, and diagnostic filtering infrastructure are the most complex components of pallet-verifier, so they’re constantly undergoing improvements for improved precision/accuracy, soundness and performance.

Upstreaming various contributions to MIRAI

Some notable upstreamed contributions include:

1 Like
3

I do have a similar tool for Xss/Sqli.