HackerPapers

arXiv:2208.00758cs.LO

Finding smart contract vulnerabilities with ConCert's property-based testing framework

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

Early discovery. Linked by one identifiable commenter. This paper is outside the main ranking; a mention is not an endorsement.

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.

arXiv comments
Journal reference
FMBC: Formal Methods for Blockchains, 2022
DOI
doi:10.4230/OASIcs.FMBC.2022.2
Subjects
cs.LOLogic in Computer Science cs.PLProgramming Languages

On Hacker News

Linked by 1 identifiable commenter in 1 comment across 1 thread, from Aug 2022 to Aug 2022. Found in 1 HN submission from Aug 2022 to Aug 2022. Open submission discussions.

Comments linking this paper, per year.

Discussed in comments1 thread

  1. Finding smart contract vulnerabilities with ConCert 1 comment

    • "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…

      belterView on HNParent context

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.