Volume
OASIcs, Volume 118
5th International Workshop on Formal Methods for Blockchains (FMBC 2024)
-
Part of:
Series:
Open Access Series in Informatics (OASIcs)
Conference: Workshop on Formal Methods for Blockchains (FMBC)
Event
FMBC 2024, April 7, 2024, Luxembourg City, LuxembourgEditors
Publication Details
- published at: 2024-05-21
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-317-1
- DBLP: db/conf/cav/fmbc2024
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 118, FMBC 2024, Complete Volume
Abstract
OASIcs, Volume 118, FMBC 2024, Complete Volume
Cite as
5th International Workshop on Formal Methods for Blockchains (FMBC 2024). Open Access Series in Informatics (OASIcs), Volume 118, pp. 1-164, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@Proceedings{bernardo_et_al:OASIcs.FMBC.2024,
title = {{OASIcs, Volume 118, FMBC 2024, Complete Volume}},
booktitle = {5th International Workshop on Formal Methods for Blockchains (FMBC 2024)},
pages = {1--164},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-317-1},
ISSN = {2190-6807},
year = {2024},
volume = {118},
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.2024},
URN = {urn:nbn:de:0030-drops-198642},
doi = {10.4230/OASIcs.FMBC.2024},
annote = {Keywords: OASIcs, Volume 118, FMBC 2024, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
5th International Workshop on Formal Methods for Blockchains (FMBC 2024). Open Access Series in Informatics (OASIcs), Volume 118, pp. 0:i-0:xii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{bernardo_et_al:OASIcs.FMBC.2024.0,
author = {Bernardo, Bruno and Marmsoler, Diego},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {5th International Workshop on Formal Methods for Blockchains (FMBC 2024)},
pages = {0:i--0:xii},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-317-1},
ISSN = {2190-6807},
year = {2024},
volume = {118},
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.2024.0},
URN = {urn:nbn:de:0030-drops-198659},
doi = {10.4230/OASIcs.FMBC.2024.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
Deductive Verification of Smart Contracts (Invited Talk)
Abstract
At the core of the Ethereum network is the Ethereum Virtual Machine (EVM) which can execute programs written in EVM bytecode. This remarkable feature empowers users to define complex business logic that can be executed programmatically by programs called smart contracts. Smart contracts are programs and may contain bugs. There are several examples of smart contract vulnerabilities that have been exploited in the past: in 2016, a re-entrance vulnerability in the Decentralised Autonomous Organisation (DAO) smart contract was exploited to steal more than USD50 Million. The total value netted from DeFi hacks in 2023 is estimated to be more than $1.5 billion. In this talk I will discuss formal verification of smart contracts. The main technique is deductive verification supported by the verification-friendly language Dafny. I will show how we can use deductive verification to reason about smart contracts, from high-level specifications (Dafny), to intermediate representation (Yul) and finally low-level EVM bytecode.
Cite as
Franck Cassez. Deductive Verification of Smart Contracts (Invited Talk). In 5th International Workshop on Formal Methods for Blockchains (FMBC 2024). Open Access Series in Informatics (OASIcs), Volume 118, p. 1:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{cassez:OASIcs.FMBC.2024.1,
author = {Cassez, Franck},
title = {{Deductive Verification of Smart Contracts}},
booktitle = {5th International Workshop on Formal Methods for Blockchains (FMBC 2024)},
pages = {1:1--1:1},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-317-1},
ISSN = {2190-6807},
year = {2024},
volume = {118},
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.2024.1},
URN = {urn:nbn:de:0030-drops-198664},
doi = {10.4230/OASIcs.FMBC.2024.1},
annote = {Keywords: Smart Contracts, Deductive Verification}
}
Document
Formal Specification of the Cardano Blockchain Ledger, Mechanized in Agda
Abstract
Blockchain systems comprise critical software that handle substantial monetary funds, rendering them excellent candidates for formal verification. One of their core components is the underlying ledger that does all the accounting: keeping track of transactions and their validity, etc.
Unfortunately, previous theoretical studies are typically confined to an idealized setting, while specifications for real implementations are scarce; either the functionality is directly implemented without a proper specification, or at best an informal specification is written on paper.
The present work expands beyond prior meta-theoretical investigations of the EUTxO model to encompass the full scale of the Cardano blockchain: our formal specification describes a hierarchy of modular transitions that covers all the intricacies of a realistic blockchain, such as fully expressive smart contracts and decentralized governance.
It is mechanized in a proof assistant, thus enjoys a higher standard of rigor: type-checking prevents minor oversights that were frequent in previous informal approaches; key meta-theoretical properties can now be formally proven; it is an executable specification against which the implementation in production is being tested for conformance; and it provides firm foundations for smart contract verification.
Apart from a safety net to keep us in check, the formalization also provides a guideline for the ledger design: one informs the other in a symbiotic way, especially in the case of state-of-the-art features like decentralized governance, which is an emerging sub-field of blockchain research that however mandates a more exploratory approach.
All the results presented in this paper have been mechanized in the Agda proof assistant and are publicly available. In fact, this document is itself a literate Agda script and all rendered code has been successfully type-checked.
Cite as
Andre Knispel, Orestis Melkonian, James Chapman, Alasdair Hill, Joosep Jääger, William DeMeo, and Ulf Norell. Formal Specification of the Cardano Blockchain Ledger, Mechanized in Agda. In 5th International Workshop on Formal Methods for Blockchains (FMBC 2024). Open Access Series in Informatics (OASIcs), Volume 118, pp. 2:1-2:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{knispel_et_al:OASIcs.FMBC.2024.2,
author = {Knispel, Andre and Melkonian, Orestis and Chapman, James and Hill, Alasdair and J\"{a}\"{a}ger, Joosep and DeMeo, William and Norell, Ulf},
title = {{Formal Specification of the Cardano Blockchain Ledger, Mechanized in Agda}},
booktitle = {5th International Workshop on Formal Methods for Blockchains (FMBC 2024)},
pages = {2:1--2:18},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-317-1},
ISSN = {2190-6807},
year = {2024},
volume = {118},
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.2024.2},
URN = {urn:nbn:de:0030-drops-198673},
doi = {10.4230/OASIcs.FMBC.2024.2},
annote = {Keywords: blockchain, distributed ledgers, UTxO, Cardano, formal verification, Agda}
}
Document
Formally Verifying the Safety of Pipelined Moonshot Consensus Protocol
Abstract
Decentralized Finance (DeFi) has emerged as a contemporary competitive as well as complementary to traditional centralized finance systems. As of 23rd January 2024, per Defillama approximately USD 55 billion is the total value locked on the DeFi applications on all blockchains put together.
A Byzantine Fault Tolerant (BFT) State Machine Replication (SMR) protocol, popularly known as the consensus protocol, is the central component of a blockchain. If forks are possible in a consensus protocol, they can be misused to carry out double spending attacks and can be catastrophic given high volumes of finance that are transacted on blockchains. Formal verification of the safety of consensus protocols is the golden standard for guaranteeing that forks are not possible. However, it is considered complex and challenging to do. This is reflected by the fact that not many complex consensus protocols are formally verified except for Tendermint and QBFT.
We focus on Supra’s Pipelined Moonshot consensus protocol. Similar to Tendermint’s formal verification, we too model Pipelined Moonshot using IVy and formally prove that for all network sizes, as long as the number of Byzantine validators is less than 1/3, the protocol does not allow forks, thus proving that Pipelined Moonshot is safe and double spending cannot be done using forks. The IVy model and proof of safety is available on y. https://github.com/Entropy-Foundation/suprabft-fv/tree/master/suprabft.
Cite as
M. Praveen, Raghavendra Ramesh, and Isaac Doidge. Formally Verifying the Safety of Pipelined Moonshot Consensus Protocol. In 5th International Workshop on Formal Methods for Blockchains (FMBC 2024). Open Access Series in Informatics (OASIcs), Volume 118, pp. 3:1-3:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{praveen_et_al:OASIcs.FMBC.2024.3,
author = {Praveen, M. and Ramesh, Raghavendra and Doidge, Isaac},
title = {{Formally Verifying the Safety of Pipelined Moonshot Consensus Protocol}},
booktitle = {5th International Workshop on Formal Methods for Blockchains (FMBC 2024)},
pages = {3:1--3:16},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-317-1},
ISSN = {2190-6807},
year = {2024},
volume = {118},
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.2024.3},
URN = {urn:nbn:de:0030-drops-198688},
doi = {10.4230/OASIcs.FMBC.2024.3},
annote = {Keywords: Blockchain consensus, Safety, Formal verification}
}
Document
Towards Mechanised Consensus in Isabelle
Abstract
A blockchain acts as a universal ledger for digital transactions between two parties that require no moderation from a third party. Such transactions are cheaper, quicker, and more secure with high traceability and transparency, with the decentralised structure of a blockchain network allowing for greater scalability and availability. For these reasons, blockchain is at the forefront of emerging technologies, with a wide variety of industries investing billions into the technology. A blockchains consensus protocol is what allows a blockchain network to be decentralised but can be subject to malicious behaviour and faults in its design and implementation that can lead to catastrophic effects like the DAO hack that resulted in a loss of $60 million. From this it is clear to see that the verifications of these protocols are paramount to ensure the safe use of blockchain. In this research, we formally verify the Proof-of-Work consensus protocol, used by Bitcoin, in Isabelle/HOL by modelling the blockchain as the longest branch in a binary tree and proving that the common prefix property holds with the assumption that the network is in majority honest. In this paper, we discuss the validity of our approach, key functions and lemmas we used to complete the proof, advantages and drawbacks of the model, related work and how this research can be taken further.
Cite as
Elliot Jones and Diego Marmsoler. Towards Mechanised Consensus in Isabelle. In 5th International Workshop on Formal Methods for Blockchains (FMBC 2024). Open Access Series in Informatics (OASIcs), Volume 118, pp. 4:1-4:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{jones_et_al:OASIcs.FMBC.2024.4,
author = {Jones, Elliot and Marmsoler, Diego},
title = {{Towards Mechanised Consensus in Isabelle}},
booktitle = {5th International Workshop on Formal Methods for Blockchains (FMBC 2024)},
pages = {4:1--4:22},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-317-1},
ISSN = {2190-6807},
year = {2024},
volume = {118},
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.2024.4},
URN = {urn:nbn:de:0030-drops-198692},
doi = {10.4230/OASIcs.FMBC.2024.4},
annote = {Keywords: Formal Methods, Blockchain, Isabelle/HOL, Consensus, Verification, Theorem Provers}
}
Document
Formalizing Automated Market Makers in the Lean 4 Theorem Prover
Abstract
Automated Market Makers (AMMs) are an integral component of the decentralized finance (DeFi) ecosystem, as they allow users to exchange crypto-assets without the need for trusted authorities or external price oracles. Although these protocols are based on relatively simple mechanisms, e.g. to algorithmically determine the exchange rate between crypto-assets, they give rise to complex economic behaviours. This complexity is witnessed by the proliferation of models that study their structural and economic properties. Currently, most of theoretical results obtained on these models are supported by pen-and-paper proofs. This work proposes a formalization of constant-product AMMs in the Lean 4 Theorem Prover. To demonstrate the utility of our model, we provide mechanized proofs of key economic properties like arbitrage, that at the best of our knowledge have only been proved by pen-and-paper before.
Cite as
Daniele Pusceddu and Massimo Bartoletti. Formalizing Automated Market Makers in the Lean 4 Theorem Prover. In 5th International Workshop on Formal Methods for Blockchains (FMBC 2024). Open Access Series in Informatics (OASIcs), Volume 118, pp. 5:1-5:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{pusceddu_et_al:OASIcs.FMBC.2024.5,
author = {Pusceddu, Daniele and Bartoletti, Massimo},
title = {{Formalizing Automated Market Makers in the Lean 4 Theorem Prover}},
booktitle = {5th International Workshop on Formal Methods for Blockchains (FMBC 2024)},
pages = {5:1--5:13},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-317-1},
ISSN = {2190-6807},
year = {2024},
volume = {118},
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.2024.5},
URN = {urn:nbn:de:0030-drops-198702},
doi = {10.4230/OASIcs.FMBC.2024.5},
annote = {Keywords: Smart contracts, Ethereum, Verification, Blockchain}
}
Document
Towards Benchmarking of Solidity Verification Tools
Abstract
Formal verification of smart contracts has become a hot topic in academic and industrial research, given the growing value of assets managed by decentralized applications and the consequent incentive for adversaries to tamper with them. Most of the current research on the verification of contracts revolves around Solidity, the main high-level language supported by Ethereum and other leading blockchains. Although bug detection tools for Solidity have been proliferating almost since the inception of Ethereum, only in the last few years we have seen verification tools capable of proving that a contract respects some desirable properties. An open issue is how to evaluate and compare the effectiveness of these tools: indeed, the existing benchmarks for general-purpose programming languages cannot be adapted to Solidity, given substantial differences in the programming model and in the desirable properties. We address this problem by proposing an open benchmark for Solidity verification tools. By exploiting our benchmark, we compare two leading tools, SolCMC and Certora, discussing their completeness, soundness and expressiveness limitations.
Cite as
Massimo Bartoletti, Fabio Fioravanti, Giulia Matricardi, Roberto Pettinau, and Franco Sainas. Towards Benchmarking of Solidity Verification Tools. In 5th International Workshop on Formal Methods for Blockchains (FMBC 2024). Open Access Series in Informatics (OASIcs), Volume 118, pp. 6:1-6:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{bartoletti_et_al:OASIcs.FMBC.2024.6,
author = {Bartoletti, Massimo and Fioravanti, Fabio and Matricardi, Giulia and Pettinau, Roberto and Sainas, Franco},
title = {{Towards Benchmarking of Solidity Verification Tools}},
booktitle = {5th International Workshop on Formal Methods for Blockchains (FMBC 2024)},
pages = {6:1--6:15},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-317-1},
ISSN = {2190-6807},
year = {2024},
volume = {118},
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.2024.6},
URN = {urn:nbn:de:0030-drops-198719},
doi = {10.4230/OASIcs.FMBC.2024.6},
annote = {Keywords: Smart contracts, Ethereum, Verification, Blockchain}
}
Document
Towards Formally Specifying and Verifying Smart Contract Upgrades in Coq
Abstract
Smart contract upgrades are costly from a verification perspective and can be a meaningful source of vulnerabilities when done incorrectly. Unfortunately, there is no established, formal framework through which one can reason about contracts as they undergo upgrades, though much work has been done to verify standalone smart contracts. Instead, one must repeat the full verification process for each contract upgrade, something which relies heavily on fallible intuition, can lead to unexpected vulnerabilities, and drives up the cost of formally verifying smart contracts. We propose a formal framework for contract upgrades in ConCert, a Coq-based smart contract verification tool. Central to this framework is our notion of a contract morphism, a theoretical tool which we introduce to formally encode structural relationships between smart contracts, and with which we can formally specify and verify an upgraded contract relative to its previous versions. We argue that ours is a natural framework for specifying and verifying contract upgrades, and hope to offer a first step towards rigorous, efficient specification and verification of contract upgrades.
Cite as
Derek Sorensen. Towards Formally Specifying and Verifying Smart Contract Upgrades in Coq. In 5th International Workshop on Formal Methods for Blockchains (FMBC 2024). Open Access Series in Informatics (OASIcs), Volume 118, pp. 7:1-7:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{sorensen:OASIcs.FMBC.2024.7,
author = {Sorensen, Derek},
title = {{Towards Formally Specifying and Verifying Smart Contract Upgrades in Coq}},
booktitle = {5th International Workshop on Formal Methods for Blockchains (FMBC 2024)},
pages = {7:1--7:14},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-317-1},
ISSN = {2190-6807},
year = {2024},
volume = {118},
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.2024.7},
URN = {urn:nbn:de:0030-drops-198728},
doi = {10.4230/OASIcs.FMBC.2024.7},
annote = {Keywords: smart contract verification, formal methods, interactive theorem prover, smart contract upgrades}
}
Document
A Practical Notion of Liveness in Smart Contract Applications
Abstract
Smart contracts are programs which manage resources in blockchain networks in an automated fashion. In this context, liveness properties are often essential: If I transfer money to a contract, will I eventually get it back?
This kind of property can be hard to specify and verify, in particular because application-specific fairness assumptions w.r.t. function invocation and the behavior of other parties are usually necessary for any liveness proof to succeed. In this work, we analyze smart contract liveness properties discussed in the literature. We find that the smart contract paradigm of decentralization and trustlessness implies that "real" liveness properties do not usually occur. The properties that have been classified as liveness can be more aptly described as enabledness, i.e., the ability of an agent to induce a state change, such as a transfer of resources.
Our contribution in this work is a specification language based on LTL to capture this kind of property. It features some special constructs to describe common properties in smart contracts, such as transfers or ownership of cryptocurrency. We show how often-used examples of liveness properties can be succinctly specified in our language. Moreover, we show how our notion of liveness can simplify formal verification compared to existing approaches.
Cite as
Jonas Schiffl and Bernhard Beckert. A Practical Notion of Liveness in Smart Contract Applications. In 5th International Workshop on Formal Methods for Blockchains (FMBC 2024). Open Access Series in Informatics (OASIcs), Volume 118, pp. 8:1-8:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{schiffl_et_al:OASIcs.FMBC.2024.8,
author = {Schiffl, Jonas and Beckert, Bernhard},
title = {{A Practical Notion of Liveness in Smart Contract Applications}},
booktitle = {5th International Workshop on Formal Methods for Blockchains (FMBC 2024)},
pages = {8:1--8:13},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-317-1},
ISSN = {2190-6807},
year = {2024},
volume = {118},
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.2024.8},
URN = {urn:nbn:de:0030-drops-198732},
doi = {10.4230/OASIcs.FMBC.2024.8},
annote = {Keywords: Smart Contracts, Formal Verification, Security, Safety and Liveness}
}
Document
Securing Aptos Framework with Formal Verification
Abstract
The Aptos Framework is a collection of smart contracts written in the Move language that define standard and common on-chain actions for the Aptos Network. As the security and safety of the Aptos Framework is of utmost importance, it has continuously undergone rigorous testing and comprehensive auditing. To further increase the level of assurance, we have formally verified its security and correctness. This involves identifying critical security requirements for each module, creating formal specifications, and subsequently verifying them using the Move Prover. To the best of our knowledge, this represents one of the first instances of formal verification being applied on such a large scale in a smart contract framework. This paper discusses how this rigorous effort ensures a high level of quality assurance for the Aptos Framework.
Cite as
Junkil Park, Teng Zhang, Wolfgang Grieskamp, Meng Xu, Gerardo Di Giacomo, Kundu Chen, Yi Lu, and Robert Chen. Securing Aptos Framework with Formal Verification. In 5th International Workshop on Formal Methods for Blockchains (FMBC 2024). Open Access Series in Informatics (OASIcs), Volume 118, pp. 9:1-9:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{park_et_al:OASIcs.FMBC.2024.9,
author = {Park, Junkil and Zhang, Teng and Grieskamp, Wolfgang and Xu, Meng and Di Giacomo, Gerardo and Chen, Kundu and Lu, Yi and Chen, Robert},
title = {{Securing Aptos Framework with Formal Verification}},
booktitle = {5th International Workshop on Formal Methods for Blockchains (FMBC 2024)},
pages = {9:1--9:16},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-317-1},
ISSN = {2190-6807},
year = {2024},
volume = {118},
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.2024.9},
URN = {urn:nbn:de:0030-drops-198741},
doi = {10.4230/OASIcs.FMBC.2024.9},
annote = {Keywords: Formal verification, Smart contracts, Aptos Network, The Move language, The Move Prover}
}
Document
Structured Contracts in the EUTxO Ledger Model
Abstract
Blockchain ledgers based on the extended UTxO model support fully expressive smart contracts to specify permissions for performing certain actions, such as spending transaction outputs or minting assets. There have been some attempts to standardize the implementation of stateful programs using this infrastructure, with varying degrees of success.
To remedy this, we introduce the framework of structured contracts to formalize what it means for a stateful program to be correctly implemented on the ledger. Using small-step semantics, our approach relates low-level ledger transitions to high-level transitions of the smart contract being specified, thus allowing users to prove that their abstract specification is adequately realized on the blockchain. We argue that the framework is versatile enough to cover a range of examples, in particular proving the equivalence of multiple concrete implementations of the same abstract specification.
Building upon prior meta-theoretical results, our results have been mechanized in the Agda proof assistant, paving the way to rigorous verification of smart contracts.
Cite as
Polina Vinogradova, Orestis Melkonian, Philip Wadler, Manuel Chakravarty, Jacco Krijnen, Michael Peyton Jones, James Chapman, and Tudor Ferariu. Structured Contracts in the EUTxO Ledger Model. In 5th International Workshop on Formal Methods for Blockchains (FMBC 2024). Open Access Series in Informatics (OASIcs), Volume 118, pp. 10:1-10:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{vinogradova_et_al:OASIcs.FMBC.2024.10,
author = {Vinogradova, Polina and Melkonian, Orestis and Wadler, Philip and Chakravarty, Manuel and Krijnen, Jacco and Jones, Michael Peyton and Chapman, James and Ferariu, Tudor},
title = {{Structured Contracts in the EUTxO Ledger Model}},
booktitle = {5th International Workshop on Formal Methods for Blockchains (FMBC 2024)},
pages = {10:1--10:19},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-317-1},
ISSN = {2190-6807},
year = {2024},
volume = {118},
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.2024.10},
URN = {urn:nbn:de:0030-drops-198757},
doi = {10.4230/OASIcs.FMBC.2024.10},
annote = {Keywords: blockchain, ledger, smart contract, formal verification, specification, transition systems, Agda, UTxO, EUTxO, small-step semantics}
}