« Home

blockchain  static-analysis  abstract-interpretation

MichelsonLiSA: A Static Analyzer for Tezos

Authors: Luca Olivieri, Thomas Jensen, Luca Negrini, Fausto Spoto
2023 IEEE International Conference on Pervasive Computing and Communications Workshops and other Affiliated Events (PerCom Workshops) (BRAIN 2023)

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.

Manuscript:	PDF
Associated project:	LiSA
Conference page:	Link
IEEE page:	Link