Abstract interpretation of Michelson smart-contracts

TL;DR

This paper introduces a static analysis tool for Michelson smart-contracts using Abstract Interpretation, capable of proving absence of runtime errors and inferring invariants, addressing the challenges posed by blockchain-specific execution models.

Contribution

The work presents a novel static analyzer for Michelson smart-contracts based on Abstract Interpretation, supporting complex features and extending to security property verification.

Findings

Proves absence of runtime errors in Michelson contracts.

Infers invariants on persistent storage over multiple calls.

Supports analysis of external contract calls.

Abstract

Static analysis of smart-contracts is becoming more widespread on blockchain platforms. Analyzers rely on techniques like symbolic execution or model checking, but few of them can provide strong soundness properties and guarantee the analysis termination at the same time. As smart-contracts often manipulate economic assets, proving numerical properties beyond the absence of runtime errors is also desirable. Smart-contract execution models differ considerably from mainstream programming languages and vary from one blockchain to another, making state-of-the-art analyses hard to adapt. For instance, smart-contract calls may modify a persistent storage impacting subsequent calls. This makes it difficult for tools to infer invariants required to formally ensure the absence of exploitable vulnerabilities. The Michelson smart-contract language, used in the Tezos blockchain, is strongly typed, stack-based, and has a strict execution model leaving few opportunities for implicit runtime errors. We present a work in progress static analyzer for Michelson based on Abstract Interpretation and implemented within MOPSA, a modular static analyzer. Our tool supports the Michelson semantic features, including inner calls to external contracts. It can prove the absence of runtime errors and infer invariants on the persistent storage over an unbounded number of calls. It is also being extended to prove high-level numerical and security properties. CCS Concepts: $\bullet$ Security and privacy $\rightarrow$ Logic and verification; $\bullet$ Software and its engineering $\rightarrow$ Automated static analysis.