SaferMaker 的文章 - 登链社区

TA的文章 TA购买的 TA喜欢的 TA收藏的

这篇文章系统介绍了符号执行作为一种确保智能合约安全性和正确性的技术，详细阐述了其定义、原理及应用。文章还对多种以太坊智能合约的符号执行工具（如Mythril、Manticore、hevm和EthBMC）进行了对比实验，展示了它们在识别智能合约漏洞方面的优势和局限，并探讨了未来的改进方向。

符号执行智能合约 Mythril Manticore EthBMC 安全性验证

发布于 2023-05-02 14:11 阅读(14) 点赞(0)

当不变量不成立时：DAI的Certora惊喜

本文探讨了MakerDAO的Multi-Collateral DAI稳定币的一个重要发现：尽管过去被认为是可证明的不可变关系，使用Certora Prover进行的形式验证显示该关系并未成立。文章详细阐述了使用Certora工具进行形式验证的过程和技术细节，并强调了开发智能合约时保持谦虚和开放心态的重要性。

Makerdao Multi-Collateral DAI Formal Verification Certora Prover 智能合约安全性

发布于 2022-06-25 10:29 阅读(9) 点赞(0)