利用ConCert基于性质的测试框架发现智能合约漏洞
计算机科学中的逻辑
2022-10-07 v1 编程语言
摘要
我们提供了三个智能合约漏洞的详细案例研究，并展示了基于性质的测试本应如何发现它们：1. Dexter1代币交易所；2. iToken；3. Brave的BAT代币的ICO。最后一个例子实际上是新的，在审计过程中被遗漏了。我们已在ConCert中实现了该测试，ConCert是Coq证明助手中对智能合约执行的通用可执行模型/规范。ConCert合约可用于生成Tezos的LIGO和Concordium的rust语言中经验证的智能合约。因此我们展示了形式化验证与智能合约基于性质的测试相结合的有效性。
引用
@article{arxiv.2208.00758,
title = {Finding smart contract vulnerabilities with ConCert's property-based testing framework},
author = {Mikkel Milo and Eske Hoy Nielsen and Danil Annenkov and Bas Spitters},
journal= {arXiv preprint arXiv:2208.00758},
year = {2022}
}