通过上下文敏感的共形验证寻找DeFi漏洞
软件工程
2024-04-17 v1
摘要
去中心化金融（DeFi）以其高可用性、透明性和防篡改等吸引人的特性正在彻底改变传统的中心化金融范式。然而，针对DeFi服务的攻击严重损害了DeFi市场，正如我们对2017年至2022年间80个真实世界DeFi事件的调查所证明的那样。现有方法基于符号执行、模型检查、语义分析和模糊测试，在识别大多数DeFi漏洞类型方面存在不足。为了解决这一缺陷，我们提出了上下文敏感的共形验证（CSCV），一种基于用户定义的时序逻辑属性自动发现DeFi漏洞的方法。CSCV构建并优化上下文以引导验证过程，该过程与共形执行并行地动态构建携带上下文的转换系统。此外，我们通过真实世界DeFi服务上的实验和定性比较证明了CSCV的有效性。实验结果表明，我们的CSCV原型成功检测了所调查事件中76.25%的漏洞，平均时间为253.06秒。
引用
@article{arxiv.2404.10376,
title = {Hunting DeFi Vulnerabilities via Context-Sensitive Concolic Verification},
author = {Yepeng Ding and Arthur Gervais and Roger Wattenhofer and Hiroyuki Sato},
journal= {arXiv preprint arXiv:2404.10376},
year = {2024}
}