License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.FMBC.2020.4
URN: urn:nbn:de:0030-drops-134176
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/13417/
Go to the corresponding OASIcs Volume Portal

Santos Reis, João ; Crocker, Paul ; Melo de Sousa, Simão

Tezla, an Intermediate Representation for Static Analysis of Michelson Smart Contracts

pdf-format:
OASIcs-FMBC-2020-4.pdf (0.4 MB)

Abstract

This paper introduces Tezla, an intermediate representation of Michelson smart contracts that eases the design of static smart contract analysers. This intermediate representation uses a store and aims to preserve the semantics, flow and resource usage of the original smart contract. This enables properties like gas consumption to be statically verified. We provide an automated decompiler of Michelson smart contracts to Tezla. In order to support our claim about the adequacy of Tezla, we develop a static analyser that takes advantage of the Tezla representation of Michelson smart contracts to prove simple but non-trivial properties.

BibTeX - Entry

@InProceedings{santosreis_et_al:OASIcs:2020:13417,
  author =	{Jo{\~a}o Santos Reis and Paul Crocker and Sim{\~a}o Melo de Sousa},
  title =	{{Tezla, an Intermediate Representation for Static Analysis of Michelson Smart Contracts}},
  booktitle =	{2nd Workshop on Formal Methods for Blockchains (FMBC 2020)},
  pages =	{4:1--4:12},
  series =	{OpenAccess Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-169-6},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{84},
  editor =	{Bruno Bernardo and Diego Marmsoler},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/13417},
  URN =		{urn:nbn:de:0030-drops-134176},
  doi =		{10.4230/OASIcs.FMBC.2020.4},
  annote =	{Keywords: Intermediate representation, Static analysis, Tezos blockchain, Michelson}
}

Keywords: Intermediate representation, Static analysis, Tezos blockchain, Michelson
Collection: 2nd Workshop on Formal Methods for Blockchains (FMBC 2020)
Issue Date: 2020
Date of publication: 11.12.2020
Supplementary Material: Source code of the implementation available at: https://gitlab.com/releaselab/fresco/tezla

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI