本文揭示了PRBMath库中mulDivSigned函数的一个设计缺陷,该缺陷会导致在计算有符号数的乘法和除法时出现精度问题,特别是在DeFi应用中可能被利用导致资金损失。Certora团队通过形式化验证工具发现了这个存在于多个PRBMath版本中的问题,并与作者Paul Razvan Berg合作,最终通过修改函数定义为向零取整来临时解决,并计划在未来提供更全面的舍入模式支持。