DROPS

Document

DOI: 10.4230/OASIcs.FMBC.2021.2

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

DOI: 10.4230/LIPIcs.CSL.2015.374

Leaving the Nest: Nominal Techniques for Variables with Interleaving Scopes

Authors: Murdoch J. Gabbay, Dan R. Ghica, and Daniela Petrisan

Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)

Abstract

We examine the key syntactic and semantic aspects of a nominal framework allowing scopes of name bindings to be arbitrarily interleaved. Name binding (e.g. delta x.M) is handled by explicit name-creation and name-destruction brackets (e.g. <delta x M x>) which admit interleaving. We define an appropriate notion of alpha-equivalence for such a language and study the syntactic structure required for alpha-equivalence to be a congruence. We develop denotational and categorical semantics for dynamic binding and provide a generalised nominal inductive reasoning principle. We give several standard synthetic examples of working with dynamic sequences (e.g. substitution) and we sketch out some preliminary applications to game semantics and trace semantics.

Cite as

Murdoch J. Gabbay, Dan R. Ghica, and Daniela Petrisan. Leaving the Nest: Nominal Techniques for Variables with Interleaving Scopes. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 374-389, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{gabbay_et_al:LIPIcs.CSL.2015.374,
  author =	{Gabbay, Murdoch J. and Ghica, Dan R. and Petrisan, Daniela},
  title =	{{Leaving the Nest: Nominal Techniques for Variables with Interleaving Scopes}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{374--389},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Kreutzer, Stephan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.374},
  URN =		{urn:nbn:de:0030-drops-54262},
  doi =		{10.4230/LIPIcs.CSL.2015.374},
  annote =	{Keywords: nominal sets, scope, alpha equivalence, dynamic sequences}
}

Search Results

Documents authored by Gabbay, Murdoch J.

Money Grows on (Proof-)Trees: The Formal FA1.2 Ledger Standard

Abstract

Cite as

Leaving the Nest: Nominal Techniques for Variables with Interleaving Scopes

Abstract

Cite as

Thanks for your feedback!

Could not send message