17.1引用
Elvira Albert, Jesús Correas, Pablo Gordillo, Guillermo Román-Díez, and Al- bert Rubio. 2019. SAFEVM: A Safety Verifier for Ethereum Smart Contracts. In Proceedings of the 28th ACM SIGSOFT International Symposium on Soft- ware Testing and Analysis (ISSTA ’19), July 15–19, 2019, Beijing, China. ACM, New York, NY, USA, 4 pages. https://doi.org/10.1145/3293882.3338999
17.2摘要
以太坊智能合約是公開的，不可變的和分佈式的，因此，它們很容易因開發人員的編程錯誤而產生漏洞。本文介紹了SAFEVM，這是一種用於以太坊智能合約的驗證工具，它使用了針對C程序的最新驗證引擎。SAFEVM將以太坊智能合約（以Solidity源代碼或編譯的EVM字節碼形式）作為輸入，並可選地使用斷言和要求驗證註釋，並在輸出中生成帶有驗證結果的報告。除了常規安全註釋外，SAFEVM還處理陣列訪問的驗證：它會自動生成SV-COMP驗證聲明，以便C驗證引擎可以證明陣列訪問的安全性。我們使用CPAchecker，SeaHorn和VeryMax作為後端驗證程序，對從etherscan.io（超過24,000個）中提取的所有合同進行了實驗評估。
17.3 SAFEVM概述
每個區塊鏈提供其自己的編程語言來實現智能合約。Solidity是一種Turing完整的語言，是為以太坊平臺編寫智能合約然後被編譯為EVM（以太坊虛擬機）字節碼的最流行的語言。 EVM執行的每條指令都有以太坊指定的相關汽油消耗量。安全性是以太坊的主要關注點，Solidity語言包含面向驗證的功能、聲明和要求，以檢查安全條件或要求並在不滿足安全條件或要求時終止執行。像往常一樣，assert函數可用於驗證目的（例如，檢查不變量），而require函數用於指定前提條件（例如，確保輸入或合同狀態變量的有效條件）。當將Solidity代碼編譯為EVM字節碼時，require條件將轉換為檢查條件和REVERT字節碼是否成立的測試。REVERT終止智能合約的整個執行，恢復狀態，並將所有剩餘的燃料退還給者。如果條件不成立，則使用斷言檢查條件，並調用INVALID字節碼。當執行INVALID時，狀態將被還原，但不會退還任何燃料，因此，其後果比REVERT更為嚴重：除了失去燃料的經濟後果外，唯一提供給交易的信息是燃料不足的錯誤消息。對數組訪問的處理與聲明相同，在訪問數組位置時，生成的EVM字節碼將檢查所訪問的位置是否在數組範圍內，否則執行INVALID字節碼。當分母為零時，除法和相關的字節碼（如MOD，SMOD，ADDMOD，MULMOD）也會導致執行INVALID。
因此，無效的字節碼是實現以太坊智能合約合法化的關鍵，因為它們被斷言違反和多個源操作失誤（例如，越界訪問，零除法）捕獲。 因此，我們對智能合約進行驗證的方法包括將智能合約的EVM字節碼反編譯為帶有ERROR批註的C程序，以使其能夠使用用於驗證C程序的現有工具進行驗證。 從低級EVM開發驗證程序具有以下優勢：（i）有時源代碼不可用（例如，區塊鏈僅存儲字節碼），（ii）在字節碼級別只可見INVALID字節碼，我們可以對上述各種安全問題進行統一處理，（iii）我們的分析適用於可編譯為EVM的任何其他語言（例如Vyper），並且不受源語言的更改或編譯器優化的影響。 幸運的是，有許多開源工具可幫助我們進行反編譯，並且已集成到工具鏈中。
圖1 SAFEVM的主要組件
圖1描繪了SAFEVM的主要組件，如下所示（陰影框是現成的二手系統）：（1）輸入。 SAFEVM採用智能合約，可以選擇帶有斷言並要求驗證註釋。智能合約可以以Solidity源代碼或EVM編譯代碼的形式給出，在後一種情況下，註釋已如上所述被編譯為字節代碼。（2）CFG。以任何一種形式，代碼都以符號形式提供給Oyente執行引擎已被擴展以根據給定的智能合約計算完整的CFG。由於Oyente不處理遞歸函數，因此在此步驟中已將其丟棄。 CFG生成階段未在本文中描述。（3）EthIR。 EthIR 從生成的CFG中將EVM字節碼反編譯為更高級別的基於規則的表示（RBR）。該階段的技術細節未在本文中描述。（4）C + SV-COMP轉換器。我們已將用於遞歸RBR表示的轉換器實現為帶有驗證的抽象Integer C程序（即，所有數據均為Integer類型）。使用SV-COMP格式的註釋。我們尚無法處理的EVM功能（例如按位操作）在轉換中被抽象化了（請參見第四節）。遵循SV-COMP格式，在C程序中將INVALID指令轉換為ERROR註釋。（5）驗證。任何使用SV-COMP註釋的Integer C程序Verification工具都可以用來驗證我們C轉換合同的安全性。我們已經使用三個最先進的C驗證器，CPA檢查器，VeryMax和SeaHorn評估了我們的方法，並且我們處理了它們生成的驗證報告以根據智能合約的功能報告結果。
我們的工具SAFEVM具有龐大的（潛在）用戶群，因為以太坊目前是用於編碼和處理智能合約的最先進的平臺。正如我們將在第五節中描述的那樣，使用SAFEVM，我們已經自動驗證了大約20％的功能的安全性（取決於驗證者），這些功能可能會執行從etherscan.io提取的整個合同（超過24,000個合同）中的INVALID字節碼，並且發現了潛力無法驗證的功能漏洞。
17.4 使用SV-COMP註釋轉換成C
作為激勵示例，我們使用實現了稱為SmartBillions的彩票系統的Solidity合同（可從https://smartbillions.com/獲得）。我們說明了對其內部功能commitDividend的安全性驗證，該函數將剩餘的紅利提交給用戶wh。通過從名稱中刪除元音，我們縮短了變量名稱。
我們翻譯器的起點是EthIR生產的RBR。 RBR由一組規則組成，這些規則包含字節碼指令的反編譯版本（例如LOAD和STORE被反編譯ssignments），其規則調用的結構是從Oyente生成的CFG中獲得的。 RBR可能包含兩種規則：稱為blockX的指令序列和名為jumpX的條件跳轉規則，其第一條指令是用於在函數定義的規則之間進行選擇的布爾條件。本節的其餘部分說明了從RBR到抽象Integer C程序的轉換的四個主要階段。
（1）C函數：對於RBR中的每個非遞歸規則定義，我們的轉換都將產生一個C函數，該函數沒有返回void的參數。循環產生的遞歸規則將轉換為迭代代碼。對於轉換的這一部分，我們根據CFG計算SCC，並通過goto指令對檢測到的循環進行建模。
（2）變量的類型：基本類型，有符號和無符號數據類型存儲在EVM字節碼中的無類型256位字中，並且字節碼不包含有關變量實際類型的信息。此外，除了少數特定的簽名操作（SLT，SGT，SIGNEXTEND，SDIV和SMOD）以外，大多數EVM操作不會在其中進行區分。由於驗證者的行為有所不同溢出，我們的翻譯允許用戶選擇（通過標誌）是在C程序中聲明所有變量的類型為int還是聲明為unsigned int的類型（將其轉換為int）用於特定於標誌的操作。
（3）變量定義：為了在驗證過程中在它們的範圍內啟用推理，SAFEVM按如下方式在C程序中轉換它們：（i）在展平執行棧時，我們將棧變量聲明為全局C變量。使它們可用於所有C函數。這些變量不需要初始化，因為它們採用程序代碼中的值。 （ii）將局部變量定義為全局C變量因為合同的功能可能會轉換為多個C函數，並且所有這些都需要訪問局部數據。它們在對應於首先使用它們的塊的功能的開始處進行初始化。 （iii）狀態變量也被轉換為所有函數均可訪問的全局變量，並且由於在驗證函數時其值未知，因此使用_VERIFIERnondet_int對其進行初始化； （iv）函數輸入參數也定義為全局變量。
（4）SV-COMP註釋：通過保證C轉換代碼中NVALID操作的不可達性，在SAFEVM中完成對以太坊智能合約的驗證。跟隨SV-COMP規則，我們將INVALID操作轉換為對VERIFIERerror函數的調用。
17.5 實驗評估
SAFEVM的所有組件（除C驗證程序外）均以Python實現，並且是開源的。 SAFEVM接受以Solidity最高版本0.4.25編寫的智能合約以及以太坊虛擬機v1.8.18的字節碼。 本節報告使用SAFEVM和CPAchecker，SeaHorn和VeryMax作為驗證後端的實驗評估結果。具體評估結果數據可以閱讀原文獲取。
從評估數據看來，我們認為儘管有很多提高精度的空間，但我們的實驗評估結果令人鼓舞：我們已經驗證了安全性。 通過使用最新的驗證程序，大約20％的功能可能會完全自動達到INVALID的INVALID字節碼。
17.6 結論
據我們所知，SAFEVM是第一個使用為C程序開發的現有驗證引擎來驗證低級EVM代碼的工具。這為驗證C程序而開發的先進技術的適用性打開了大門，這些先進技術可用於對智能合約進行編碼的新語言。儘管我們的工具仍處於原型階段，但它提供了轉換方法的概念驗證，並且我們認為它為構建EVM智能合約的驗證工具提供了有希望的基礎。我們打算在將來的工作中改進的一些方面是處理存儲在內存中的數據，因為一旦內存上進行存儲操作，SAFEVM就會使用EthIR組件將其抽象化。為EVM智能合約開發內存分析對於驗證準確性至關重要。我們還旨在將來處理EVM字節碼中廣泛使用的按位操作。數組和地圖的高級推理（以太坊智能合約中唯一可用的數據結構）也可以添加到框架中，以提高準確性。這也需要反編譯方面的進一步工作。同樣，在反編譯期間學習有關變量類型的信息將對驗證過程的準確性產生影響。
本文由南京大學軟件學院2016級本科生曹佳瑋轉述。
閱讀更多 慕測科技 的文章
