Volume
OASIcs, Volume 95
3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)
-
Part of:
Series:
Open Access Series in Informatics (OASIcs)
Conference: Workshop on Formal Methods for Blockchains (FMBC)
Publication Details
- published at: 2021-11-30
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-209-9
- DBLP: db/conf/cav/fmbc2021
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 95, FMBC 2021, Complete Volume
Abstract
OASIcs, Volume 95, FMBC 2021, Complete Volume
Cite as
3rd International Workshop on Formal Methods for Blockchains (FMBC 2021). Open Access Series in Informatics (OASIcs), Volume 95, pp. 1-68, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@Proceedings{bernardo_et_al:OASIcs.FMBC.2021,
title = {{OASIcs, Volume 95, FMBC 2021, Complete Volume}},
booktitle = {3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)},
pages = {1--68},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-209-9},
ISSN = {2190-6807},
year = {2021},
volume = {95},
editor = {Bernardo, Bruno and Marmsoler, Diego},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2021},
URN = {urn:nbn:de:0030-drops-154239},
doi = {10.4230/OASIcs.FMBC.2021},
annote = {Keywords: OASIcs, Volume 95, FMBC 2021, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
3rd International Workshop on Formal Methods for Blockchains (FMBC 2021). Open Access Series in Informatics (OASIcs), Volume 95, pp. 0:i-0:xii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{bernardo_et_al:OASIcs.FMBC.2021.0,
author = {Bernardo, Bruno and Marmsoler, Diego},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)},
pages = {0:i--0:xii},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-209-9},
ISSN = {2190-6807},
year = {2021},
volume = {95},
editor = {Bernardo, Bruno and Marmsoler, Diego},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2021.0},
URN = {urn:nbn:de:0030-drops-154246},
doi = {10.4230/OASIcs.FMBC.2021.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Towards Verified Price Oracles for Decentralized Exchange Protocols
Abstract
Various smart contracts have been designed and deployed on blockchain platforms to enable cryptocurrency trading, leading to an ever expanding user base of decentralized exchange platforms (DEXs). Automated Market Maker contracts enable token exchange without the need of third party book-keeping. These contracts also serve as price oracles for other contracts, by using a mathematical formula to calculate token exchange rates based on token reserves. However, the price oracle mechanism is vulnerable to attacks both from programming errors and from mistakes in the financial model, and so far their complexity makes it difficult to formally verify them. We present a verified AMM contract and validate its financial model by proving a theorem about a lower bound on the cost of manipulation of the token prices to the attacker. The contract is implemented using the DeepSEA system, which ensures that the theorem applies to the actual EVM bytecode of the contract. This theorem could be used as proof of correctness for other contracts using the AMM, so this is a step towards a verified DeFi landscape.
Cite as
Kinnari Dave, Vilhelm Sjöberg, and Xinyuan Sun. Towards Verified Price Oracles for Decentralized Exchange Protocols. In 3rd International Workshop on Formal Methods for Blockchains (FMBC 2021). Open Access Series in Informatics (OASIcs), Volume 95, pp. 1:1-1:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{dave_et_al:OASIcs.FMBC.2021.1,
author = {Dave, Kinnari and Sj\"{o}berg, Vilhelm and Sun, Xinyuan},
title = {{Towards Verified Price Oracles for Decentralized Exchange Protocols}},
booktitle = {3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)},
pages = {1:1--1:14},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-209-9},
ISSN = {2190-6807},
year = {2021},
volume = {95},
editor = {Bernardo, Bruno and Marmsoler, Diego},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2021.1},
URN = {urn:nbn:de:0030-drops-154254},
doi = {10.4230/OASIcs.FMBC.2021.1},
annote = {Keywords: Smart Contract Verification, Interactive Theorem Proving, Blockchain, Decentralized Finance}
}
Document
Money Grows on (Proof-)Trees: The Formal FA1.2 Ledger Standard
Abstract
Once you have invented digital money, you may need a ledger to track who owns what - along with an interface to that ledger so that users of your money can transact. On the Tezos blockchain this implies: a smart contract (distributed program), storing in its state a ledger to map owner addresses to token quantities; along with standardised entrypoints to query and transact on accounts.
A bank does a similar job - it maps account numbers to account quantities and permits users to transact - but in return the bank demands trust, it incurs expense to maintain a centralised server and staff, it uses a proprietary interface ... and it may speculate using your money and/or display rent-seeking behaviour. A blockchain ledger is by design decentralised, inexpensive, open, and it won't just decide to bet your tokens on risky derivatives (unless you want it to).
The FA1.2 standard is an open standard for ledger-keeping smart contracts on the Tezos blockchain. Several FA1.2 implementations already exist.
Or do they? Is the standard sensible and complete? Are the implementations correct? And what are they implementations of? The FA1.2 standard is written in English, a specification language favoured by wet human brains but notorious for its incompleteness and ambiguity when rendered into dry and unforgiving code.
In this paper we report on a formalisation of the FA1.2 standard as a Coq specification, and on a formal verification of three FA1.2-compliant smart contracts with respect to that specification. Errors were found and ambiguities were resolved; but also, there now exists a mathematically precise and battle-tested specification of the FA1.2 ledger standard.
We will describe FA1.2 itself, outline the structure of the Coq theories - which in itself captures some non-trivial and novel design decisions of the development - and review the detailed verification of the implementations.
Cite as
Murdoch J. Gabbay, Arvid Jakobsson, and Kristina Sojakova. Money Grows on (Proof-)Trees: The Formal FA1.2 Ledger Standard. In 3rd International Workshop on Formal Methods for Blockchains (FMBC 2021). Open Access Series in Informatics (OASIcs), Volume 95, pp. 2:1-2:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{gabbay_et_al:OASIcs.FMBC.2021.2,
author = {Gabbay, Murdoch J. and Jakobsson, Arvid and Sojakova, Kristina},
title = {{Money Grows on (Proof-)Trees: The Formal FA1.2 Ledger Standard}},
booktitle = {3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)},
pages = {2:1--2:14},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-209-9},
ISSN = {2190-6807},
year = {2021},
volume = {95},
editor = {Bernardo, Bruno and Marmsoler, Diego},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2021.2},
URN = {urn:nbn:de:0030-drops-154267},
doi = {10.4230/OASIcs.FMBC.2021.2},
annote = {Keywords: Distributed ledger, smart contracts, Coq, formal verification, blockchain}
}
Document
Short Paper
Using Coq to Enforce the Checks-Effects-Interactions Pattern in DeepSEA Smart Contracts (Short Paper)
Abstract
Using the DeepSEA system for smart contract proofs, this paper investigates how to use the Coq theorem prover to enforce that smart contracts follow the Checks-Effects-Interactions Pattern. This pattern is widely understood to mitigate the risks associated with reentrancy. The infamous "The DAO" exploit is an example of the risks of not following the Checks-Effects-Interactions Pattern. It resulted in the loss of over 50 million USD and involved reentrancy - the exploit used would not have been possible if the Checks-Effects-Interactions Pattern had been followed.
Remix IDE, for example, already has a tool to check that the Checks-Effects-Interactions Pattern has been followed as part of the Solidity Static Analysis module which is available as a plugin. However, aside from simply replicating the Remix IDE feature, implementing a Checks-Effects-Interactions Pattern checker in the proof assistant Coq also allows us to use the proofs, which are generated in the process, in other proofs related to the smart contract.
As an example of this, we will demonstrate an idea for how the modelling of Ether transfer can be simplified by using automatically generated proofs of the property that each smart contract function will call the Ether transfer method at most once (excluding any calls related to invoking other smart contracts). This property is a consequence of following a strict version of the Checks-Effects-Interactions Pattern as given in this paper.
Cite as
Daniel Britten, Vilhelm Sjöberg, and Steve Reeves. Using Coq to Enforce the Checks-Effects-Interactions Pattern in DeepSEA Smart Contracts (Short Paper). In 3rd International Workshop on Formal Methods for Blockchains (FMBC 2021). Open Access Series in Informatics (OASIcs), Volume 95, pp. 3:1-3:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{britten_et_al:OASIcs.FMBC.2021.3,
author = {Britten, Daniel and Sj\"{o}berg, Vilhelm and Reeves, Steve},
title = {{Using Coq to Enforce the Checks-Effects-Interactions Pattern in DeepSEA Smart Contracts}},
booktitle = {3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)},
pages = {3:1--3:8},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-209-9},
ISSN = {2190-6807},
year = {2021},
volume = {95},
editor = {Bernardo, Bruno and Marmsoler, Diego},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2021.3},
URN = {urn:nbn:de:0030-drops-154272},
doi = {10.4230/OASIcs.FMBC.2021.3},
annote = {Keywords: smart contracts, formal methods, blockchain}
}
Document
Short Paper
Formally Documenting Tenderbake (Short Paper)
Abstract
In this paper, we propose a formal documentation of Tenderbake, the new Tezos consensus algorithm, slated to replace the current Emmy family algorithms. The algorithm is broken down to its essentials and represented as an automaton. The automaton models the various aspects of the algorithm: (i) the individual participant, referred to as a baker, (ii) how bakers communicate over the network (the mempool) and (iii) the overall network the bakers operate in. We also present a TLA+ implementation, which has proven to be useful for reasoning about this automaton and refining our documentation. The main goal of this work is to serve as a formal foundation for extracting intricate test scenarios and verifying invariants that Tenderbake’s implementation should satisfy.
Cite as
Sylvain Conchon, Alexandrina Korneva, Çagdas Bozman, Mohamed Iguernlala, and Alain Mebsout. Formally Documenting Tenderbake (Short Paper). In 3rd International Workshop on Formal Methods for Blockchains (FMBC 2021). Open Access Series in Informatics (OASIcs), Volume 95, pp. 4:1-4:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{conchon_et_al:OASIcs.FMBC.2021.4,
author = {Conchon, Sylvain and Korneva, Alexandrina and Bozman, \c{C}agdas and Iguernlala, Mohamed and Mebsout, Alain},
title = {{Formally Documenting Tenderbake}},
booktitle = {3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)},
pages = {4:1--4:9},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-209-9},
ISSN = {2190-6807},
year = {2021},
volume = {95},
editor = {Bernardo, Bruno and Marmsoler, Diego},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2021.4},
URN = {urn:nbn:de:0030-drops-154281},
doi = {10.4230/OASIcs.FMBC.2021.4},
annote = {Keywords: Consensus algorithm, Tezos blockchain, TLA+}
}
Document
Short Paper
Towards Contract Modules for the Tezos Blockchain (Short Paper)
Abstract
Programmatic interaction with a blockchain is often clumsy. Many interfaces handle only loosely structured data, often in JSON format, that is inconvenient to handle and offers few guarantees.
Contract modules provide a statically checked interface to interact with contracts on the Tezos blockchain. A module specification provides all types as well as information about potential failure conditions of the contract. The specification is checked against the contract implementation using symbolic execution. An OCaml module is generated that contains a function for each entry point of the contract. The types of these functions fully describe the interface including the failure conditions and guarantee type-safe and sometimes fail-safe invocation of the contract on the blockchain.
Cite as
Thi Thu Ha Doan and Peter Thiemann. Towards Contract Modules for the Tezos Blockchain (Short Paper). In 3rd International Workshop on Formal Methods for Blockchains (FMBC 2021). Open Access Series in Informatics (OASIcs), Volume 95, pp. 5:1-5:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{doan_et_al:OASIcs.FMBC.2021.5,
author = {Doan, Thi Thu Ha and Thiemann, Peter},
title = {{Towards Contract Modules for the Tezos Blockchain}},
booktitle = {3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)},
pages = {5:1--5:9},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-209-9},
ISSN = {2190-6807},
year = {2021},
volume = {95},
editor = {Bernardo, Bruno and Marmsoler, Diego},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2021.5},
URN = {urn:nbn:de:0030-drops-154294},
doi = {10.4230/OASIcs.FMBC.2021.5},
annote = {Keywords: contract API, modules, static checking}
}