如需转载请注明出处,侵权必究。
本文发表于CCS ’2022,第一作者是伊利诺伊理工学院和犹他大学芝加哥分校(Illinois Institute of Technology & University of Utah Chicago)的Yue Duan。
这篇文章关注于对去中心化应用(DApp)中智能合约的自动化安全审查,力图找到DApp中不正确或不公平的智能合约逻辑。例如,“卖方自己不得出价竞拍”等。相较于前人的工作,作者将模型检查技术运用到了智能合约代码语义恢复当中,并提出以UI界面文本为驱动、静态程序分析来引导的新技术,解决了智能合约新环境下的一个重要问题——自动化语义级安全分析。具体来说,文章的工具VetSC可以从合约代码中提取业务模型图,以捕获其内在的业务和安全逻辑,简化后续的模型检查工作。同时,VetSC利用从DApp用户界面检索到的文本语义,自动确定需要检查的安全规范,并通过排除不可信的UI文本,对 UI逻辑的一致性进行了验证。最后,作者通过一系列的实验证明了,VetSC可以准确地解释智能合约代码,同时自动化地,将high-level智能合约逻辑上的安全规范,应用于low-level对应的智能合约代码上,以进行同类合约的安全审查,并高效地发现现实世界DApp中的安全风险。将VetSC应用于34个真实世界的DApp后,更是成功地发现了19种新的安全风险,如过期彩票和重复投票等。
背景
样例分析
检测方法
实验评估
总结
Q&A
文案:陈奇童
排版:CXT
戳“阅读原文”即可查看论文原文哦~
原文始发于微信公众号(复旦白泽战队):白泽带你读论文 | VetSC
- 左青龙
- 微信扫一扫
- 右白虎
- 微信扫一扫
评论