-
Finding smart contract vulnerabilities with ConCert's property-based testing framework
Authors:
Mikkel Milo,
Eske Hoy Nielsen,
Danil Annenkov,
Bas Spitters
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 contra…
▽ More
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.
△ Less
Submitted 1 August, 2022;
originally announced August 2022.
-
Extracting functional programs from Coq, in Coq
Authors:
Danil Annenkov,
Mikkel Milo,
Jakob Botsch Nielsen,
Bas Spitters
Abstract:
We implement extraction of Coq programs to functional languages based on MetaCoq's certified erasure. We extend the MetaCoq erasure output language with ty** information and use it as an intermediate representation, which we call $λ^T_\square$. We complement the extraction functionality with a full pipeline that includes several standard transformations (eta-expansion, inlining, etc) implemented…
▽ More
We implement extraction of Coq programs to functional languages based on MetaCoq's certified erasure. We extend the MetaCoq erasure output language with ty** information and use it as an intermediate representation, which we call $λ^T_\square$. We complement the extraction functionality with a full pipeline that includes several standard transformations (eta-expansion, inlining, etc) implemented in a proof-generating manner along with a verified optimisation pass removing unused arguments. We prove the pass correct wrt. a conventional call-by-value operational semantics of functional languages. From the optimised $λ^T_\square$ representation, we obtain code in two functional smart contract languages (Liquidity and CameLIGO), the functional language Elm, and a subset of the multi-paradigm language for systems programming Rust. Rust is currently gaining popularity as a language for smart contracts, and we demonstrate how our extraction can be used to extract smart contract code for the Concordium network. The development is done in the context of the ConCert framework that enables smart contract verification. We contribute with two verified real-world smart contracts (boardroom voting and escrow), which we use, among other examples, to exemplify the applicability of the pipeline. In addition, we develop a verified web application and extract it to fully functional Elm code. In total, this gives us a way to write dependently typed programs in Coq, verify, and then extract them to several target languages while retaining a small trusted computing base of only MetaCoq and the pretty-printers into these languages.
△ Less
Submitted 6 August, 2021;
originally announced August 2021.
-
Extracting Smart Contracts Tested and Verified in Coq
Authors:
Danil Annenkov,
Mikkel Milo,
Jakob Botsch Nielsen,
Bas Spitters
Abstract:
We implement extraction of Coq programs to functional languages based on MetaCoq's certified erasure. As part of this, we implement an optimisation pass removing unused arguments. We prove the pass correct wrt. a conventional call-by-value operational semantics of functional languages. We apply this to two functional smart contract languages, Liquidity and Midlang, and to the functional language E…
▽ More
We implement extraction of Coq programs to functional languages based on MetaCoq's certified erasure. As part of this, we implement an optimisation pass removing unused arguments. We prove the pass correct wrt. a conventional call-by-value operational semantics of functional languages. We apply this to two functional smart contract languages, Liquidity and Midlang, and to the functional language Elm. Our development is done in the context of the ConCert framework that enables smart contract verification. We contribute a verified boardroom voting smart contract featuring maximum voter privacy such that each vote is kept private except under collusion of all other parties. We also integrate property-based testing into ConCert using QuickChick and our development is the first to support testing properties of interacting smart contracts. We test several complex contracts such as a DAO-like contract, an escrow contract, an implementation of a Decentralized Finance (DeFi) contract which includes a custom token standard (Tezos FA2), and more. In total, this gives us a way to write dependent programs in Coq, test them semi-automatically, verify, and then extract to functional smart contract languages, while retaining a small trusted computing base of only MetaCoq and the pretty-printers into these languages.
△ Less
Submitted 26 April, 2021; v1 submitted 16 December, 2020;
originally announced December 2020.
