Document Open Access Logo

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

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

PDF
Thumbnail PDF

File

OASIcs.FMBC.2020.4.pdf
  • Filesize: 447 kB
  • 12 pages

Document Identifiers

Author Details

João Santos Reis
  • Release Lab, Nova-Lincs, University of Beira Interior, Portugal
Paul Crocker
  • Release Lab, C4, University of Beira Interior, Portugal
Simão Melo de Sousa
  • Release Lab, C4, Nova-Lincs, University of Beira Interior, Portugal

Funding

This work was supported and funded by the Tezos Foundation by the project FRESCO (Formal Verification of Tezos Smart Contracts).

Cite AsGet BibTex

João Santos Reis, Paul Crocker, and Simão Melo de Sousa. Tezla, an Intermediate Representation for Static Analysis of Michelson Smart Contracts. In 2nd Workshop on Formal Methods for Blockchains (FMBC 2020). Open Access Series in Informatics (OASIcs), Volume 84, pp. 4:1-4:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/OASIcs.FMBC.2020.4

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program analysis
Keywords
  • Intermediate representation
  • Static analysis
  • Tezos blockchain
  • Michelson

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

Supplementary Materials

References

  1. Gabriel Alfour. LIGO. URL: https://ligolang.org/.
  2. Stephen Andrews and Richard Ayotte. Fi - Smart coding for smart contracts. URL: https://fi-code.com/.
  3. Pedro Antonino and A. W. Roscoe. Formalising and verifying smart contracts with Solidifier: A bounded model checker for Solidity. arXiv:2002.02710 [cs], February 2020. URL: http://arxiv.org/abs/2002.02710.
  4. Bruno Bernardo, Raphaël Cauderlier, Zhenlei Hu, Basile Pesin, and Julien Tesson. Mi-Cho-Coq, a framework for certifying Tezos Smart Contracts. In 1st Workshop on Formal Methods for Blockchains, September 2019. URL: http://arxiv.org/abs/1909.08671.
  5. Bruno Bernardo, Raphaël Cauderlier, Basile Pesin, and Julien Tesson. Albert, an intermediate smart-contract language for the Tezos blockchain. In 4th Workshop on Trusted Smart Contracts, January 2020. URL: http://arxiv.org/abs/2001.02630.
  6. Luís Pedro Arrojado da Horta, João Santos Reis, Mário Pereira, and Simão Melo de Sousa. WhylSon: Proving your Michelson Smart Contracts in Why3. arXiv:2005.14650 [cs], May 2020. URL: http://arxiv.org/abs/2005.14650.
  7. DaiLambda. SCaml. URL: https://gitlab.com/dailambda/scaml.
  8. Michael del Castillo. The DAO Attacked: Code Issue Leads to $60 Million Ether Theft, June 2016. URL: https://www.coindesk.com/dao-attacked-code-issue-leads-60-million-ether-theft.
  9. Thomas Durieux, João F. Ferreira, Rui Abreu, and Pedro Cruz. Empirical Review of Automated Analysis Tools on 47,587 Ethereum Smart Contracts. In 42nd International Conference on Software Engineering (ICSE '20), February 2020. URL: https://doi.org/10.1145/3377811.3380364.
  10. Josselin Feist, Gustavo Greico, and Alex Groce. Slither: A static analysis framework for smart contracts. In Proceedings of the 2nd International Workshop on Emerging Trends in Software Engineering for Blockchain, WETSEB '19, pages 8-15, Montreal, Quebec, Canada, May 2019. IEEE Press. URL: https://doi.org/10.1109/wetseb.2019.00008.
  11. L M Goodman. Tezos-a self-amending crypto-ledger White paper. Technical report, Tezos, 2014. Google Scholar
  12. John B. Kam and Jeffrey D. Ullman. Monotone data flow analysis frameworks. Acta Informatica, 7(3):305-317, 1977. URL: https://doi.org/10.1007/BF00290339.
  13. RELEASE Lab. FRESCO - formal verification and static analysis of tezos compliant smart contracts, gitlab. URL: https://gitlab.com/releaselab/fresco.
  14. Nomadic Labs. Michelson Reference. URL: https://michelson.nomadic-labs.com.
  15. Nomadic Labs. Michelson: The language of Smart Contracts in Tezos. URL: http://tezos.gitlab.io/whitedoc/michelson.html.
  16. Francois Maurel and Smart Chain Arena. SmartPy. URL: https://smartpy.io/.
  17. A. Miné, A. Ouadjaout, and M. Journault. Design of a modular platform for static analysis. In Proc. of 9h Workshop on Tools for Automatic Program Analysis (TAPAS'18), Lecture Notes in Computer Science (LNCS), page 4, August 2018. URL: http://www-apr.lip6.fr/~mine/publi/mine-al-tapas18.pdf.
  18. João Reis. Softcheck, a generic and modular data-flow analyser. URL: https://gitlab.com/joaosreis/softcheck.
  19. João Reis. TezCheck Analysis Results - GitLab. URL: https://gitlab.com/releaselab/fresco/tezcheck-results.
  20. B. K. Rosen, M. N. Wegman, and F. K. Zadeck. Global value numbers and redundant computations. In Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL '88, pages 12-27, San Diego, California, United States, 1988. ACM Press. URL: https://doi.org/10.1145/73560.73562.
  21. João Santos Reis. SoftCheck, uma plataforma de construção de análises estáticas para a segurança de programas, genérica e composicional. PhD thesis, University of Beira Interior, Covilhã, Portugal, July 2018. Google Scholar
  22. João Santos Reis. TezCheck - softcheck interface for tezos, gitlab. URL: https://gitlab.com/releaselab/fresco/tezcheck.
  23. Ilya Sergey, Amrit Kumar, and Aquinas Hobor. Scilla: A Smart Contract Intermediate-Level LAnguage. arXiv:1801.00687 [cs], January 2018. URL: http://arxiv.org/abs/1801.00687.
  24. Ilya Sergey, Vaivaswatha Nagaraj, Jacob Johannsen, Amrit Kumar, Anton Trunov, and Ken Chan Guan Hao. Safer smart contract programming with Scilla. Proceedings of the ACM on Programming Languages, 3(OOPSLA):1-30, October 2019. URL: https://doi.org/10.1145/3360611.
  25. Serokell and TQ Group. Lorentz. URL: https://gitlab.com/morley-framework/morley/-/tree/master/code/lorentz.
  26. Nick Szabo. Formalizing and Securing Relationships on Public Networks. First Monday, 2(9), September 1997. URL: https://doi.org/10.5210/fm.v2i9.548.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact