Document Open Access Logo

Multi: A Formal Playground for Multi-Smart Contract Interaction

Authors Martín Ceresa , César Sánchez

PDF
Thumbnail PDF

File

OASIcs.FMBC.2022.5.pdf
  • Filesize: 0.61 MB
  • 16 pages

Document Identifiers

Author Details

Martín Ceresa
  • IMDEA Software Institute, Madrid, Spain
César Sánchez
  • IMDEA Software Institute, Madrid, Spain

Funding

This work was funded in part by the Madrid Regional Government under project "S2018/TCS-4339 (BLOQUES-CM)‘’ and by a research grant from Nomadic Labs and the Tezos Foundation.

Cite AsGet BibTex

Martín Ceresa and César Sánchez. Multi: A Formal Playground for Multi-Smart Contract Interaction. In 4th International Workshop on Formal Methods for Blockchains (FMBC 2022). Open Access Series in Informatics (OASIcs), Volume 105, pp. 5:1-5:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/OASIcs.FMBC.2022.5

Abstract

Blockchains are maintained by a network of participants, miner nodes, that run algorithms designed to maintain collectively a distributed machine tolerant to Byzantine attacks. From the point of view of users, blockchains provide the illusion of centralized computers that perform trustable verifiable computations, where all computations are deterministic and the results cannot be manipulated or undone. Every blockchain is equipped with a crypto-currency. Programs running on blockchains are called smart-contracts and are written in a special-purpose programming language with deterministic semantics. Each transaction begins with an invocation from an external user to a smart contract. Smart contracts have local storage and can call other contracts, and more importantly, they store, send and receive cryptocurrency. Once installed in a blockchain, the code of the smart-contract cannot be modified. Therefore, it is very important to guarantee that contracts are correct before deployment. However, the resulting ecosystem makes it very difficult to reason about program correctness, since smart-contracts can be executed by malicious users or malicious smart-contracts can be designed to exploit other contracts that call them. Many attacks and bugs are caused by unexpected interactions between multiple contracts, the attacked contract and unknown code that performs the exploit. Moreover, there is a very aggressive competition between different blockchains to expand their user base. Ideas are implemented fast and blockchains compete to offer and adopt new features quickly. In this paper, we propose a formal playground that allows reasoning about multi-contract interactions and is extensible to incorporate new features, study their behaviour and ultimately prove properties before features are incorporated into the real blockchain. We implemented a model of computation that models the execution platform, abstracts the internal code of each individual contract and focuses on contract interactions. Even though our Coq implementation is still a work in progress, we show how many features, existing or proposed, can be used to reason about multi-contract interactions.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program reasoning
  • Theory of computation → Program constructs
  • Theory of computation → Abstract machines
Keywords
  • blockchain
  • formal methods
  • theorem prover
  • smart-contracts

Metrics

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

Related Versions

References

  1. Victor Allombert, Mathias Bourgoin, and Julien Tesson. Introduction to the tezos blockchain, 2019. URL: https://doi.org/10.48550/ARXIV.1909.08458.
  2. Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. Alternating-time temporal logic. J. ACM, 49(5):672-713, September 2002. URL: https://doi.org/10.1145/585265.585270.
  3. Danil Annenkov, Jakob Botsch Nielsen, and Bas Spitters. Concert: a smart contract certification framework in coq. Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, January 2020. URL: https://doi.org/10.1145/3372885.3373829.
  4. Bruno Bernardo, Raphaël Cauderlier, Zhenlei Hu, Basile Pesin, and Julien Tesson. Mi-cho-coq, a framework for certifying tezos smart contracts. CoRR, abs/1909.08671, 2019. URL: http://arxiv.org/abs/1909.08671.
  5. Tezos Blockchain. Tezos agora: Florence, no ba (psflorena), 2021-12-24. URL: https://agora.tezos.com/period/46.
  6. Margarita Capretto, Martin Ceresa, and Cesar Sanchez. Transaction monitoring of smart contracts, 2022. URL: https://doi.org/10.48550/ARXIV.2207.02517.
  7. Alberto Cuesta Cañada, Fiona Kobayashi, fubuloubu, and Austin Williams. Eip-3156: Flash loans. URL: https://eips.ethereum.org/EIPS/eip-3156.
  8. Joshua Ellul, Jonathan Galea, Max Ganado, Stephen Mccarthy, and Gordon J. Pace. Regulating blockchain, dlt and smart contracts: a technology regulator’s perspective. ERA Forum, 21(2):209-220, October 2020. URL: https://doi.org/10.1007/s12027-020-00617-7.
  9. Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv, and Yoni Zohar. Online detection of effectively callback free objects with applications to smart contracts. Proc. ACM Program. Lang., 2(POPL), December 2017. URL: https://doi.org/10.1145/3158136.
  10. Ligo. Ligo: A friendly smart contract language for tezos, 2022. URL: https://ligolang.org/.
  11. Jakob Botsch Nielsen and Bas Spitters. Smart contract interactions in coq. In FM Workshops (1), volume 12232 of Lecture Notes in Computer Science, pages 380-391. Springer, 2019. Google Scholar
  12. Zoe Paraskevopoulou, Cătălin HriŢcu, Maxime Dénès, Leonidas Lampropoulos, and Benjamin C. Pierce. Foundational property-based testing. In Christian Urban and Xingyuan Zhang, editors, Interactive Theorem Proving, pages 325-343, Cham, 2015. Springer International Publishing. Google Scholar
  13. Anton Permenev, Dimitar Dimitrov, Petar Tsankov, Dana Drachsler-Cohen, and Martin Vechev. Verx: Safety verification of smart contracts. In 2020 IEEE Symposium on Security and Privacy (SP), pages 1661-1677, 2020. URL: https://doi.org/10.1109/SP40000.2020.00024.
  14. Daian Phil. Analysis of the dao exploit, 2016. URL: https://hackingdistributed.com/2016/06/18/analysis-of-the-dao-exploit/.
  15. Dan Robinson and Georgios Konstantopoulos. Ethereum is a dark forest, 2020. URL: https://www.paradigm.xyz/2020/08/ethereum-is-a-dark-forest.
  16. Ilya Sergey, Amrit Kumar, and Aquinas Hobor. Scilla: a smart contract intermediate-level language, 2018. URL: https://doi.org/10.48550/ARXIV.1801.00687.
  17. Ilya Sergey, Amrit Kumar, and Aquinas Hobor. Temporal properties of smart contracts. In Tiziana Margaria and Bernhard Steffen, editors, Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice, pages 323-338, Cham, 2018. Springer International Publishing. Google Scholar
  18. Jon Stephens, Kostas Ferles, Benjamin Mariano, Shuvendu Lahiri, and Isil Dillig. Smartpulse: Automated checking of temporal properties in smart contracts. In 42nd IEEE Symposium on Security and Privacy. IEEE, May 2021. URL: https://www.microsoft.com/en-us/research/publication/smartpulse-automated-checking-of-temporal-properties-in-smart-contracts/.
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