白泽带你读论文 | VetSC

admin 2023年2月15日20:12:21评论24 views字数 6267阅读20分53秒阅读模式


如需转载请注明出处,侵权必究。


本文发表于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种新的安全风险,如过期彩票和重复投票等。


背景

去中心化应用程序(DApp)是在去中心化网络上运行的应用程序,DApp结合了智能合约(区块链上的程序)和前端的用户界面。与需要专业技能才能进行交互的原始智能合约相比,去中心化应用在值得信赖的交易与用户友好的界面之间取得了平衡。因此,DApp越来越受欢迎——在过去三年中,已经有18个类别的4000个DApp被创建,每月都有数百个新应用发布。
尽管如此,去中心化应用的快速普及也带来了安全风险。由于不正确或不公平的智能合约逻辑,不安全的DApp可能会造成严重的财务损失。许多先前研究都试图验证智能合约的正确性与安全性,所用方法往往依赖于开发人员在源代码中创建的函数符号和变量名称来获得关键的语义。然而,这些符号是不可信的,且有时会由于缺少源代码或故意混淆等情况而不可用;此外,先前的工作必须对每个智能合约功能,重复地进行源代码手动解释。即便是同一类型的合同,由于它们的实施可能会使用不同的功能或变量名称,也无法自动地应用相应安全规范。

样例分析

白泽带你读论文 | VetSC

作者使用真实世界的以太坊分散应用程序Auction DApp演示了这个问题。图1显示了带有三个按钮的用户界面。具体来说,用户可以单击“立即出价”按钮,参与由商品所有者创建的现有拍卖。如果所有者按下同一页面上的特定按钮“取消拍卖”,拍卖也可能被取消。
白泽带你读论文 | VetSC
这两个按钮分别与两个智能合约函数bidOnAction()和cancelAuction()在内部关联。图2描述了使用Solidity(以太坊合约专用编程语言)实现的两个智能合约函数。为了可读性,此处以源代码显示程序,而实际的分析是直接在字节码上执行的。
bidOnAction()执行投标过程。它从交易属性msg.value(Ln.2)中获取出价,该属性表示函数调用方(即投标人)发送的金额。然后,会进行两次检查,以确保业主不能出价,拍卖未到期。如果两项检查都通过,则函数将出价与当前最高出价lastBid.amount或默认价格startPrice进行比较,从而确定新价格是否更高(Ln.11-21)。
cancelAuction()使用修饰符isOwner(Ln.31)来确保只有商品所有者才能调用该函数。当执行时,该函数首先根据给定的id(Ln.32-33)检索Auction对象myAuction和先前接受的出价[_id]的数组。接下来,如果存在先前出价(Ln.36-39),它将退还该数组中的最后一个出价者,即当前最高的出价者。最终将此拍卖变为非活动状态,同时通过发出声明生成日志(Ln.40-41)。
单击“取消拍卖”按钮时,可能会触发cancelAuction()中的安全问题。取消拍卖时必须执行两项安全规则:(1)只有所有者才能取消拍卖;以及(2)未收到有效投标。第二条保证了拍卖的公平性,因为它确保了当参与者已经提交了有效的出价时,无论所有者的意图如何,拍卖都不会被任意终止。然而,cancelAuction()并不强制执行此策略,因此允许所有者在任何阶段取消拍卖。

检测方法

1、智能合约自动化语义恢复的独特点
为了将high-level的安全规范(例如,“卖方自己不得出价竞拍”)应用于low-level上对应的智能合同代码,必须先揭示单个智能合约功能的业务逻辑级操作,例如出价;接着将交易概念(例如,投标人、卖方、出价价格)与功能中的特定变量相关联,然后再从high-level的安全规范中,手动创建智能合约特定的正式规范。
事实上,将精确的安全规范自动应用于智能合约函数是一个具有挑战性的问题,因为它需要安全验证器来识别该函数及其变量的语义。例如,为了检测图2样例中的安全问题,验证器必须能够理解cancelAuction()函数用于“终止竞价过程”,并将变量拍卖[_id]和接受[_id]分别与“本次拍卖”和“本次竞标中接受的先前出价”相关联。只有这样,验证器才能发现违反上述公平策略的行为,因为该函数允许在存在有效出价(bidsLength!=0)时停用拍卖(拍卖[_id].active=false)。
先前验证合同安全性的工作(如VerX)通过从源代码中手动读取符号(如函数和变量名)来推断这些语义。然而,这种方法既不有效也不稳健。为了解决这个问题,作者尝试自动恢复智能合约函数和关键变量的语义。
自动化和稳健的语义恢复已在许多领域得到了很好的研究。不幸的是,VMI(Virtual machine introspection 虚拟机自省技术)和二进制分析技术只能恢复操作系统级的数据结构和原始类型,并不涉及应用程序级的语义;移动和物联网应用程序分析器基于语义丰富的框架API(例如,sendTextMessage()、lock.unlock())来解释程序行为,然而,智能合约的编程语言中并不存在此类API。
白泽带你读论文 | VetSC

2、传统模型检查的问题及本文提出的优化
模型检查同样在大量的先前工作中被用来自动匹配,语义级工业过程规范和低级控制器代码。然而,
(1)它依赖于一个假设,即分析师对目标工业过程具有高水平但精确的知识优势,因此可以制定精确的规范。然而,当分析未知方开发的各种DApp时,这一假设并不成立。
(2)与严格表达有限控制变量之间核心依赖关系的控制器逻辑相比,智能合约代码不那么严格,通常包含了与其核心逻辑无关的变量及其关系。引入大量非必要代码可能会导致模型检查过于复杂和不精确。
为了解决这些问题,作者提出了一种新的UI驱动、程序分析引导的模型检查技术,该技术可以自动提取去中心化应用程序中的智能合约语义,以实现有针对性的安全检查。
具体来说,为了排除无关代码并减少模型检查器的搜索空间,作者通过静态程序分析,从合同函数中提取业务模型图,这些合同函数可以跨关键事务财产捕获内在业务逻辑;为了自动选择安全审查的规范,作者利用从DApp用户界面收集的文本信息,来描述高级底层合同逻辑行为。

3、所实现工具VetSC的工作流程
白泽带你读论文 | VetSC

给定一个DApp,VetSC
1) 首先提取每个智能合约功能的业务模型。特别地,先确定每个函数中的关键业务级属性。从这些属性开始进行静态控制流和数据流分析,以构建表示函数语义模型的业务模型图。
2) 接下来,通过UI引导的模型检查,恢复业务模型提取图的语义。(更具体地说,先分析DApp的web代码,以将每个合约函数与触发该函数的前端小部件相关联。然后,将自然语言处理技术应用于小部件上的文本,以推断小部件描述的业务逻辑。根据从UI组件中提取的文本语义,可以从预定义的业务模型中选择相应的业务逻辑规范。因此,进行模型检查,根据此规范验证业务模型图。如果发现重大不一致,将报告此问题并终止分析。)
3) 如果提取的图与所描述的语义一致,就可以确定智能合约函数的业务逻辑。从而可以自动将相应的安全规则,应用于该功能的审查,以检测任何违规行为。
白泽带你读论文 | VetSC

相较于前人的语义恢复工作,本文的最大的创新之处在于将该技术应用在了智能合约这一新环境中。也因此,本文发明了一种新的算法来提取能够反映语义的,智能合约和交易中的特定属性。此外,本文还进一步恢复了业务逻辑级的语义。

白泽带你读论文 | VetSC

值得注意的是,尽管作者的观察结果表明,来自良性开发人员的UI信息在很大程度上是可信的,但作者并不假设所有DApp UI文本都是正确或完整的。
因此,为了在合并UI信息时谨慎起见,作者采用了基于矛盾证明的方法。即首先认为UI文本解释的业务逻辑是正确的,这使工具能够避免对相应规范的详尽搜索,从而缩小检查范围。之后,如果内部逻辑实际上偏离了DApp描述(例如,UI显示DApp是一个赌博应用程序,但其内部智能合约代码实现的是拍卖逻辑),则会出现警告。只有当内部逻辑与UI语义相匹配时,才会进行安全规范的校验。

实验评估

数据集收集
利用GitHub引擎,使用关键字“DApp+”搜索“最佳匹配”开源非令牌项目,并从6个类别中检索出前100个应用。然后,从600个中确定了144个具有UI的应用程序。之后进一步排除了无法安装的“不完整”应用程序,最终获得了30个可用的应用程序。“不完整”的应用主要有以下三类:
a) 后端智能合约代码无法构建或部署,因为编译器版本不兼容或缺少部署规范。
b) 前端UI代码仅包含单个核心组件,但不包含重要的或最新的依赖项或入口点。许多项目甚至都不知道精确的npm版本;一些应用程序不提供包括index.HTML在内的关键HTML界面。
c) 即使后端功能和前端小部件都已完成,它们的连接也可能被错误配置。
对于“不完整”的应用,VetSC需要对它们执行动态分析,以在运行时将前端HTML文本和JavaScript代码与后端合约调用相关联。

影响力研究
同时,为验证该测试集是否具有代表性,作者分别从流行度与同质化两个角度展开了分析:
首先,在34个测试应用中,作者手动验证(通过元数据、网站信息、简单代码匹配)其中11个已部署在以太坊主网上,此现象表明,该数据集已涵盖当下非常流行的去中心化应用。
其次,作者还发现,在以太坊区块链和GitHub项目中,其核心功能(例如,投标、交易等)代码高度同质化,仅通过简单的字符串匹配,就发现了1396个副本(507个来自区块链,889个来自GitHub),其智能合约代码与数据集中34个应用程序相同。

结果分析

白泽带你读论文 | VetSC
1、误报及漏报
 大部分误报是由于间接的“资金流动”造成的。虽然这些应用的智能合约实际上符合规则,将资金发送给了收款人,但它们并没有直接使用send()API实现这样的交易。相反,它们首先将资金添加到收款人的虚拟账户中,然后在减少虚拟余额的同时转移资金。VetSC的静态分析没有跟踪到对虚拟余额执行算术运算的资金流,因此错过了这一间接资金转移,导致误报。
VetSC分别在检查彩票抽奖安全2号政策(截止日期前不得抽奖)、钱包取款安全1号规则(余额检查)和投票安全2号规则(禁止双重投票)时,出现了三个漏报。其中的10号应用实际上是以隐含的方式检查彩票游戏的结束时间。在其智能合约中没有根据最终期限检查当前时间,而是根据单个“回合”的结束时间进行检查。VetSC并未将这些“子期限”与最终期限相关联,因此未检测到此类时间检查。

白泽带你读论文 | VetSC
2、限制与不足之处
1) 本文的语义推理仍然受到NLP所共有的障碍——修辞和隐喻。例如,拍卖App“以太王座之王”有一个按钮是“认领王座”,它实际上的功能是出价,但因为该短语与竞标过程中使用的常见文本差异过大,无法正确识别。
2) 对于动态生成的网页的内容,除非触发了某些JS代码,否则无法自动化地观察。
3) 除此之外,虽然大多数小部件文本都是短语,但确实存在长文本的小部件。因此有必要在句子层面识别核心语义实体,而不是直接应用单词层面的解释。
4) 其次,领域知识的利用可能会从根本上限制VetSC探索更广泛的文本语义的能力。
5) 此外,由于UI分析部分基于文本解释,因此无法处理那些不包含任何文本,使用图标传递信息的组件。

3、大型应用与Defi(去中心化金融)应用
文章的语义推理适用于大型应用程序,因为即使复杂应用程序中的核心逻辑可能很密集(1836行),其核心需进行安全分析的拍卖逻辑仅包含少量代码(约20行)。当然,如果应用核心逻辑过于复杂,也可能影响模型检查的精度和效率。
白泽带你读论文 | VetSC
DeFi(去中心化金融)应用程序使用密集的跨合约(Cross-Contract)交易,在区块链上提供复杂的金融服务。
文章的评估表明,尽管理论上VetSC仍能够捕捉到它们的核心业务逻辑,却无法处理其中跨越了多个合约的部分。本质上,这一缺陷是因为VetSC采用了和VerX一样的有效外部无回调Effectively External Callback Free(EECF)模型,因此会将所有的外部调用都视为NOP(无操作指令)。

总结

文章首次实现了对去中心化应用(DApp)中合同语义的自动化安全审查工具——VetSC,这是一种新颖的UI驱动、程序分析引导的模型检查技术,可以自动提取去中心化应用程序中的合同语义,从而实现有针对性的安全检查。文章通过业务模型图来建模核心业务逻辑行为,从DApp UI中检索文本语义,以帮助自动定制安全规范。同时,将VetSC应用于34个真实世界的DApp后,已发现了19个新的安全问题。

Q&A

1、为什么需要收集UI的上下文信息Scontext?
主要用于区分具有相同文本的UI组件,在不同业务场景下的功能差异,例如,拍卖应用程序中的“立即购买”按钮表示出价,而赌博应用程序中具有相同文本的按钮表示“下注”。
2、为什么要在字节码而不是源码上进行分析?
去中心化应用中包含许多不相关的指令,且源代码存在混淆和不开源的情况,难以准确捕获其中智能合约的核心逻辑,使用静态分析有选择地提取表示程序语义的Solidity字节码指令,则可以避免这个问题。
3、为什么可以识别字节码中的交易属性,如何识别?
作者研究了EVM文档,发现交易属性的用法是通过特殊指令实现的。例如,对于实例𝑚𝑠𝑔.𝑠𝑒𝑛𝑑𝑒𝑟,只能由EVM指令CALLER访问,而CALLVALUE指令则用于检索𝑚𝑠𝑔.𝑣𝑎𝑙𝑢𝑒。由于交易属性的数量有限,并且指令是固定的,因此作者可以通过维护一个预定义的指令列表,以便在字节码程序中发现这些交易属性。
4、内存中的别名匹配是如何实现的?会存在漏报吗?
作者自定义了一个指向性分析,使用计算树的结构作为签名来表示内存偏移量,分析了同一地址的存储和加载,以便显式地连接相应的操作。
虽然VetSC的内存别名匹配技术可能会导致理论上的漏报。然而,由于应用中整个合约仅使用Solidity编译器的一个版本进行编译,该编译器以相同的方式计算同一内存位置的偏移量,因此作者在实践中没有发现错误。
5、数据集中为什么要排除令牌交换应用程序?
因为令牌交换应用程序的业务和安全逻辑,通常不是在智能合约中实现,而是在自定义应用程序级别实现的。

文案:陈奇童

排版:CXT

戳“阅读原文”即可查看论文原文哦~


复旦白泽战队
一个有情怀的安全团队




原文始发于微信公众号(复旦白泽战队):白泽带你读论文 | VetSC

  • 左青龙
  • 微信扫一扫
  • weinxin
  • 右白虎
  • 微信扫一扫
  • weinxin
admin
  • 本文由 发表于 2023年2月15日20:12:21
  • 转载请保留本文链接(CN-SEC中文网:感谢原作者辛苦付出):
                   白泽带你读论文 | VetSChttps://cn-sec.com/archives/1553906.html

发表评论

匿名网友 填写信息