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).
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) 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
}
Diving Deeper
Check out the full introductory blog post to learn more about how pallet-verifier works under the hood (see also).
Key highlights include details about:
- Automatic entry point generation which makes analysis with MIRAI tractable and efficient (and reasonably sound), which is a challenge for MIRAI for our use case because FRAME is inherently a generic 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 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/
asconversions), 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).
Installation and Usage
Check out pallet-verifier’s GitHub repository for installation and usage instructions, as well access to the source code (including 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.
