License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.FMBC.2022.2
URN: urn:nbn:de:0030-drops-171834
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/17183/
Go to the corresponding OASIcs Volume Portal


Milo, Mikkel ; Nielsen, Eske Hoy ; Annenkov, Danil ; Spitters, Bas

Finding Smart Contract Vulnerabilities with ConCert’s Property-Based Testing Framework

pdf-format:
OASIcs-FMBC-2022-2.pdf (0.8 MB)


Abstract

We provide three detailed case studies of vulnerabilities in smart contracts, and show how property based testing would have found them: 1. the Dexter1 token exchange; 2. the iToken; 3. the ICO of Brave’s BAT token. The last example is, in fact, new, and was missed in the auditing process.
We have implemented this testing in ConCert, a general executable model/specification of smart contract execution in the Coq proof assistant. ConCert contracts can be used to generate verified smart contracts in Tezos' LIGO and Concordium’s rust language. We thus show the effectiveness of combining formal verification and property-based testing of smart contracts.

BibTeX - Entry

@InProceedings{milo_et_al:OASIcs.FMBC.2022.2,
  author =	{Milo, Mikkel and Nielsen, Eske Hoy and Annenkov, Danil and Spitters, Bas},
  title =	{{Finding Smart Contract Vulnerabilities with ConCert’s Property-Based Testing Framework}},
  booktitle =	{4th International Workshop on Formal Methods for Blockchains (FMBC 2022)},
  pages =	{2:1--2:13},
  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/opus/volltexte/2022/17183},
  URN =		{urn:nbn:de:0030-drops-171834},
  doi =		{10.4230/OASIcs.FMBC.2022.2},
  annote =	{Keywords: Smart Contracts, Formal Verification, Property-Based Testing, Coq}
}

Keywords: Smart Contracts, Formal Verification, Property-Based Testing, Coq
Collection: 4th International Workshop on Formal Methods for Blockchains (FMBC 2022)
Issue Date: 2022
Date of publication: 06.10.2022
Supplementary Material: Software (The ConCert Framework): https://github.com/AU-COBRA/ConCert/tree/fmbc2022 archived at: https://archive.softwareheritage.org/swh:1:dir:00e8602bf86a672643073ed9b89a9de8436247a6


DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI