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的安全問題，並在後續分享更多發現。