Volume
OASIcs, Volume 84
2nd Workshop on Formal Methods for Blockchains (FMBC 2020)
-
Part of:
Series:
Open Access Series in Informatics (OASIcs)
Conference: Workshop on Formal Methods for Blockchains (FMBC)
Publication Details
- published at: 2020-12-11
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-169-6
- DBLP: db/conf/cav/fmbc2020
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 84, FMBC 2020, Complete Volume
Abstract
OASIcs, Volume 84, FMBC 2020, Complete Volume
Cite as
2nd Workshop on Formal Methods for Blockchains (FMBC 2020). Open Access Series in Informatics (OASIcs), Volume 84, pp. 1-136, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@Proceedings{bernardo_et_al:OASIcs.FMBC.2020,
title = {{OASIcs, Volume 84, FMBC 2020, Complete Volume}},
booktitle = {2nd Workshop on Formal Methods for Blockchains (FMBC 2020)},
pages = {1--136},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-169-6},
ISSN = {2190-6807},
year = {2020},
volume = {84},
editor = {Bernardo, Bruno and Marmsoler, Diego},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2020},
URN = {urn:nbn:de:0030-drops-134121},
doi = {10.4230/OASIcs.FMBC.2020},
annote = {Keywords: OASIcs, Volume 84, FMBC 2020, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
2nd Workshop on Formal Methods for Blockchains (FMBC 2020). Open Access Series in Informatics (OASIcs), Volume 84, pp. 0:i-0:xii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{bernardo_et_al:OASIcs.FMBC.2020.0,
author = {Bernardo, Bruno and Marmsoler, Diego},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {2nd Workshop on Formal Methods for Blockchains (FMBC 2020)},
pages = {0:i--0:xii},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-169-6},
ISSN = {2190-6807},
year = {2020},
volume = {84},
editor = {Bernardo, Bruno and Marmsoler, Diego},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2020.0},
URN = {urn:nbn:de:0030-drops-134137},
doi = {10.4230/OASIcs.FMBC.2020.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
Formal Design, Implementation and Verification of Blockchain Languages Using K (Invited Talk)
Abstract
The usual post-mortem approach to formal language semantics and verification, where the language is firstly implemented and used in production for many years before a need for formal semantics and verification tools naturally arises, simply does not work anymore. New blockchain languages or virtual machines are proposed at an alarming rate, followed by new versions of them every few weeks, together with programs (or smart contracts) in these languages that are responsible for financial transactions of potentially significant value. Formal analysis and verification tools are therefore needed immediately for such languages and virtual machines. We will present recent academic and commercial results in developing blockchain languages and virtual machines that come directly equipped with formal analysis and verification tools. The main idea is to generate all these automatically, correct-by-construction from a formal language specification.
Cite as
Grigore Rosu. Formal Design, Implementation and Verification of Blockchain Languages Using K (Invited Talk). In 2nd Workshop on Formal Methods for Blockchains (FMBC 2020). Open Access Series in Informatics (OASIcs), Volume 84, p. 1:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{rosu:OASIcs.FMBC.2020.1,
author = {Rosu, Grigore},
title = {{Formal Design, Implementation and Verification of Blockchain Languages Using K}},
booktitle = {2nd Workshop on Formal Methods for Blockchains (FMBC 2020)},
pages = {1:1--1:1},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-169-6},
ISSN = {2190-6807},
year = {2020},
volume = {84},
editor = {Bernardo, Bruno and Marmsoler, Diego},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2020.1},
URN = {urn:nbn:de:0030-drops-134141},
doi = {10.4230/OASIcs.FMBC.2020.1},
annote = {Keywords: Blockchain, K Framework}
}
Document
Short Paper
Formal Specification and Verification of Solidity Contracts with Events (Short Paper)
Abstract
Events in the Solidity language provide a means of communication between the on-chain services of decentralized applications and the users of those services. Events are commonly used as an abstraction of contract execution that is relevant from the users' perspective. Users must, therefore, be able to understand the meaning and trust the validity of the emitted events. This paper presents a source-level approach for the formal specification and verification of Solidity contracts with the primary focus on events. Our approach allows the specification of events in terms of the on-chain data that they track, and the predicates that define the correspondence between the blockchain state and the abstract view provided by the events. The approach is implemented in solc-verify, a modular verifier for Solidity, and we demonstrate its applicability with various examples.
Cite as
Ákos Hajdu, Dejan Jovanović, and Gabriela Ciocarlie. Formal Specification and Verification of Solidity Contracts with Events (Short Paper). In 2nd Workshop on Formal Methods for Blockchains (FMBC 2020). Open Access Series in Informatics (OASIcs), Volume 84, pp. 2:1-2:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{hajdu_et_al:OASIcs.FMBC.2020.2,
author = {Hajdu, \'{A}kos and Jovanovi\'{c}, Dejan and Ciocarlie, Gabriela},
title = {{Formal Specification and Verification of Solidity Contracts with Events}},
booktitle = {2nd Workshop on Formal Methods for Blockchains (FMBC 2020)},
pages = {2:1--2:9},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-169-6},
ISSN = {2190-6807},
year = {2020},
volume = {84},
editor = {Bernardo, Bruno and Marmsoler, Diego},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2020.2},
URN = {urn:nbn:de:0030-drops-134153},
doi = {10.4230/OASIcs.FMBC.2020.2},
annote = {Keywords: Smart contracts, Solidity, events, specification, verification}
}
Document
Populating the Peephole Optimizer of a Smart Contract Compiler
Abstract
Developing compiler optimizations, especially for new, rapidly evolving smart contract languages, can be onerous and error-prone, but is especially important for smart contracts, where deployment and execution directly translate to monetary cost and which cannot change once deployed. One common optimization technique is the use of peephole optimizations, replacement rules that are applied using pattern-matching. These rules are normally constructed using human expertise, which is both time-consuming and far from systematic in exploring opportunities for optimization. In this work we propose a pipeline to automatically populate the peephole optimizer of a smart contract compiler. We apply superoptimization to an existing code base to obtain sequences of instructions, which can be replaced by cheaper, observationally equivalent instructions. We then generate peephole optimization rules by extracting the underlying patterns of these optimizations. We provide a case study of our approach and a prototype implementation for bytecode of the Ethereum Virtual Machine, the tool ppltr, which combines the superoptimizer ebso and the rule generator sorg. Then we evaluate our approach by generating and applying nearly 1k peephole optimization rules extracted from 2k optimizations obtained from deployed bytecode.
Cite as
Maria A. Schett and Julian Nagele. Populating the Peephole Optimizer of a Smart Contract Compiler. In 2nd Workshop on Formal Methods for Blockchains (FMBC 2020). Open Access Series in Informatics (OASIcs), Volume 84, pp. 3:1-3:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{schett_et_al:OASIcs.FMBC.2020.3,
author = {Schett, Maria A. and Nagele, Julian},
title = {{Populating the Peephole Optimizer of a Smart Contract Compiler}},
booktitle = {2nd Workshop on Formal Methods for Blockchains (FMBC 2020)},
pages = {3:1--3:15},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-169-6},
ISSN = {2190-6807},
year = {2020},
volume = {84},
editor = {Bernardo, Bruno and Marmsoler, Diego},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2020.3},
URN = {urn:nbn:de:0030-drops-134169},
doi = {10.4230/OASIcs.FMBC.2020.3},
annote = {Keywords: Compiler Optimizations, Constraint Solving, Ethereum Bytecode}
}
Document
Tezla, an Intermediate Representation for Static Analysis of Michelson Smart Contracts
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.
Cite as
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)
Copy BibTex To Clipboard
@InProceedings{santosreis_et_al:OASIcs.FMBC.2020.4,
author = {Santos Reis, Jo\~{a}o and Crocker, Paul and Melo de Sousa, Sim\~{a}o},
title = {{Tezla, an Intermediate Representation for Static Analysis of Michelson Smart Contracts}},
booktitle = {2nd Workshop on Formal Methods for Blockchains (FMBC 2020)},
pages = {4:1--4:12},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-169-6},
ISSN = {2190-6807},
year = {2020},
volume = {84},
editor = {Bernardo, Bruno and Marmsoler, Diego},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2020.4},
URN = {urn:nbn:de:0030-drops-134176},
doi = {10.4230/OASIcs.FMBC.2020.4},
annote = {Keywords: Intermediate representation, Static analysis, Tezos blockchain, Michelson}
}
Document
A Blockchain Model in Tamarin and Formal Analysis of Hash Time Lock Contract
Abstract
Formal analysis and verification methods can aid the design and validation of security properties in blockchain based protocols. However, to generate a reasonable and correct verification, a proper model for the blockchain is needed. In this paper, we give a blockchain model in Tamarin. Based on our model we analyze and give a formal verification for the hash time lock contract, an atomic cross chain trading protocol. The result shows that our model is able to identify an underlying assumption for the hash time lock contract and that the model is useful for analyzing blockchain based protocols.
Cite as
Colin Boyd, Kristian Gjøsteen, and Shuang Wu. A Blockchain Model in Tamarin and Formal Analysis of Hash Time Lock Contract. In 2nd Workshop on Formal Methods for Blockchains (FMBC 2020). Open Access Series in Informatics (OASIcs), Volume 84, pp. 5:1-5:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{boyd_et_al:OASIcs.FMBC.2020.5,
author = {Boyd, Colin and Gj{\o}steen, Kristian and Wu, Shuang},
title = {{A Blockchain Model in Tamarin and Formal Analysis of Hash Time Lock Contract}},
booktitle = {2nd Workshop on Formal Methods for Blockchains (FMBC 2020)},
pages = {5:1--5:13},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-169-6},
ISSN = {2190-6807},
year = {2020},
volume = {84},
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.2020.5},
URN = {urn:nbn:de:0030-drops-134187},
doi = {10.4230/OASIcs.FMBC.2020.5},
annote = {Keywords: Blockchain model, Tamarin, Hash time lock contract, Formal verification}
}
Document
Authenticated Data Structures as Functors in Isabelle/HOL
Abstract
Merkle trees are ubiquitous in blockchains and other distributed ledger technologies (DLTs). They guarantee that the involved systems are referring to the same binary tree, even if each of them knows only the cryptographic hash of the root. Inclusion proofs allow knowledgeable systems to share subtrees with other systems and the latter can verify the subtrees' authenticity. Often, blockchains and DLTs use data structures more complicated than binary trees; authenticated data structures generalize Merkle trees to such structures.
We show how to formally define and reason about authenticated data structures, their inclusion proofs, and operations thereon as datatypes in Isabelle/HOL. The construction lives in the symbolic model, i.e., we assume that no hash collisions occur. Our approach is modular and allows us to construct complicated trees from reusable building blocks, which we call Merkle functors. Merkle functors include sums, products, and function spaces and are closed under composition and least fixpoints. As a practical application, we model the hierarchical transactions of Canton, a practical interoperability protocol for distributed ledgers, as authenticated data structures. This is a first step towards formalizing the Canton protocol and verifying its integrity and security guarantees.
Cite as
Andreas Lochbihler and Ognjen Marić. Authenticated Data Structures as Functors in Isabelle/HOL. In 2nd Workshop on Formal Methods for Blockchains (FMBC 2020). Open Access Series in Informatics (OASIcs), Volume 84, pp. 6:1-6:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{lochbihler_et_al:OASIcs.FMBC.2020.6,
author = {Lochbihler, Andreas and Mari\'{c}, Ognjen},
title = {{Authenticated Data Structures as Functors in Isabelle/HOL}},
booktitle = {2nd Workshop on Formal Methods for Blockchains (FMBC 2020)},
pages = {6:1--6:15},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-169-6},
ISSN = {2190-6807},
year = {2020},
volume = {84},
editor = {Bernardo, Bruno and Marmsoler, Diego},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2020.6},
URN = {urn:nbn:de:0030-drops-134196},
doi = {10.4230/OASIcs.FMBC.2020.6},
annote = {Keywords: Merkle tree, functor, distributed ledger, datatypes, higher-order logic}
}
Document
Mechanized Formal Model of Bitcoin’s Blockchain Validation Procedures
Abstract
We present the first mechanized formal model of Bitcoin’s transaction and blockchain data structures including the formalization of the blockchain validation procedures. Our formal model, though still a simplified representation of an actual Bitcoin blockchain, includes regular and coinbase transactions, segregated witnesses, relative and absolute locktime, the Bitcoin Script language expressions together with a denotational semantics, transaction fees and block rewards. We formally specify the details of validity checks performed when adding new blocks to the blockchain. We assume perfect cryptography and use the symbolic approach for modeling hash functions and digital signatures.
To demonstrate the utility of the model, we formally state and prove several essential properties of a valid blockchain - transactions are unique, each coin can be spent at most once and the new value is only created through block rewards. The model and the proofs are largely independent of Bitcoin specific details and easily generalize to any cryptocurrency blockchain based on the Unspent Transaction Output (UTXO) paradigm.
We mechanize all the results using the Coq proof assistant.
Cite as
Kristijan Rupić, Lovro Rožić, and Ante Derek. Mechanized Formal Model of Bitcoin’s Blockchain Validation Procedures. In 2nd Workshop on Formal Methods for Blockchains (FMBC 2020). Open Access Series in Informatics (OASIcs), Volume 84, pp. 7:1-7:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{rupic_et_al:OASIcs.FMBC.2020.7,
author = {Rupi\'{c}, Kristijan and Ro\v{z}i\'{c}, Lovro and Derek, Ante},
title = {{Mechanized Formal Model of Bitcoin’s Blockchain Validation Procedures}},
booktitle = {2nd Workshop on Formal Methods for Blockchains (FMBC 2020)},
pages = {7:1--7:14},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-169-6},
ISSN = {2190-6807},
year = {2020},
volume = {84},
editor = {Bernardo, Bruno and Marmsoler, Diego},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2020.7},
URN = {urn:nbn:de:0030-drops-134209},
doi = {10.4230/OASIcs.FMBC.2020.7},
annote = {Keywords: blockchain, Bitcoin, program verification, Coq}
}
Document
Short Paper
Towards Verifying the Bitcoin-S Library (Short Paper)
Abstract
We try to verify properties of the Bitcoin-S library, a Scala implementation of parts of the Bitcoin protocol. We use the Stainless verifier which supports programs in a fragment of Scala called Pure Scala. Since Bitcoin-S is not written in this fragment, we extract the relevant code from it and rewrite it until we arrive at code that we successfully verify. In that process we find and fix two bugs in Bitcoin-S.
Cite as
Ramon Boss, Kai Brünnler, and Anna Doukmak. Towards Verifying the Bitcoin-S Library (Short Paper). In 2nd Workshop on Formal Methods for Blockchains (FMBC 2020). Open Access Series in Informatics (OASIcs), Volume 84, pp. 8:1-8:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{boss_et_al:OASIcs.FMBC.2020.8,
author = {Boss, Ramon and Br\"{u}nnler, Kai and Doukmak, Anna},
title = {{Towards Verifying the Bitcoin-S Library}},
booktitle = {2nd Workshop on Formal Methods for Blockchains (FMBC 2020)},
pages = {8:1--8:9},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-169-6},
ISSN = {2190-6807},
year = {2020},
volume = {84},
editor = {Bernardo, Bruno and Marmsoler, Diego},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2020.8},
URN = {urn:nbn:de:0030-drops-134212},
doi = {10.4230/OASIcs.FMBC.2020.8},
annote = {Keywords: Bitcoin, Scala, Bitcoin-S, Stainless}
}
Document
On the Formal Verification of the Stellar Consensus Protocol
Abstract
The Stellar Consensus Protocol (SCP) is a quorum-based BFT consensus protocol. However, instead of using threshold-based quorums, SCP is permissionless and its quorum system emerges from participants’ self-declared trust relationships. In this paper, we describe the methodology we deploy to formally verify the safety and liveness of SCP for arbitrary but fixed configurations.
The proof uses a combination of Ivy and Isabelle/HOL. In Ivy, we model SCP in first-order logic, and we verify safety and liveness under eventual synchrony. In Isabelle/HOL, we prove the validity of our first-order encoding with respect to a more direct higher-order model. SCP is currently deployed in the Stellar Network, and we believe this is the first mechanized proof of both safety and liveness, specified in LTL, for a deployed BFT protocol.
Cite as
Giuliano Losa and Mike Dodds. On the Formal Verification of the Stellar Consensus Protocol. In 2nd Workshop on Formal Methods for Blockchains (FMBC 2020). Open Access Series in Informatics (OASIcs), Volume 84, pp. 9:1-9:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{losa_et_al:OASIcs.FMBC.2020.9,
author = {Losa, Giuliano and Dodds, Mike},
title = {{On the Formal Verification of the Stellar Consensus Protocol}},
booktitle = {2nd Workshop on Formal Methods for Blockchains (FMBC 2020)},
pages = {9:1--9:9},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-169-6},
ISSN = {2190-6807},
year = {2020},
volume = {84},
editor = {Bernardo, Bruno and Marmsoler, Diego},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2020.9},
URN = {urn:nbn:de:0030-drops-134226},
doi = {10.4230/OASIcs.FMBC.2020.9},
annote = {Keywords: Consensus, Blockchains, First-Order Logic, Stellar, Ivy Prover, Decidability}
}
Document
Short Paper
Formal Specification and Model Checking of the Tendermint Blockchain Synchronization Protocol (Short Paper)
Abstract
Blockchain synchronization is one of the core protocols of Tendermint blockchains. In this short paper, we discuss our recent efforts in formal specification of the protocol and its implementation, as well as some initial model checking results. We demonstrate that the protocol quality and understanding can be improved by writing specifications and model checking them.
Cite as
Sean Braithwaite, Ethan Buchman, Igor Konnov, Zarko Milosevic, Ilina Stoilkovska, Josef Widder, and Anca Zamfir. Formal Specification and Model Checking of the Tendermint Blockchain Synchronization Protocol (Short Paper). In 2nd Workshop on Formal Methods for Blockchains (FMBC 2020). Open Access Series in Informatics (OASIcs), Volume 84, pp. 10:1-10:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{braithwaite_et_al:OASIcs.FMBC.2020.10,
author = {Braithwaite, Sean and Buchman, Ethan and Konnov, Igor and Milosevic, Zarko and Stoilkovska, Ilina and Widder, Josef and Zamfir, Anca},
title = {{Formal Specification and Model Checking of the Tendermint Blockchain Synchronization Protocol}},
booktitle = {2nd Workshop on Formal Methods for Blockchains (FMBC 2020)},
pages = {10:1--10:8},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-169-6},
ISSN = {2190-6807},
year = {2020},
volume = {84},
editor = {Bernardo, Bruno and Marmsoler, Diego},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2020.10},
URN = {urn:nbn:de:0030-drops-134238},
doi = {10.4230/OASIcs.FMBC.2020.10},
annote = {Keywords: Blockchain, Fault Tolerance, Byzantine Faults, Model Checking}
}
Document
Inter-Blockchain Protocols with the Isabelle Infrastructure Framework
Abstract
The main incentives of blockchain technology are distribution and distributed change, consistency, and consensus. Beyond just being a distributed ledger for digital currency, smart contracts add transaction protocols to blockchains to execute terms of a contract in a blockchain network. Inter-blockchain (IBC) protocols define and control exchanges between different blockchains.
The Isabelle Infrastructure framework {has been designed to} serve security and privacy for IoT architectures by formal specification and stepwise attack analysis and refinement. A major case study of this framework is a distributed health care scenario for data consistency for GDPR compliance. This application led to the development of an abstract system specification of blockchains for IoT infrastructures.
In this paper, we first give a summary of the concept of IBC. We then introduce an instantiation of the Isabelle Infrastructure framework to model blockchains. Based on this we extend this model to instantiate different blockchains and formalize IBC protocols. We prove the concept by defining the generic property of global consistency and prove it in Isabelle.
Cite as
Florian Kammüller and Uwe Nestmann. Inter-Blockchain Protocols with the Isabelle Infrastructure Framework. In 2nd Workshop on Formal Methods for Blockchains (FMBC 2020). Open Access Series in Informatics (OASIcs), Volume 84, pp. 11:1-11:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{kammuller_et_al:OASIcs.FMBC.2020.11,
author = {Kamm\"{u}ller, Florian and Nestmann, Uwe},
title = {{Inter-Blockchain Protocols with the Isabelle Infrastructure Framework}},
booktitle = {2nd Workshop on Formal Methods for Blockchains (FMBC 2020)},
pages = {11:1--11:12},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-169-6},
ISSN = {2190-6807},
year = {2020},
volume = {84},
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.2020.11},
URN = {urn:nbn:de:0030-drops-134249},
doi = {10.4230/OASIcs.FMBC.2020.11},
annote = {Keywords: Blockchain, smart contracts, interactive theorem proving, inter-blockchain protocols}
}