Move语言引用安全验证中的整数溢出漏洞分析

近期，在对Move语言进行深入研究时，我们发现了一个新的整数溢出漏洞。这个漏洞存在于引用安全验证过程中，其触发过程颇为有趣。本文将对这个漏洞进行深入分析，并探讨Move语言的一些相关背景知识。

Move语言在执行字节码前会进行代码单元验证，分为四个步骤。这个漏洞出现在reference_safety步骤中。

引用安全验证模块定义了用于验证过程主体的引用安全性的转移函数。其检查内容包括验证没有悬空引用、对可变引用的访问是否安全、对全局存储引用的访问是否安全等。

引用安全验证入口函数会调用analyze_function，对每个基本块进行验证。基本块是指除入口和出口外没有分支指令的代码序列。Move语言通过遍历字节码，查找所有分支指令和循环指令序列来确定基本块。

Move语言支持两种类型的引用：不可变引用&和可变引用&mut。不可变引用用于读取数据，可变引用用于修改数据。合理使用引用类型有助于维护安全性并识别读取模块。

引用安全模块会以函数为单位，扫描函数中基本块的字节码指令，验证所有引用操作是否合法。验证过程主要涉及AbstractState结构体，包含borrow graph和locals，用于确保函数中的引用安全性。

验证过程中会比较执行基本块前后的state，通过join_result是否发生变化来合并pre state和post state。如果发生变化且当前块存在指向自身的后向边（表示存在循环），将跳回循环开头，继续执行该基本块，直到post state等于pre state或因错误中止。

漏洞出现在判断join结果是否改变的过程中。当参数长度与局部变量长度之和大于256时，由于使用u8类型迭代locals，会导致整数溢出。虽然Move有检查locals个数的过程，但check bounds模块只检查了locals，未包括参数长度。

这个整数溢出漏洞可能导致拒绝服务（DoS）攻击。攻击者可以通过构造循环代码块并利用溢出改变块的state，使新的locals map与之前不同。当再次执行execute_block函数时，分析basic block中的字节码指令序列会访问新的locals map。如果指令需要访问的索引在新的AbstractState locals map中不存在，将导致DoS。

为验证这个漏洞，可以在git中重现PoC。PoC中的代码块包含一个无条件分支指令，每次执行最后一条指令时都会跳回第一条指令，导致多次调用execute_block和join函数。

这个漏洞表明即使是像Move这样注重安全的语言也可能存在安全隐患。它强调了代码审计的重要性，同时也建议Move语言设计者在运行时增加更多检查代码，以防止意外情况发生。目前Move主要在verify阶段进行安全检查，但一旦验证被绕过，运行阶段缺乏足够的安全加固可能导致更严重的问题。

作为Move语言安全研究的领导者，我们将继续深入研究Move的安全问题，并在后续分享更多发现。