Volume
OASIcs, Volume 105
4th International Workshop on Formal Methods for Blockchains (FMBC 2022)
-
Part of:
Series:
Open Access Series in Informatics (OASIcs)
Conference: Workshop on Formal Methods for Blockchains (FMBC)
Event
FMBC 2022, August 11, 2022, Haifa, IsraelEditors
Publication Details
- published at: 2022-10-06
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-250-1
- DBLP: db/conf/cav/fmbc2022
Access Numbers
- Detailed Access Statistics available here
-
Total Document Accesses (updated on a weekly basis):
0PDF Downloads
Documents
No documents found matching your filter selection.
Document
Complete Volume
OASIcs, Volume 105, FMBC 2022, Complete Volume
Abstract
OASIcs, Volume 105, FMBC 2022, Complete Volume
Cite as
4th International Workshop on Formal Methods for Blockchains (FMBC 2022). Open Access Series in Informatics (OASIcs), Volume 105, pp. 1-74, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@Proceedings{dargaye_et_al:OASIcs.FMBC.2022,
title = {{OASIcs, Volume 105, FMBC 2022, Complete Volume}},
booktitle = {4th International Workshop on Formal Methods for Blockchains (FMBC 2022)},
pages = {1--74},
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-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2022},
URN = {urn:nbn:de:0030-drops-171802},
doi = {10.4230/OASIcs.FMBC.2022},
annote = {Keywords: OASIcs, Volume 105, FMBC 2022, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
4th International Workshop on Formal Methods for Blockchains (FMBC 2022). Open Access Series in Informatics (OASIcs), Volume 105, pp. 0:i-0:xii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{dargaye_et_al:OASIcs.FMBC.2022.0,
author = {Dargaye, Zaynah and Schneidewind, Clara},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {4th International Workshop on Formal Methods for Blockchains (FMBC 2022)},
pages = {0:i--0:xii},
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-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2022.0},
URN = {urn:nbn:de:0030-drops-171813},
doi = {10.4230/OASIcs.FMBC.2022.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
MEV-Freedom, in DeFi and Beyond (Invited Talk)
Abstract
Maximal Extractable Value (MEV) refers to a class of recent attacks on public blockchains, where adversaries with the power to reorder, drop or insert transactions in a block can "extract" value from user transactions in the mempool. Empirical research has shown that mainstream DeFi protocols, like e.g. Automated Market Makers and Lending Pools, are massively targeted by MEV attacks. This has detrimental effects on their users, on transaction fees, and on the congestion of blockchain networks. Despite the growing knowledge on MEV attacks on blockchain protocols, an exact definition is still missing. Indeed, formally defining these attacks is an essential prerequisite to the design of provably secure, MEV-free blockchain protocols. In this talk, we propose a formal definition of MEV, based on a general, abstract model of blockchains and smart contracts. We then introduce MEV-freedom, a property enjoyed by contracts resistant to MEV attacks. We validate this notion by rigorously proving that Automated Market Makers and Lending Pools are not MEV-free. We finally discuss how to design MEV-free contracts.
Cite as
Massimo Bartoletti. MEV-Freedom, in DeFi and Beyond (Invited Talk). In 4th International Workshop on Formal Methods for Blockchains (FMBC 2022). Open Access Series in Informatics (OASIcs), Volume 105, p. 1:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{bartoletti:OASIcs.FMBC.2022.1,
author = {Bartoletti, Massimo},
title = {{MEV-Freedom, in DeFi and Beyond}},
booktitle = {4th International Workshop on Formal Methods for Blockchains (FMBC 2022)},
pages = {1:1--1:1},
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-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2022.1},
URN = {urn:nbn:de:0030-drops-171827},
doi = {10.4230/OASIcs.FMBC.2022.1},
annote = {Keywords: Blockchain, Smart Contracts, Formal Security Notion}
}
Document
Finding Smart Contract Vulnerabilities with ConCert’s Property-Based Testing Framework
Abstract
We provide three detailed case studies of vulnerabilities in smart contracts, and show how property based testing would have found them: 1. the Dexter1 token exchange; 2. the iToken; 3. the ICO of Brave’s BAT token. The last example is, in fact, new, and was missed in the auditing process.
We have implemented this testing in ConCert, a general executable model/specification of smart contract execution in the Coq proof assistant. ConCert contracts can be used to generate verified smart contracts in Tezos' LIGO and Concordium’s rust language. We thus show the effectiveness of combining formal verification and property-based testing of smart contracts.
Cite as
Mikkel Milo, Eske Hoy Nielsen, Danil Annenkov, and Bas Spitters. Finding Smart Contract Vulnerabilities with ConCert’s Property-Based Testing Framework. In 4th International Workshop on Formal Methods for Blockchains (FMBC 2022). Open Access Series in Informatics (OASIcs), Volume 105, pp. 2:1-2:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{milo_et_al:OASIcs.FMBC.2022.2,
author = {Milo, Mikkel and Nielsen, Eske Hoy and Annenkov, Danil and Spitters, Bas},
title = {{Finding Smart Contract Vulnerabilities with ConCert’s Property-Based Testing Framework}},
booktitle = {4th International Workshop on Formal Methods for Blockchains (FMBC 2022)},
pages = {2:1--2:13},
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-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2022.2},
URN = {urn:nbn:de:0030-drops-171834},
doi = {10.4230/OASIcs.FMBC.2022.2},
annote = {Keywords: Smart Contracts, Formal Verification, Property-Based Testing, Coq}
}
Document
Automatic Generation of Attacker Contracts in Solidity
Abstract
Smart contracts on the Ethereum blockchain continue to suffer from well-published problems. A particular example is the well-known smart contract reentrancy vulnerability, which continues to be exploited. In this article, we present preliminary work on a method which, given a smart contract that may be vulnerable to such a reentrancy attack, proceeds to attempt to automatically derive an "attacker" contract which can be used to successfully attack the vulnerable contract. The method uses property-based testing to generate, semi-randomly, large numbers of potential attacker contracts, and then proceeds to check whether any of them is a successful attacker. The method is illustrated using a case study where an attack is derived for a vulnerable contract.
Cite as
Ignacio Ballesteros, Clara Benac-Earle, Luis Eduardo Bueso de Barrio, Lars-Åke Fredlund, Ángel Herranz, and Julio Mariño. Automatic Generation of Attacker Contracts in Solidity. In 4th International Workshop on Formal Methods for Blockchains (FMBC 2022). Open Access Series in Informatics (OASIcs), Volume 105, pp. 3:1-3:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{ballesteros_et_al:OASIcs.FMBC.2022.3,
author = {Ballesteros, Ignacio and Benac-Earle, Clara and de Barrio, Luis Eduardo Bueso and Fredlund, Lars-\r{A}ke and Herranz, \'{A}ngel and Mari\~{n}o, Julio},
title = {{Automatic Generation of Attacker Contracts in Solidity}},
booktitle = {4th International Workshop on Formal Methods for Blockchains (FMBC 2022)},
pages = {3:1--3:14},
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-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2022.3},
URN = {urn:nbn:de:0030-drops-171840},
doi = {10.4230/OASIcs.FMBC.2022.3},
annote = {Keywords: Property-Based Testing, Smart Contracts, Reentrancy Attack}
}
Document
Proofgold: Blockchain for Formal Methods
Abstract
Proofgold is a peer to peer cryptocurrency making use of formal logic. Users can publish theories and then develop a theory by publishing documents with definitions, conjectures and proofs. The blockchain records the theories and their state of development (e.g., which theorems have been proven and when). Two of the main theories are a form of classical set theory (for formalizing mathematics) and an intuitionistic theory of higher-order abstract syntax (for reasoning about syntax with binders). We have also significantly modified the open source Proofgold Core client software to create a faster, more stable and more efficient client, Proofgold Lava. Two important changes are the cryptography code and the database code, and we discuss these improvements. We also discuss how the Proofgold network can be used to support large formalization efforts.
Cite as
Chad E. Brown, Cezary Kaliszyk, Thibault Gauthier, and Josef Urban. Proofgold: Blockchain for Formal Methods. In 4th International Workshop on Formal Methods for Blockchains (FMBC 2022). Open Access Series in Informatics (OASIcs), Volume 105, pp. 4:1-4:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{brown_et_al:OASIcs.FMBC.2022.4,
author = {Brown, Chad E. and Kaliszyk, Cezary and Gauthier, Thibault and Urban, Josef},
title = {{Proofgold: Blockchain for Formal Methods}},
booktitle = {4th International Workshop on Formal Methods for Blockchains (FMBC 2022)},
pages = {4:1--4:15},
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-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2022.4},
URN = {urn:nbn:de:0030-drops-171851},
doi = {10.4230/OASIcs.FMBC.2022.4},
annote = {Keywords: Formal logic, Blockchain, Proofgold}
}
Document
Multi: A Formal Playground for Multi-Smart Contract Interaction
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-dev.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}
}