blockchain static-analysis abstract-interpretation

Publication: MichelsonLiSA: A Static Analyzer for Tezos

L. Olivieri, T. Jensen, L. Negrini, F. Spoto

2023 IEEE International Conference on Pervasive Computing and Communications Workshops and other Affiliated Events (PerCom Workshops) (BRAIN 2023)
Atlanta, GA, USA, March 13, 2023
Workshop paper

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