MichelsonLiSA: A Static Analyzer for Tezos

Abstract

Smart contracts are immutable code deployed in a blockchain, whose execution modifies its global state. Code im-mutability leads to immutable bugs. To prevent such bugs, static program analysis infers information about the behavior of the code, statically, before code execution and deployment. This paper introduces MichelsonLiSA, a static analyzer based on abstract interpretation for the verification of smart contracts written in the Michelson low-level language of the Tezos blockchain. It applies MichelsonLiSA to the identification of security issues arising from cross-contract invocations.