论文标题
通过音乐会的基于财产的测试框架查找智能合同漏洞
Finding smart contract vulnerabilities with ConCert's property-based testing framework
论文作者
论文摘要
我们提供三个详细的案例研究，以了解智能合约中的漏洞，并展示基于物业的测试如何找到它们： 1。dexter1代币交换； 2。 3。勇敢的蝙蝠令牌的ICO。 实际上，最后一个例子是新的，并且在审计过程中被错过。我们已经在COUQ证明助手中对智能合约执行的一般可执行模型/规范进行了协同实施此测试。音乐会合同可用于在Tezos的Ligo和Concordium的Rust语言中生成经过验证的智能合约。因此，我们显示了将正式验证和基于财产的智能合约测试结合起来的有效性。
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.
