# Pallet-verifier updates thread

**URL:** <https://forum.polkadot.network/t/pallet-verifier-updates-thread/12634>\
**Category:** Tech Talk\
**Tags:** frame, security\
**Created:** [April 23, 2025, 1:53pm UTC](https://forum.polkadot.network/t/pallet-verifier-updates-thread/12634 "2025-04-23T13:53:49Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![davidsemakula](https://dub1.discourse-cdn.com/flex005/user_avatar/forum.polkadot.network/davidsemakula/32/2360_2.png) [@davidsemakula](https://forum.polkadot.network/u/davidsemakula)\
**Post date:** [April 23, 2025, 1:53pm UTC](https://forum.polkadot.network/t/pallet-verifier-updates-thread/12634/1 "2025-04-23T13:53:49Z")

</div>

Hello there! 👋

I’m [David Semakula](https://github.com/davidsemakula), the creator of [pallet-verifier](https://github.com/davidsemakula/pallet-verifier).

[pallet-verifier](https://github.com/davidsemakula/pallet-verifier) is a tool for detecting [common security vulnerabilities](https://secure-contracts.com/not-so-smart-contracts/substrate/) and insecure patterns in [FRAME pallets](https://docs.substrate.io/learn/runtime-development/#frame) using [static program analysis](https://en.wikipedia.org/wiki/Static_program_analysis) techniques like [data-flow analysis](https://en.wikipedia.org/wiki/Data-flow_analysis), [abstract interpretation](https://en.wikipedia.org/wiki/Abstract_interpretation) and [symbolic execution](https://en.wikipedia.org/wiki/Symbolic_execution).

I’ll be using this thread to share regular updates about new feature releases for the project (you can use [this project board](https://github.com/users/davidsemakula/projects/3/views/1) 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](https://davidsemakula.com/blog/introducing-pallet-verifier) (and/or the accompanying [forum post](https://forum.polkadot.network/t/introducing-pallet-verifier-a-tool-for-detecting-common-security-vulnerabilities-and-insecure-patterns-in-frame-pallets/11138)).

## Background

`pallet-verifier` was created in response to an [RFP (Request for Proposal)](https://grants.web3.foundation/docs/RFPs/Static-Analysis-for-Runtime-Pallets) from the [Web3 Foundation](https://web3.foundation) and received initial funding from the [Web3 Foundation’s technical Grants Program](https://medium.com/web3foundation/web3-foundation-grants-wave-21-recipients-cb84921761fd).

## Overview

At the highest level, `pallet-verifier` is a custom [Rust compiler (rustc) driver](https://rustc-dev-guide.rust-lang.org/rustc-driver/intro.html) which uses [MIRAI](https://github.com/endorlabs/MIRAI) as a backend for [abstract interpretation](https://github.com/endorlabs/MIRAI/blob/main/documentation/Overview.md#abstract-interpretation) (and in the future, also as a [tag and taint analysis](https://github.com/endorlabs/MIRAI/blob/main/documentation/TagAnalysis.md) engine). It’s also distributed as a [custom cargo sub-command](https://doc.rust-lang.org/cargo/reference/external-tools.html#custom-subcommands) (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](https://en.wikipedia.org/wiki/Lint_(software)) which simply detect problematic [syntactic](https://en.wikipedia.org/wiki/Syntax_(programming_languages)) patterns (e.g. [clippy](https://github.com/rust-lang/rust-clippy), [dylint](https://github.com/trailofbits/dylint) e.t.c), `pallet-verifier` (using [MIRAI](https://github.com/endorlabs/MIRAI)) goes beyond this by performing a [flow, path and context-sentitive](https://en.wikipedia.org/wiki/Data-flow_analysis#Sensitivities) analysis ([see also](https://github.com/endorlabs/MIRAI/blob/main/documentation/Overview.md#abstract-interpretation)) which evaluates the [reachability](https://en.wikipedia.org/wiki/Reachability_problem) 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.

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

```

## Useful Resources

- Check out `pallet-verifier`’s [GitHub repository](https://github.com/davidsemakula/pallet-verifier) for [installation](https://github.com/davidsemakula/pallet-verifier/blob/master/README.md#installation) and [usage](https://github.com/davidsemakula/pallet-verifier/blob/master/README.md#usage) instructions, as well access to the source code (including detailed inline source documentation) e.t.c.
- Visit the [GitHub project board](https://github.com/users/davidsemakula/projects/3/views/1) for a high-level overview of currently planned features, and/or [create an issue](https://github.com/davidsemakula/pallet-verifier/issues) to report bugs or make feature requests/proposals (PRs are also welcome 🙂).
- Dive into the [full introductory blog post](https://davidsemakula.com/blog/introducing-pallet-verifier) (and/or the accompanying [forum post](https://forum.polkadot.network/t/introducing-pallet-verifier-a-tool-for-detecting-common-security-vulnerabilities-and-insecure-patterns-in-frame-pallets/11138)) to learn more about `pallet-verifier`’s [launch capabilities](https://davidsemakula.com/blog/introducing-pallet-verifier#current-capabilities) and [architecture](https://davidsemakula.com/blog/introducing-pallet-verifier#architecture) ([see also](https://github.com/davidsemakula/pallet-verifier/blob/master/ARCHITECTURE.md)). Key highlights include details about:
  - Automatic [entry point generation](https://davidsemakula.com/blog/introducing-pallet-verifier#entry-point-generation) which makes analysis with [MIRAI](https://github.com/endorlabs/MIRAI) tractable and efficient (and reasonably sound), which is a [challenge for MIRAI for our use case](https://github.com/endorlabs/MIRAI/blob/main/documentation/Overview.md#entry-points) because [FRAME](https://docs.substrate.io/learn/runtime-development/#frame) is inherently a [generic](https://doc.rust-lang.org/book/ch10-00-generics.html) framework, while unit tests as entry points for abstract interpretation suffer from under-approximation of program semantics and/or inefficient use of resources.
  - Automatic [invariant annotation](https://davidsemakula.com/blog/introducing-pallet-verifier#invariant-annotations) infrastructure 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](https://github.com/davidsemakula/pallet-verifier/blob/master/src/providers/passes/int_cast_overflow.rs)), or [declaring invariants](https://crates.io/crates/mirai-annotations) 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](https://github.com/davidsemakula/pallet-verifier/blob/master/src/providers/passes/iterator_invariants.rs)).

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

---

<div class="post-metadata">

**Author:** ![davidsemakula](https://dub1.discourse-cdn.com/flex005/user_avatar/forum.polkadot.network/davidsemakula/32/2360_2.png) [@davidsemakula](https://forum.polkadot.network/u/davidsemakula)\
**Post date:** [April 23, 2025, 1:56pm UTC](https://forum.polkadot.network/t/pallet-verifier-updates-thread/12634/2 "2025-04-23T13:56:07Z")

</div>

Here’s what’s new (or notable) since pallet-verifier’s [initial launch announcement](https://davidsemakula.com/blog/introducing-pallet-verifier):

## Improved analysis of pallet storage operations

`pallet-verifier` now [aliases](https://en.wikipedia.org/wiki/Aliasing_(computing)) 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::*`](https://docs.rs/sp-io/latest/sp_io/storage/index.html) host function calls for accessing runtime storage are essentially [“foreign functions”](https://github.com/endorlabs/MIRAI/blob/main/documentation/Overview.md#foreign-functions), so MIRAI can’t alias them automatically.

This aliasing and subsequent invariant propagation (including [live-variable and borrowed-variable analyzes](https://en.wikipedia.org/wiki/Live-variable_analysis) 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).

```rust
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](https://docs.rs/frame-support/latest/frame_support/traits/trait.Hooks.html).

By default, for only the [`integrity_test` hook](https://docs.rs/frame-support/latest/frame_support/traits/trait.Hooks.html#method.integrity_test), `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](https://docs.rs/frame-support/latest/frame_support/traits/tokens/index.html) (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](https://github.com/endorlabs/MIRAI/pulls?q=is%3Apr+author%3Adavidsemakula) to [MIRAI](https://github.com/endorlabs/MIRAI)

Some notable upstreamed contributions include:

- [Fixing a memory leak that lead to OOM (Out of Memory) issues](https://github.com/endorlabs/MIRAI/pull/11) which initially made MIRAI almost impossible to use for our use case.
  - One notable outcome of this fix is that quite a few pallets whose analysis previously caused OOM issues on a 32 GB RAM machine can now be analyzed with a memory limit as low as 512 MB (with 1 GB being sufficient typically).

- [Fixing issues related to generic args specialization for unevaluated MIR constants](https://github.com/endorlabs/MIRAI/pull/13) which previously caused panics in the abstract interpreter.
- [Implementing more robust logic for resolution of compiler (rustc) and abstract interpreter (MIRAI) intrinsics](https://github.com/endorlabs/MIRAI/pull/27) which previously caused panics in the abstract interpreter.

---

<div class="post-metadata">

**Author:** ![hacxx](https://avatars.discourse-cdn.com/v4/letter/h/a88e4f/32.png) [@hacxx](https://forum.polkadot.network/u/hacxx)\
**Post date:** [April 23, 2025, 10:00pm UTC](https://forum.polkadot.network/t/pallet-verifier-updates-thread/12634/3 "2025-04-23T22:00:39Z")

</div>

I do have a similar tool for Xss/Sqli.