Formalising Decentralised Exchanges in Coq

TY - GEN

T1 - Formalising Decentralised Exchanges in Coq

AU - Nielsen, Eske Hoy

AU - Annenkov, Danil

AU - Spitters, Bas

N1 - Funding Information: We would like to thank the LIGO team and in particular Tom Jack, Raphaël Cauderlier, Exequiel Rivas, Rémi Lesénéchal and Gabriel Alfour for the pleasant discussions. This research was partially supported by a grant from Nomadic Labs, by the Concordium Blockchain Research Center, and by a grant from CopenhagenFinTech. Publisher Copyright: © 2023 ACM.

PY - 2023/1

Y1 - 2023/1

N2 - The number of attacks and accidents leading to significant losses of crypto-assets is growing. According to Chainalysis, in 2021, approx. $14 billion has been lost due to various incidents, and this number is dominated by Decentralized Finance (DeFi) applications. To address these issues, one can use a collection of tools ranging from auditing to formal methods. We use formal verification and provide the first formalisation of a DeFi contract in a foundational proof assistant capturing contract interactions. We focus on Dexter2, a decentralized, non-custodial exchange for the Tezos network similar to Uniswap on Ethereum. The Dexter implementation consists of several smart contracts. This poses unique challenges for formalisation due to the complex contract interactions. Our formalisation includes proofs of functional correctness with respect to an informal specification for the contracts involved in Dexter's implementation. Moreover, our formalisation is the first to feature proofs of safety properties of the interacting smart contracts of a decentralized exchange. We have extracted our contract from Coq into CameLIGO code, so it can be deployed on the Tezos blockchain. Uniswap and Dexter are paradigmatic for a collection of similar contracts. Our methodology thus allows us to implement and verify DeFi applications featuring similar interaction patterns.

AB - The number of attacks and accidents leading to significant losses of crypto-assets is growing. According to Chainalysis, in 2021, approx. $14 billion has been lost due to various incidents, and this number is dominated by Decentralized Finance (DeFi) applications. To address these issues, one can use a collection of tools ranging from auditing to formal methods. We use formal verification and provide the first formalisation of a DeFi contract in a foundational proof assistant capturing contract interactions. We focus on Dexter2, a decentralized, non-custodial exchange for the Tezos network similar to Uniswap on Ethereum. The Dexter implementation consists of several smart contracts. This poses unique challenges for formalisation due to the complex contract interactions. Our formalisation includes proofs of functional correctness with respect to an informal specification for the contracts involved in Dexter's implementation. Moreover, our formalisation is the first to feature proofs of safety properties of the interacting smart contracts of a decentralized exchange. We have extracted our contract from Coq into CameLIGO code, so it can be deployed on the Tezos blockchain. Uniswap and Dexter are paradigmatic for a collection of similar contracts. Our methodology thus allows us to implement and verify DeFi applications featuring similar interaction patterns.

KW - blockchain

KW - Coq

KW - decentralized finance

KW - smart contracts

KW - software correctness

U2 - 10.1145/3573105.3575685

DO - 10.1145/3573105.3575685

M3 - Article in proceedings

AN - SCOPUS:85146984012

SN - 979-8-4007-0026-2

SP - 290

EP - 302

BT - CPP '23

A2 - Krebbers, Robert

A2 - Traytel, Dmitriy

A2 - Pientka, Brigitte

A2 - Zdancewic, Steve

PB - Association for Computing Machinery

CY - New York

T2 - 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023 - Co-located with POPL 2023

Y2 - 16 January 2023 through 17 January 2023

ER -