DROPS

Document

Invited Talk

DOI: 10.4230/OASIcs.FMBC.2022.1

MEV-Freedom, in DeFi and Beyond (Invited Talk)

Authors: Massimo Bartoletti

Published in: OASIcs, Volume 105, 4th International Workshop on Formal Methods for Blockchains (FMBC 2022)

Abstract

Maximal Extractable Value (MEV) refers to a class of recent attacks on public blockchains, where adversaries with the power to reorder, drop or insert transactions in a block can "extract" value from user transactions in the mempool. Empirical research has shown that mainstream DeFi protocols, like e.g. Automated Market Makers and Lending Pools, are massively targeted by MEV attacks. This has detrimental effects on their users, on transaction fees, and on the congestion of blockchain networks. Despite the growing knowledge on MEV attacks on blockchain protocols, an exact definition is still missing. Indeed, formally defining these attacks is an essential prerequisite to the design of provably secure, MEV-free blockchain protocols. In this talk, we propose a formal definition of MEV, based on a general, abstract model of blockchains and smart contracts. We then introduce MEV-freedom, a property enjoyed by contracts resistant to MEV attacks. We validate this notion by rigorously proving that Automated Market Makers and Lending Pools are not MEV-free. We finally discuss how to design MEV-free contracts.

Cite as

Massimo Bartoletti. MEV-Freedom, in DeFi and Beyond (Invited Talk). In 4th International Workshop on Formal Methods for Blockchains (FMBC 2022). Open Access Series in Informatics (OASIcs), Volume 105, p. 1:1, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{bartoletti:OASIcs.FMBC.2022.1,
  author =	{Bartoletti, Massimo},
  title =	{{MEV-Freedom, in DeFi and Beyond}},
  booktitle =	{4th International Workshop on Formal Methods for Blockchains (FMBC 2022)},
  pages =	{1:1--1:1},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-250-1},
  ISSN =	{2190-6807},
  year =	{2022},
  volume =	{105},
  editor =	{Dargaye, Zaynah and Schneidewind, Clara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2022.1},
  URN =		{urn:nbn:de:0030-drops-171827},
  doi =		{10.4230/OASIcs.FMBC.2022.1},
  annote =	{Keywords: Blockchain, Smart Contracts, Formal Security Notion}
}

Document

DOI: 10.4230/LIPIcs.CONCUR.2018.40

Progress-Preserving Refinements of CTA

Authors: Massimo Bartoletti, Laura Bocchi, and Maurizio Murgia

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)

Abstract

We develop a theory of refinement for timed asynchronous systems, in the setting of Communicating Timed Automata (CTA). Our refinement applies point-wise to the components of a system of CTA, and only affecting their time constraints - in this way, we achieve compositionality and decidability. We then establish a decidable condition under which our refinement preserves behavioural properties of systems, such as their global and local progress. Our theory provides guidelines on how to implement timed protocols using the real-time primitives of programming languages. We validate our theory through a series of experiments, supported by an open-source tool which implements our verification techniques.

Cite as

Massimo Bartoletti, Laura Bocchi, and Maurizio Murgia. Progress-Preserving Refinements of CTA. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 40:1-40:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{bartoletti_et_al:LIPIcs.CONCUR.2018.40,
  author =	{Bartoletti, Massimo and Bocchi, Laura and Murgia, Maurizio},
  title =	{{Progress-Preserving Refinements of CTA}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{40:1--40:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.40},
  URN =		{urn:nbn:de:0030-drops-95786},
  doi =		{10.4230/LIPIcs.CONCUR.2018.40},
  annote =	{Keywords: protocol implementation, communicating timed automata, message passing}
}

Search Results

Documents authored by Bartoletti, Massimo

MEV-Freedom, in DeFi and Beyond (Invited Talk)

Abstract

Cite as

Progress-Preserving Refinements of CTA

Abstract

Cite as

Thanks for your feedback!

Could not send message