在Coq正式建立分散的交易所
Formalising Decentralised Exchanges in Coq
摘要：
导致加密资产重大损失的攻击和事故数量正在增加。根据Chainalysis的数据，到2021年，大约由于各种事件，已经损失了140亿美元，而这个数字主要是分散式金融（DeFi）应用程序。为了解决这些问题，可以使用从审计到正式方法的一系列工具。我们使用形式化验证，并在捕获合同交互的基础证明助手中提供DeFi合同的第一次形式化。我们专注于Dexter2，这是一个去中心化的，非托管的Tezos网络交换，类似于以太坊上的Uniswap。Dexter的实现由几个智能合约组成。由于复杂的合同互动，这对正式化提出了独特的挑战。我们的形式化包括证明功能的正确性方面的一个非正式规范德克斯特的实施所涉及的合同。此外，我们的形式化是第一个证明去中心化交易所的交互智能合约的安全属性的特征。我们已经将合约从Coq提取到CameLIGO代码中，因此它可以部署在Tezos区块链上。Uniswap和Dexter是一系列类似合同的典范。因此，我们的方法使我们能够实现和验证具有类似交互模式的DeFi应用程序。
英文摘要：
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. In order 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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
