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

Authors Murdoch J. Gabbay , Arvid Jakobsson , Kristina Sojakova



PDF
Thumbnail PDF

File

OASIcs.FMBC.2021.2.pdf
  • Filesize: 0.59 MB
  • 14 pages

Document Identifiers

Author Details

Murdoch J. Gabbay
  • Heriot-Watt University, Edinburgh, UK
  • Nomadic Labs, Paris, France
Arvid Jakobsson
  • Nomadic Labs, Paris, France
Kristina Sojakova
  • INRIA, Paris, France

Acknowledgements

The authors acknowledge the support of Nomadic Labs and the detailed and very helpful comments of three anonymous referees. We also thank Benoît Rognier, the Edukera team, and Tom Jack for their feedback and support.

Cite AsGet BibTex

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)
https://doi.org/10.4230/OASIcs.FMBC.2021.2

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.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Formal software verification
  • Theory of computation → Program verification
  • Social and professional topics → Quality assurance
Keywords
  • Distributed ledger
  • smart contracts
  • Coq
  • formal verification
  • blockchain

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. Nicola Atzei, Massimo Bartoletti, and Tiziana Cimoli. A Survey of Attacks on Ethereum Smart Contracts (SoK). In Matteo Maffei and Mark Ryan, editors, Principles of Security and Trust, pages 164-186, Berlin, Heidelberg, 2017. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-662-54455-6_8.
  2. Bruno Bernardo, Raphaël Cauderlier, Zhenlei Hu, Basile Pesin, and Julien Tesson. Mi-Cho-Coq, a Framework for Certifying Tezos Smart Contracts. In Formal Methods. FM 2019 International Workshops - Porto, Portugal, October 7-11, 2019, Revised Selected Papers, Part I, volume 12232 of Lecture Notes in Computer Science, pages 368-379. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-54994-7_28.
  3. L.M. Goodman. Tezos - a self-amending crypto-ledger, 2014. URL: https://tezos.com/whitepaper.pdf.
  4. Ivica Nikolić, Aashish Kolluri, Ilya Sergey, Prateek Saxena, and Aquinas Hobor. Finding The Greedy, Prodigal, and Suicidal Contracts at Scale. In Proceedings of the 34th Annual Computer Security Applications Conference, ACSAC '18, page 653–663, New York, NY, USA, 2018. Association for Computing Machinery. URL: https://doi.org/10.1145/3274694.3274743.
  5. Daejun Park, Yi Zhang, Manasvi Saxena, Philip Daian, and Grigore Roşu. A Formal Verification Tool for Ethereum VM Bytecode. In Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2018, page 912–915, New York, NY, USA, 2018. Association for Computing Machinery. URL: https://doi.org/10.1145/3236024.3264591.
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