Design and Implementation of Static Analyses for Tezos Smart Contracts
Authors: Luca Olivieri, Luca Negrini, Vincenzo Arceri, Thomas Jensen, Fausto SpotoJanuary 11, 2024
Journal paper
Abstract
Once deployed in blockchain, smart contracts become immutable: attackers can exploit bugs and vulnerabilities in their code, that cannot be replaced with a bug-free version. For this reason, the verification of smart contracts before they are deployed in blockchain is important. However, the development of verification tools is not easy, especially if one wants to obtain guarantees by using formal methods. This paper describes the development, from scratch, of a static analyzer based on abstract interpretation for the verification of real-world Tezos smart contracts. The analyzer is generic with respect to the property under analysis. This paper shows taint analysis as a concrete instantiation of the analyzer, at different levels of precision, to detect untrusted cross-contract invocations.