22 Search Results for "Bernardo, Bruno"


Volume

OASIcs, Volume 95

3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)

FMBC 2021, July 18-19, 2021, Los Angeles, California, USA (Virtual Conference)

Editors: Bruno Bernardo and Diego Marmsoler

Volume

OASIcs, Volume 84

2nd Workshop on Formal Methods for Blockchains (FMBC 2020)

FMBC 2020, July 20-21, 2020, Los Angeles, California, USA (Virtual Conference)

Editors: Bruno Bernardo and Diego Marmsoler

Document
Complete Volume
OASIcs, Volume 95, FMBC 2021, Complete Volume

Authors: Bruno Bernardo and Diego Marmsoler

Published in: OASIcs, Volume 95, 3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)


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-dev.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

Authors: Bruno Bernardo and Diego Marmsoler

Published in: OASIcs, Volume 95, 3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)


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-dev.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

Authors: Kinnari Dave, Vilhelm Sjöberg, and Xinyuan Sun

Published in: OASIcs, Volume 95, 3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)


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

Authors: Murdoch J. Gabbay, Arvid Jakobsson, and Kristina Sojakova

Published in: OASIcs, Volume 95, 3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)


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-dev.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)

Authors: Daniel Britten, Vilhelm Sjöberg, and Steve Reeves

Published in: OASIcs, Volume 95, 3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)


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-dev.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)

Authors: Sylvain Conchon, Alexandrina Korneva, Çagdas Bozman, Mohamed Iguernlala, and Alain Mebsout

Published in: OASIcs, Volume 95, 3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)


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)

Authors: Thi Thu Ha Doan and Peter Thiemann

Published in: OASIcs, Volume 95, 3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)


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-dev.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}
}
Document
Complete Volume
OASIcs, Volume 84, FMBC 2020, Complete Volume

Authors: Bruno Bernardo and Diego Marmsoler

Published in: OASIcs, Volume 84, 2nd Workshop on Formal Methods for Blockchains (FMBC 2020)


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

Authors: Bruno Bernardo and Diego Marmsoler

Published in: OASIcs, Volume 84, 2nd Workshop on Formal Methods for Blockchains (FMBC 2020)


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)

Authors: Grigore Rosu

Published in: OASIcs, Volume 84, 2nd Workshop on Formal Methods for Blockchains (FMBC 2020)


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)

Authors: Ákos Hajdu, Dejan Jovanović, and Gabriela Ciocarlie

Published in: OASIcs, Volume 84, 2nd Workshop on Formal Methods for Blockchains (FMBC 2020)


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

Authors: Maria A. Schett and Julian Nagele

Published in: OASIcs, Volume 84, 2nd Workshop on Formal Methods for Blockchains (FMBC 2020)


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

Authors: João Santos Reis, Paul Crocker, and Simão Melo de Sousa

Published in: OASIcs, Volume 84, 2nd Workshop on Formal Methods for Blockchains (FMBC 2020)


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}
}
  • Refine by Author
  • 4 Bernardo, Bruno
  • 4 Marmsoler, Diego
  • 2 Sjöberg, Vilhelm
  • 1 Boss, Ramon
  • 1 Boyd, Colin
  • Show More...

  • Refine by Classification
  • 5 Security and privacy → Logic and verification
  • 5 Software and its engineering → Formal software verification
  • 4 Computer systems organization → Peer-to-peer architectures
  • 4 Security and privacy → Distributed systems security
  • 4 Theory of computation → Logic and verification
  • Show More...

  • Refine by Keyword
  • 4 Blockchain
  • 3 blockchain
  • 3 smart contracts
  • 2 Bitcoin
  • 2 Conference Organization
  • Show More...

  • Refine by Type
  • 20 document
  • 2 volume

  • Refine by Publication Year
  • 14 2020
  • 8 2021

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail