基于符號執行的代幣買賣漏洞和權限轉移漏洞的檢測驗證方法

劉宇航 劉軍杰 文偉平

(北京大學軟件與微電子學院 北京 100871)

隨著區塊鏈技術和應用的不斷發展落地，越來越多的用戶和軟件工程師傾向于在區塊鏈平臺上開發、交互應用甚至配置數字資產.智能合約就是存儲和運行在區塊鏈上的應用程序，通過智能合約和區塊鏈的POW，POS，PBFT等共識機制，可以在數字世界建立信任.以太坊、幣安智能鏈等很多區塊鏈平臺都支持智能合約的運行.區塊鏈的智能合約一般由圖靈完備的編程語言寫成.智能合約帶給開發者和用戶以無限的創造性，能夠使用智能合約編程語言(例如Solidity)定義各種規則，生成更多去中心化的應用供平臺用戶進行調用和交互.

這種去中心化、靈活可變、安全可靠的特性，使得智能合約被廣泛地用于去中心化金融(DeFi[1])和數字貨幣領域.

然而由于智能合約開發者的代碼不規范、智能合約編程語言或虛擬機固有的缺陷，使得區塊鏈上存在大量有漏洞甚至容易被利用的智能合約，造成了很多智能合約攻擊事件的發生，尤其是在去中心化金融領域，很多有漏洞的智能合約上存儲的數字資產被攻擊者一卷而空，產生不可估量的損失.

在DeFi領域中最常見的攻擊事件中，一類是欺詐性代幣攻擊事件，也被稱為“貔貅盤”事件.這種攻擊一般和與去中心化交易所進行交互的代幣合約有關，這種代幣合約由于合約開發者在編寫智能合約transfer函數時產生了有意或者無意的代碼漏洞，或者嵌入了惡意的后門代碼，使得該合約中的代幣買賣存在漏洞，例如只能在交易所買入，無法賣出，或者實際賣出數量與用戶所期望數量不相符等.

另一種則是基于智能合約owner權限轉移漏洞的攻擊事件.幾乎所有的智能合約中都有權限控制相關的代碼邏輯，如何正確地將權限控制置于自己所開發的代碼中，對于開發者來說相當重要，如果設計不當就會產生權限篡改的風險.著名的跨鏈互操作協議Poly Network[2]，就曾因為權限控制代碼邏輯漏洞，被攻擊者修改了合約屬主權限，從而在以太坊、幣安智能鏈以及Polygon這3大區塊鏈平臺上分別被盜走2.5億美元、2.7億美元、8 500萬美元的加密資產，損失總額高達6.1億美元[3].

目前對于智能合約漏洞的研究往往僅限于一些傳統的特定漏洞，例如：整數溢出、重入、delegatecall導致的意外代碼執行、合約構造函數與合約名不一致等漏洞[4].這些漏洞有一部分已經被更新版本的智能合約語言編譯器消除，例如Solidity在0.8版本將默認內置整數溢出檢查[5]，開發者不再為因疏忽引起的整數溢出漏洞而擔驚受怕，同時在Solidity 0.4.22版本之后，開發者定義的合約構造函數名也不需要與合約名一致，而是統一用constructor代替，消除了合約構造函數與合約名不一致漏洞的產生.另外為避免一些漏洞，例如未檢查返回值、重入漏洞等，智能合約Solidity網站也發布了簡潔、可靠的安全編程規范[6-7]和框架避免寫出有漏洞的合約.

可以看出很傳統的智能合約漏洞模式已經逐漸被消除和有效地規避，并且在目前的研究中發現并未產生過大的危害[8].但目前各種新型的智能合約漏洞正在逐漸涌現，例如本文提到的造成欺詐性代幣攻擊的代幣買賣漏洞和造成權限篡改攻擊的智能合約owner權限轉移漏洞，而目前的研究很少能夠總結出一套全面的、有效的自動化檢測方案.

鑒于此，本文提出了一種針對智能合約字節碼和源碼的基于靜態語義分析和符號執行的智能合約漏洞檢測方法，可以用來檢測智能合約的代幣買賣漏洞和owner權限轉移漏洞.

本文的主要貢獻在于：

1) 對于智能合約代幣買賣漏洞和權限轉移漏洞進行研究，總結了代幣買賣漏洞和owner權限轉移漏洞模型；

2) 在智能合約字節碼和源碼層面，提出了針對代幣買賣漏洞和owner權限轉移漏洞的自動化檢測工具；

3) 調研和總結了目前在以太坊和幣安智能鏈2大區塊鏈平臺上的代幣買賣漏洞和owner權限轉移漏洞的常見利用情況以及攻擊背景和手法.

1 相關工作

在基于符號執行的智能合約自動化安全審計技術領域，Luu等人[9]提出了基于符號執行的Oyente工具來自動化檢測智能合約中存在的整數溢出、時間戳依賴、交易順序依賴以及重入等漏洞；Muller[10]提出了另外一款基于符號執行技術的工具Mythril，以檢測整數溢出、代碼重入等常見安全問題；Tsankov等人[11]開發了一種基于符號執行的智能合約自動化檢測工具Securify,該工具可以針對給定的性質來驗證智能合約的行為是否安全；Nikolic等人[12]實現了一種基于符號分析和程序驗證器的工具Maian，該工具通過分析智能合約函數之間調用的字節碼序列來檢測可能存在的安全漏洞；Zhou等人[13]設計了一種名為SASC的靜態分析工具，該工具同樣基于符號執行技術，用于智能合約邏輯分析，可以生成函數之間調用流圖，以幫助查找智能合約潛在的邏輯漏洞.除此之外，還有Manticore[14],VerX[15]等智能合約自動化檢測工具也是采用符號執行技術.

在基于程序靜態分析的智能合約自動化安全審計技術方面，Tikhomirov等人[16]提出了一種可擴展的靜態分析工具SmartCheck，將solidity源代碼轉換為基于XML的中間表示形式，然后根據定義的XPath進行漏洞檢測；Feist等人[17]提出了一種靜態分析框架Slither，它集成了大量漏洞檢測模型，通過中間表示(SlithIR)可實現簡單、高精度的分析，并提供一個API來輕松編寫自定義合約分析；Kalra等人[18]提出了智能合約的靜態分析框架ZEUS，它能夠自定義用戶策略，將附加上用戶策略的合約源碼轉換為LLVM-IR的中間表示，然后結合LLVM-IR的分析工具進行代碼分析和漏洞檢測.該方案在進行合約源碼到中間表示轉換時容易失真，LLVM-IR無法完全模擬智能合約的代碼和運行環境.

在基于模糊測試的智能合約漏洞檢測領域，Trail of Bits安全團隊[19]提出了以太坊智能合約模糊測試框架Echidna，通過靜態分析和模擬執行智能合約源碼來自動化生成調用合約方法的交易數據.而ContractFuzzer[20]將模糊測試和漏洞檢測方式結合，通過隨機生成交易數據、交易發起者、交易金額和日志監測來檢測有無漏洞觸發.在模糊測試種子生成策略方面，ILF[21]采用基于神經網絡的機器學習算法，對通過符號執行后生成的高覆蓋率交易序列進行學習，從而生成更好的模糊測試策略.但是模糊測試方法相較于符號執行，依舊存在著路徑覆蓋不夠全面的問題.

以上大多數工具都是針對傳統的以太坊智能合約漏洞，如算術溢出、重入、交易順序依賴、delegatecall導致意外代碼執行[22]等，但對于其他的一些危害較為嚴重的新型漏洞模式則不能準確識別，比如代幣買賣漏洞、owner權限轉移漏洞等.

2 漏洞分析及其檢測方法

2.1 代幣買賣漏洞

2.1.1 漏洞產生的原因及危害

代幣買賣漏洞通常發生在遵循ERC-20代幣標準的智能合約的transfer函數調用流中.

ERC-20代幣標準是以太坊區塊鏈上一種通用的同質化代幣標準，通過遵循ERC-20代幣標準，可以讓不同智能合約中發行的代幣都具有相同的類型和接口.

ERC-20代幣標準中定義了標準函數和標準事件，如表1所示.其中涉及到代幣買賣的函數是transfer和transferFrom函數，這2種函數一般會調用同一種開發者自定義的子函數“_transfer(address sender,address recipient,uint256 amount)”，即執行sender地址向recipient地址轉賬amount數量的代幣操作.

表1 ERC-20代幣標準

本文將transfer和transferFrom函數調用中的程序行為抽象為“_transfer(address from,address to,uint256 amount)”函數行為.

圖1所示為一個代幣買賣漏洞代碼片段：

圖1 代幣買賣漏洞代碼片段

代碼第4行條件分支語句中當sender地址為owner時，執行正常的第5行和第6行轉賬操作；如果sender地址不為owner時，執行第8行和第9行操作，即接收方recipient地址余額僅增加amount的一半.

代幣買賣漏洞是指類似上述代碼的這種情況：實際轉賬數量與用戶所期望數量不相符，收取了高額的轉賬手續費；只能特定賬戶進行轉出，普通用戶只能轉入，不能轉出等.

在DeFi領域，大多數代幣都在去中心化交易所(DEX)中建立了交易對和流動池，在去中心化交易所中用戶可以使用其他價值較高的數字貨幣(例如wBTC,wETH,wBNB,USDT等)來買入這些代幣，一旦這些代幣合約中出現買賣漏洞，買入后無法賣出，或者賣出數量遠低于實際數額，那么用戶的wBTC,wETH,wBNB,USDT等數字貨幣將會鎖在合約中，對用戶的數字資產造成巨額損失.

2.1.2 漏洞分析與漏洞模型

將合約源代碼轉換為字節碼，第5,6,8,9行關于“_balances”的修改存儲操作在字節碼層面的模型特征為

SHA(memory)→SLOAD(key)→ADD(value,amount)→SSTORE(key,new_value)

全局變量_balances在Solidity智能合約中是一個address映射到uint256類型的Mapping數據結構，其在以太坊虛擬機(EVM)底層通過key-value方式進行存儲，value就是映射中對應的uint256數值，key值是將address與全局變量_balances的槽位拼接后進行哈希(SHA3指令)得到的256位數值.SHA3指令對memory中存儲的值進行哈希，SLOAD指令則通過哈希后得到的key值在storage中進行檢索相應的value.對檢索到的value值進行加或減(SUB指令)操作，然后將新的value值存儲(SSTORE指令)到key對應的變量_balance中.

漏洞點在于在SSTORE指令時，任意recipient地址(0地址和sender地址這種特殊地址除外)以及_balance的槽位作為key時，其存儲的value數值不等于原value數值與用戶調用transfer函數時amount的加和.

2.1.3 漏洞檢測方法

本文代幣買賣漏洞檢測方法步驟如圖2所示：

圖2 代幣買賣漏洞檢測方法

圖2中：

1) 對智能合約源代碼進行編譯形成字節碼；

2) 對字節碼和操作碼進行靜態分析，構建基本塊和控制流圖；

3) 通過ERC-20標準函數簽名對第2步靜態分析處理后的contract對象匹配出符合ERC-20標準的代幣合約；

4) 對符合ERC-20標準的代幣合約的balanceOf(address_owner)進行靜態語義分析，確定在執行“_balance[_owner]”時的_balance變量的槽位；

5) 基于符號執行技術，符號化transfer以及transferFrom函數參數，符號化msg.sender地址；

6) 建立約束條件，求解當滿足

balance[_to]==balance[_to]+amount

的msg.sender的值集合情況；

7) 當滿足模型的msg.sender值為有限個，則上報代幣買賣漏洞.

2.2 owner權限轉移漏洞

2.2.1 漏洞產生的原因及危害

在編寫智能合約的過程中，合約的開發者一般會設置一個“owner”值，該值所代表的地址擁有一些特權，如轉賬、函數調用等.如果對“owner”值的修改沒有施加限制條件，那么攻擊者能夠修改該值為自己的地址，從而攻擊者會利用這些特權來攻擊合約并獲取利益.

圖3所示為owner權限轉移漏洞代碼片段：

圖3 owner權限轉移漏洞代碼片段

圖3中第5行表明在構建函數時可以將owner權限設置給合約創建者，同時第12行mint函數附加了修飾符onlyOwner，第9行判斷只有當調用者等于owner時才可以進行第13,14行的mint函數操作.mint函數用于屬主向某個地址鑄造更多的代幣.在第16行setOwner函數可以修改owner變量，但是未附加修飾符onlyOwner，使得任意地址可以調用setOwner函數對owner變量進行修改，從而讓屬主轉變為攻擊者地址，再調用mint函數就可以鑄造大量代幣分發給攻擊者地址.

2.2.2 漏洞分析與漏洞模型

經過調研發現，owner所在的storage槽位一般與onlyOwner修飾符以及構造函數中msg.sender相關.在構造函數中，owner一般由msg.sender或者普通地址類型變量進行初始化.在onlyOwner修飾符中，owner一般被用于與msg.sender值比較，其在字節碼層面的模型特征為

EQ(owner,msg.sender)→ISZERO→JUMPI.

同時從字節碼層面分析，owner權限轉移漏洞模型可以總結為：合約執行過程中存在SSTORE指令，并且SSTORE指令的key值與owner所在的storage槽位相等.

2.2.3 漏洞檢測方法

本文owner權限轉移漏洞檢測方法的步驟如圖4所示：

圖4 owner權限轉移漏洞檢測方法

圖4中：

1) 對智能合約源代碼進行編譯形成字節碼.

2) 對字節碼和操作碼進行靜態分析，構建基本塊和控制流圖.

3) 確定“owner”的存儲位置.詳細過程為：在合約內，一般會對“owner”變量賦值為msg.sender，即合約的創建者，msg.sender由CALLER操作碼壓入EVM棧中，賦值操作由SSTORE操作碼完成.在操作碼序列中尋找CALLER操作碼，CALLER會將msg.sender的值放入棧中，對棧中該數據進行跟蹤.在操作碼序列中尋找SSTORE操作碼，SSTORE操作會從棧中獲取key和value.如果value為msg.sender或者經過AND運算后的20 B變量(一般為address類型變量)，那么key就是“owner”在storage中的存儲位置.同時通過第2步靜態語義分析中尋找的onlyOwner修飾符，對與msg.sender變量比較的全局變量槽位進行捕獲.將上述這2種方式確定的存儲位置記錄下來，取其交集作為owner變量的存儲位置供后續步驟使用.

4) 符號執行，根據步驟3)確定的存儲位置，判斷寫操作的存儲位置是否是該位置.遍歷尋找SSTORE操作碼，SSTORE操作碼會從EVM棧中取出key，判斷key是否與步驟1)中找到的“owner”的存儲位置一致.如果是，則記錄該路徑.

5) 對滿足上述條件的路徑進行約束求解，有解則報告該漏洞.根據當前的約束條件進行求解，如果有解則表明存在任意調用者可以對“owner”的值進行修改，即存在漏洞.

3 漏洞檢測工具的設計與實現

3.1 總體架構

該漏洞檢測模型總體架構如圖5所示，主要包括合約收集、預處理、靜態分析、符號執行和漏洞模型分析5個模塊：

圖5 漏洞檢測模型總體架構

3.2 模塊設計與實現

3.2.1 合約收集模塊

合約收集模塊集成了以太坊infra節點和幣安智能鏈節點，可以通過各種方式對合約源代碼和字節碼進行收集，收集方式包括本地讀取、通過etherscan收集源代碼、通過合約地址收集鏈上字節碼和etherscan源碼及字節碼、通過塊高度區間收集鏈上合約源碼和字節碼等.

同時集成了Ethereum Signature Database[23]的API，可以通過字典查詢的方式對字節碼中的函數簽名進行猜解.

3.2.2 預處理模塊

預處理模塊的主要功能是對輸入的數據進行預處理，包括輸入校驗和數據處理.對于輸入的智能合約solidity源碼數據和EVM字節碼數據，首先校驗其合法性.如果輸入的數據為solidity源碼，則需要使用solc編譯器編譯為EVM字節碼.

預處理模塊執行流程如圖6所示：

圖6 預處理模塊

3.2.3 靜態分析模塊

靜態分析模塊構建基本塊和控制流圖，基本塊只包含順序執行的指令，只有1個入口和1個出口，入口處于基本塊的第1條指令，出口位于基本塊的最后1條指令，中間不出現任何分叉.如果遇到跳轉指令(JUMP或JUMPI)，那么結束當前基本塊，將該指令作為當前基本塊的最后1條指令，并分叉出1個新的基本塊，將JUMPDEST指令作為新基本塊的第1條指令.基本塊B和基本塊C之間存在1條邊則構建形成基本塊控制流.

3.2.4 符號執行模塊

經過預處理模塊得到字節碼數據以及靜態分析處理后的基本塊和控制流圖，模擬EVM執行字節碼，并創建當前的執行狀態，包括Stack，Memory和Storage.每個操作碼指令都對應1個狀態，通過符號執行，可以獲取每個狀態下Stack，Memory和Storage所存儲的內容.然后利用該狀態空間的基本代碼塊和路徑約束條件集，添加約束和路徑集合形成新的符號執行控制流圖.如圖7所示：

圖7 符號執行模塊

3.2.5 漏洞分析模塊

漏洞分析模塊包括代幣買賣漏洞檢測模塊和owner權限轉移漏洞模塊.

漏洞分析模塊通過符號執行以及靜態分析暴露的接口，對EVM的stack，memory，storage，calldata，sender等進行符號化，同時由于SMT對哈希指令SHA3的支持較弱，添加SHA3的符號化組件，在符號化表達式語義層面對涉及SHA3的約束進行求解.最終利用Z3求解器對約束進行求解并上報漏洞，如圖8所示：

圖8 漏洞分析模塊

4 工具測試與實驗分析

4.1 測試環境及樣本類型

為驗證工具的有效性以及性能等指標，本文使用以下硬件和軟件環境進行測試，如表2和表3所示：

表2 硬件環境

表3 軟件環境

本文在以太坊主網的去中心化交易所Uniswap以及幣安智能鏈主網的去中心化交易所PancakeSwap各抽取50個代幣合約作為代幣買賣漏洞的測試樣本，一共100個代幣合約.

本文爬取了以太坊主網區塊高度13 000 000～13 001 000中新部署的合約，共計172個，同時在此樣本基礎上，增加12個與owner權限轉移漏洞相關的智能合約CVE，作為owner權限轉移漏洞的檢測樣本.

代幣買賣漏洞在CVE庫中沒有相應案例，故只使用鏈上交易所合約樣本.

4.2 測試結果與分析

4.2.1 代幣買賣漏洞

對代幣買賣漏洞檢測工具進行測試，結果如表4所示：

表4 代幣買賣漏洞測試結果

由表4可發現，代幣買賣漏洞檢測工具運行用時較長，誤報率較高.

經過分析，運行用時長主要是符號執行耗時過長.

誤報率過高主要原因有2個：一是由于大量代幣合約在轉賬時設置手續費，使得實際轉賬金額與原數額有差別.經粗略統計，對于正常合約手續費設置基本在25%以內.二是因為一些合約設置了白名單和黑名單，限制了一些地址的轉賬權.

以代幣合約DogeKing(幣安智能鏈地址0x641 EC142E67ab213539815f67e4276975c2f8D50)為例，其代碼片段如圖9所示：

圖9 代幣合約DogeKing代碼片段

該合約就是收取手續費類型的代幣合約.第7～18行，合約對不包含在_isExcludedFromFees映射中的地址收取轉賬手續費.由于該合約轉賬手續費不高，其用戶也普遍知曉并遵從其手續費的機制，因此該合約不屬于代幣買賣漏洞.

以檢出的漏洞合約(幣安智能鏈地址0xe9E 3666f64c699529c9d3f9e2c506FF13fDe0E61)為例，對漏洞樣本進行分析，由于該合約未開源，其字節碼反編譯后的代碼片段如圖10所示：

圖10 0xe9漏洞合約反編譯后的代碼片段

在第2～6行、第7～11行、第12～21行，均對用戶轉賬行為進行了限制.第2行的變量unknown1e445a90是一個全局開關，值由屬主控制，當為false時，所有普通用戶才可以轉賬.第7行是一個特權數組，在數組中的地址才可以進行轉賬.第12～21行，全局變量unknown1b355427Address存儲屬主地址，如果轉賬用戶為屬主才允許轉賬.在幣安智能鏈上觀測該合約的交易可以發現，該合約代幣approve函數同樣存在上述類似的惡意限制，balanceOf函數進行了惡意改寫，balanceOf函數代碼片段如圖11所示.

圖11 balanceOf函數代碼片段

在滿足全局開關變量unknown1e445a90為false(第2行所示)、查詢余額的地址為屬主(第3行所示)、查詢余額的地址屬于特權數組(第4行所示)3個條件之一的情況下，才會返回真實余額(第6行所示)，否則所有用戶將返回1個固定值的全局變量(第5行所示).惡意balanceOf函數讓所有普通用戶觀察到自己的地址內有大量代幣，誘使他們通過去中心化交易所進行投資買入，卻無法賣出.該合約屬于有后門的惡意合約.

4.2.2 owner權限轉移漏洞

對owner權限轉移漏洞檢測工具進行測試，結果如表5所示：

表5 owner權限轉移漏洞測試結果

由表5可知，本文工具運行用時較長，誤報率較低，檢出率低.

經過分析，運行用時長主要是符號執行耗時過長，并且由于符號執行中對所有的SSTORE都嘗試進行約束求解，使得時間消耗相較于代幣買賣漏洞的檢測用時高.檢出率低和誤報率低原因一是因為模型針對性強，準確度高，其次是因為OpenZepplin區塊鏈應用標準中規范了訪問控制權限的開發模式，幫助開發者避免一些容易疏忽的權限漏洞.

以檢出的CVE-2021-34273漏洞合約為例，對漏洞樣本進行分析，漏洞合約代碼片段如圖12所示.

圖12 檢出的CVE-2021-34273漏洞合約代碼片段

該合約為ERC-20代幣合約BTC2X(B2X)的一部分，用來初始化合約中的owner值，以及定義限定修飾符onlyOwner，并且可以將ownership轉移給其他地址.

在漏洞合約中使用owner變量來存儲合約擁有者地址，但由于構造函數名的錯誤，合約允許任何人調用owned()函數來修改合約的所有者，存在owner權限漏洞.第4行代碼中，由于owned()函數訪問修飾符為public，從而任何人可以調用該函數修改owner值為自己賬戶的地址.當惡意攻擊者調用該函數修改owner值為自己賬戶的地址后，便可以調用代幣合約中的其他函數來獲利.

5 結 論

針對代幣買賣的后門漏洞以及owner權限轉移漏洞的檢測問題，本文提出了一種源代碼和字節碼層面的自動化檢測方法.通過靜態語義分析與符號執行相結合的技術，對漏洞點進行檢測，并且通過符號執行自動化形成利用路徑.通過在以太坊和幣安智能鏈上主網合約進行測試，發現了新的代幣買賣漏洞合約，通過實驗，與owner權限轉移漏洞相關的CVE也得到自動化的檢測和復現.