本文揭示了PRBMath库中mulDivSigned函数的一个设计缺陷,该缺陷会导致在计算有符号数的乘法和除法时出现精度问题,特别是在DeFi应用中可能被利用导致资金损失。Certora团队通过形式化验证工具发现了这个存在于多个PRBMath版本中的问题,并与作者Paul Razvan Berg合作,最终通过修改函数定义为向零取整来临时解决,并计划在未来提供更全面的舍入模式支持。
本文介绍了Certora Equivalence Checker工具,旨在帮助开发者优化DeFi产品的智能合约,解决Gas消耗、安全性和市场发布速度之间的三重困境。通过比较不同版本的代码,工具能有效检测潜在的低严重性和高严重性漏洞,并加强开发过程中的形式验证,确保代码的功能等价性。