在Coq中形式化去中心化交易所
计算机科学中的逻辑
2022-03-16 v1 密码学与安全
摘要
导致加密资产重大损失的攻击与事故数量正在增长。据Chainalysis统计,2021年约140亿美元因各类事件损失,其中大部分来自去中心化金融(DeFi)应用。为解决这些问题,可使用从审计到形式化方法的一系列工具。我们采用形式化验证,并提供了在基础证明辅助工具中捕获合约交互的DeFi合约首个形式化。我们聚焦于Dexter2——Tezos网络上类似以太坊Uniswap的去中心化、非托管交易所。Dexter实现由若干智能合约组成。由于复杂的合约交互,这对形式化提出了独特挑战。我们的形式化包含针对Dexter实现所涉合约的非形式化规范的功能正确性证明。此外,我们的形式化是首个具备去中心化交易所交互智能合约安全性性质证明的工作。我们已将合约从Coq提取为CameLIGO代码,从而可部署于Tezos区块链。Uniswap与Dexter是一系列类似合约的典型代表。因此,我们的方法学使我们能够实现并验证具有类似交互模式的DeFi应用。
引用
@article{arxiv.2203.08016,
title = {Formalising Decentralised Exchanges in Coq},
author = {Eske Hoy Nielsen and Danil Annenkov and Bas Spitters},
journal= {arXiv preprint arXiv:2203.08016},
year = {2022}
}