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

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

*Corresponding author af dette arbejde

Publikation: Bidrag til bog/antologi/rapport/proceedingKonferencebidrag i proceedingsForskningpeer review

1 Citationer (Scopus)

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.

OriginalsprogEngelsk
Titel4th International Workshop on Formal Methods for Blockchains (FMBC 2022)
RedaktørerZaynah Dargaye, Clara Schneidewind
Antal sider13
ForlagDagstuhl Publishing
Publikationsdatookt. 2022
ISBN (Trykt)978-3-95977-250-1
DOI
StatusUdgivet - okt. 2022
Begivenhed4th International Workshop on Formal Methods for Blockchains, FMBC 2022 - Haifa, Israel
Varighed: 11 aug. 2022 → …

Konference

Konference4th International Workshop on Formal Methods for Blockchains, FMBC 2022
Land/OmrådeIsrael
ByHaifa
Periode11/08/2022 → …
SponsorExcellence Cluster ORIGINS
NavnOpenAccess Series in Informatics
Vol/bind105
ISSN2190-6807

Fingeraftryk

Dyk ned i forskningsemnerne om 'Finding Smart Contract Vulnerabilities with ConCert's Property-Based Testing Framework'. Sammen danner de et unikt fingeraftryk.

Citationsformater