本文讨论了在去中心化金融（DeFi）协议中，使用Solidity/Yul库进行数学计算的重要性。重点是展示了如何通过等价检查工具检测和证明常量函数市场制造商（CFMM）中的算术漏洞和相应的经济攻击，特别是PRBMath库中的舍入错误。文章提供了案例分析和完整的代码示例，强调了自动化检查的必要性。
本文揭示了PRBMath库中mulDivSigned函数的一个设计缺陷，该缺陷会导致在计算有符号数的乘法和除法时出现精度问题，特别是在DeFi应用中可能被利用导致资金损失。Certora团队通过形式化验证工具发现了这个存在于多个PRBMath版本中的问题，并与作者Paul Razvan Berg合作，最终通过修改函数定义为向零取整来临时解决，并计划在未来提供更全面的舍入模式支持。
Certora
netanel_81808