Search Results

Documents authored by Ceresa, Martín

Artifact
Software
DOI: 10.4230/artifacts.23003
Fraud Proof Games

Authors: Martín Ceresa and César Sánchez

Abstract
Cite as

Martín Ceresa, César Sánchez. Fraud Proof Games (Software). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-23003,
   title = {{Fraud Proof Games}}, 
   author = {Ceresa, Mart{\'\i}n and S\'{a}nchez, C\'{e}sar},
   note = {Software, version 1., swhId: \href{https://archive.softwareheritage.org/swh:1:dir:761ba38f606c1b4a0a9e202e6518d092d51ff381;origin=https://gitlab.software.imdea.org/martin.ceresa/leanfpgames;visit=swh:1:snp:fac56d84158cb280cdb40d50d82de3afae8bc491;anchor=swh:1:rev:7d12774f898db347810efdabd41c8a81b867222f}{\texttt{swh:1:dir:761ba38f606c1b4a0a9e202e6518d092d51ff381}} (visited on 2025-05-16)},
   url = {https://gitlab.software.imdea.org/martin.ceresa/leanfpgames},
   doi = {10.4230/artifacts.23003},
}
Document
DOI: 10.4230/OASIcs.FMBC.2025.5
Towards a Mechanization of Fraud Proof Games in Lean

Authors: Martín Ceresa and César Sánchez

Published in: OASIcs, Volume 129, 6th International Workshop on Formal Methods for Blockchains (FMBC 2025)

Abstract
Arbitration games from Referee Delegation of Computations are central to layer two optimistic rollup architectures (L2), one of the most prominent mechanisms for scaling blockchains. L2 blockchains operate on the principle that computations are valid unless proven otherwise. Challenging incorrect computations requires users to construct fraud proofs through a dispute resolution process that involves two opposing players. Fraud proofs are objects that establish when proposed computations are invalid, and they are so computationally small and cheap that can be checked by the underlying trusted blockchain. Arbitration games, this challenging process, involve one player posing strategic questions and another player revealing details about computations. Arbitration games start from the posting of Disputable Assertions (DAs), DAs contain partial information about computations including their result. Since there is no trust between players, hashes are posted as compact witnesses of knowledge. One player provides information decomposing hashes while the other decides which "path" to take navigating the computation trace. When a path is exhausted, all the required information to compute the result from the data provided following the path has been revealed and the path can be proven to be faulty or correct. We explore in this paper the formalization of arbitration games in Lean4, introducing the first machine-checkable strategies that honest players can play guaranteeing success. These strategies ensure: on one side, the successful debunking of dishonest computations via the construction of fraud proofs, while in the other, the successful navigation of the challenge process through correct answers. In short, these are the winning strategies that honest players (on both sides) can follow. We explore in this paper formal abstractions to capture disputable assertions, arbitration games on finite binary trees asserting data-availability and membership, game transformations, and then discuss how to work towards a general formal framework for referee delegation of computations.
Cite as

Martín Ceresa and César Sánchez. Towards a Mechanization of Fraud Proof Games in Lean. In 6th International Workshop on Formal Methods for Blockchains (FMBC 2025). Open Access Series in Informatics (OASIcs), Volume 129, pp. 5:1-5:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{ceresa_et_al:OASIcs.FMBC.2025.5,
  author =	{Ceresa, Mart{\'\i}n and S\'{a}nchez, C\'{e}sar},
  title =	{{Towards a Mechanization of Fraud Proof Games in Lean}},
  booktitle =	{6th International Workshop on Formal Methods for Blockchains (FMBC 2025)},
  pages =	{5:1--5:17},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-371-3},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{129},
  editor =	{Marmsoler, Diego and Xu, Meng},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2025.5},
  URN =		{urn:nbn:de:0030-drops-230327},
  doi =		{10.4230/OASIcs.FMBC.2025.5},
  annote =	{Keywords: blockchain, formal methods, layer-2, optimistic rollups, arbitration games}
}
Document
DOI: 10.4230/OASIcs.FMBC.2022.5
Multi: A Formal Playground for Multi-Smart Contract Interaction

Authors: Martín Ceresa and César Sánchez

Published in: OASIcs, Volume 105, 4th International Workshop on Formal Methods for Blockchains (FMBC 2022)

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.
Cite as

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)

Copy BibTex To Clipboard

@InProceedings{ceresa_et_al:OASIcs.FMBC.2022.5,
  author =	{Ceresa, Mart{\'\i}n and S\'{a}nchez, C\'{e}sar},
  title =	{{Multi: A Formal Playground for Multi-Smart Contract Interaction}},
  booktitle =	{4th International Workshop on Formal Methods for Blockchains (FMBC 2022)},
  pages =	{5:1--5:16},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-250-1},
  ISSN =	{2190-6807},
  year =	{2022},
  volume =	{105},
  editor =	{Dargaye, Zaynah and Schneidewind, Clara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2022.5},
  URN =		{urn:nbn:de:0030-drops-171868},
  doi =		{10.4230/OASIcs.FMBC.2022.5},
  annote =	{Keywords: blockchain, formal methods, theorem prover, smart-contracts}
}
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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