引用
Hildenbrandt E, Saxena M, Zhu X, et al. Kevm: A complete semantics of the ethereum virtual machine[R]. 2017.
16.1摘要
分佈式系統和應用密碼學社區感興趣的一個發展領域是智能合約——它是通過區塊鏈來同步其狀態的自執行性金融工具。以太坊（Ethereum）就是這樣一種智能合約系統，目前已得到廣泛的實際採用，以太坊已經發展成為可確保約300億美元幣值和每日超過300,000筆交易的系統。
不幸的是，這些技術的興起被一系列重複的安全漏洞和引人注目的合同失敗案例所破壞。為了解決這些問題，以太坊社區已經開展形式驗證和程序分析的研究。儘管如此，目前尚不存在關於EVM（以太坊虛擬機）正式、嚴格、全面和可執行的語義學，使得無法基於語義來構建研究工具。
在這項工作中，我們介紹了KEVM，EVM的第一個完全可執行的形式語義，即執行智能合約的字節碼語言。我們在可執行語義的框架K中創建此語義。我們的語義不僅通過了官方提供用於EVM實現的40,683個測試壓力測試套件，而且還揭示了基於現有的EVM語義的紙上形式化的歧義和潛在的錯誤源，這些特性使KEVM成為理想的正式可參考實現。
我們繼續為EVM合約尋求一種語義優先的形式驗證方法，並通過使用KEVM驗證示例智能合約的算術運算和第二個合約中的令牌傳遞函數的正確運算，來證明其實用性。我們證明了我們的方法是可行的，並且在計算上沒有限制。我們希望我們的工作可以為以太坊開發各種有用的正式衍生工具提供基礎，包括模型檢查器，經認證的編譯器和程序等效檢查器。
16.2介紹
比特幣是早期的加密貨幣之一，在實踐和學術上都取得了成功，因此引發了人們對區塊鏈技術潛在應用的廣泛搜索。以太坊就是這樣一個系統，它使用準Turing完整編程語言實現了通用的複製“世界計算機”。以太坊的一個目標是允許開發在區塊鏈交易中執行的任意應用程序和腳本，使用區塊鏈以一種可以被系統中任何參與者驗證的方式在全球範圍內同步其狀態。以太坊系統中的參與者和合約以稱為Ether的分佈式貨幣進行交易。以太坊網絡上的賬戶可以與基於虛擬機的語言（稱為EVM）關聯。這些程序稱為“智能合約”，在交易調用帳戶時執行。
智能合約的日益普及已導致對其安全性的審查越來越嚴格。但是，智能合約中存在許多細微的錯誤，從交易順序依賴到處理不當的異常。EVM支持合同間執行，從而使豐富的網絡動態成為可能，因為合同將其計算的一部分卸載到其他合同中，這進一步使獲得這些合同的嚴格保證的問題變得更加複雜。
為了應對高保證要求和豐富的對抗模型之間的這種複雜混合，以太坊基金會特別呼籲“以人機可讀、可執行的形式對EVM進行規範化”，“以EVM字節碼或Solidity開發經過正式驗證的庫”和“用小語言開發經過正式驗證的編譯器”。在我們的工作中，直接處理了前兩個問題，併為第三個問題打下基礎。
16.3EVM的K語義（KEVM）
16.3.1邏輯語義結構
KEVM在邏輯上分為三個模塊，每個模塊涉及不同級別的語義。
- data.k：低級EVM客戶端代碼中使用的數據表示形式及其關聯的數據結構，以及它們根據K本機數據結構的定義。
- evm.k：K中的EVM語義的形式化，包括各種操作碼的執行語義、世界和網絡狀態、氣體語義以及在執行過程中可能發生的各種錯誤。
- ethereum.k：額外的運行EVM代碼的執行環境/驅動程序，具有解析用於測試參考EVM實現的JSON測試文件的模式。
在本節的其餘部分，我們將重點關注evm.k，並描述如何將一些重要或困難的EVM操作形式化為K規則。
16.3.2EVM執行狀態（配置）
在K中，使用一種配置來指定系統的潛在狀態，以便轉換規則可以輕鬆訪問和更新該狀態的不同組件。 每個過渡規則代表一個執行步驟，並將一個配置重寫為另一個。 EVM的狀態分為兩個部分：活動交易的狀態（執行智能合約）和整個網絡的狀態（帳戶信息）。 為了反映這一點，我們的配置包括兩部分——執行子狀態和網絡狀態。
執行子狀態：每次執行EVM都有一個關聯的帳戶，一個程序計數器，當前程序，一個字堆棧和一個易失性本地內存。
網絡狀態：區塊鏈對應於一組帳戶狀態。
16.3.3EVM硬件
KEVM以當前操作碼上的一條命令管道的形式提供EVM執行週期，每條命令都會更新狀態的某些部分。 在此過程中，可能會引發異常，並且在捕獲異常時可能會還原狀態。 在這裡，我們描述了隨後定義EVM的“硬件”。
具體“異常”的表現和相應的控制流、處理方式可以閱讀原文獲取。
16.3.4EVM程序和執行
EVM操作碼：EVM程序是與EVM操作碼相對應的字節序列；每個操作碼都有一個英文助記符。
自變量加載：執行操作碼時，將從中解壓縮正確數量的自變量。
執行週期：EVM的執行週期首先對異常狀態進行多次檢查，然後實際執行狀態更新。總體而言，它包括三個宏步驟：
- 在給定當前狀態的情況下，檢查操作碼是否異常。
- 執行與操作相關的狀態更新。
- 將程序計數器遞增到給定運算符的正確值。
燃料（gas）語義：將#exec運算符轉換為兩個連續的狀態更新。 首先，應用#gas更新，然後應用對執行狀態的更新。 由於在EVM模型中計算和內存都會產生成本，因此，為了計算#gas，我們將計算由於執行導致的內在氣體，再計算內存消耗成本。
操作碼語義：最後，扣除費用後，我們準備讓操作碼在worldstate上執行。 運算符#exec將操作碼直接放在單元格的前面，並加載了中的參數。
請注意，我們利用了K的配置抽象，它允許每個規則僅指定與其操作相關的配置部分。 正如我們所展示的，這使我們的規則簡潔，易於閱讀，並精確且專有地捕獲了它們定義的相關計算的語義性質。 這也使語義更新/維護更加簡單。單元結構的變化只能影響提及該單元的規則。
16.4語義評估
為了評估我們的語義，我們專注於測量正確性、性能和可擴展性。
16.4.1正確性和性能
我們將KEVM的具體評估重點放在以太坊基金會發布的官方VMTests測試套件上。 EVM的先前語義工作，包括當前唯一可用的可執行語義，已使用該測試套件作為語義完整性的基準。該測試套件包含40,683個測試，KEVM通過了所有格式良好的測試。下表顯示了KEVM、Lem語義和以太坊基金會分配的C ++參考實現之間的性能比較。通過與C ++參考實現進行比較，我們展示了使用KEVM形式語義進行原型設計，開發和測試套件評估的可行性。所有執行時間均以完整的CPU時間給出。
通過使用功能強大的硬件，進一步改進了功能；利用測試固有的並行性和為持續集成（CI）建造的機器，我們能夠在7分鐘內通過KEVM運行完整的測試套件（包括壓力測試）（不將壓力測試的時間縮短至3分鐘） 。這將KEVM定位於高保證CI環境的可行性。用於語言規範的相同語義可以合理地用於快速測試。我們相信這些有希望的經驗結果支持KEVM的長期願景：交易執行時間的中位數不到40毫秒，並且性能接近本機參考實現，因此我們的語義理論上能夠每天處理單筆數百萬筆交易線程商品硬件，高於以太坊網絡當前的每日交易量。我們認為，這些結果證實了以太坊的正式參考客戶的未來工作方向，其中派生的KEVM解釋器可以實時處理以太坊交易，為需要它的用戶提供最大可能的保證，並補充為性能而設計的現有實現。除了在開發/原型製作過程中運行測試之外，從我們的語義中衍生的其他工具還可以用於調試EVM和以EVM編寫的智能合約中的新功能，以及用於智能合約的形式分析。
16.4.2可擴展性
我們在設計語義時考慮了可擴展性。通過異常和條件分支提供控制流的簡單命令式語言使我們可以添加更多基元來擴展KEVM。為了在語義的執行中具有更大的靈活性，我們在一個額外的單元格上將執行參數化。當前支持三種模式：NORMAL執行，VMTESTS執行和GASANALYZE模式。
16.5衍生分析工具
開發用於K定義的形式化分析工具可以通過以下兩種方式之一進行：設計和實現獨立於語言的分析工具，該工具可以處理所有K定義，或者使用執行分析的執行驅動程序/監視器來擴展現有的語義。在本節中，我們將介紹直接和自動地從形式語義派生的兩個工具：KEVM語義調試器和KEVM程序驗證器。
16.5.1語義調試器
在命令中添加--debugger選項，可將用戶放入KDebug shell。在此Shell中，許多調試命令向用戶公開，包括step，peek和back。給定編程語言的語義，這些命令可用於手動探索目標程序的執行。還要注意，語義調試器只是K符號執行引擎的包裝，使它能夠處理符號狀態以及具體狀態。我們的KEVM調試器在定義EVM的語義方面被證明非常有用，因為當測試失敗時，調試器可以逐步執行其相關部分以精確定位故障。既然語義已經完成並通過了測試，調試器仍然可以通過逐步執行各個EVM程序來分析各個EVM程序，除提供具體調試器提供的傳統狀態信息外，還提供豐富的語義狀態信息。這可以用來確保EVM程序的行為，甚至可以與傳統的調試工具集成在一起，以進一步擴展調試環境。
16.5.2程序驗證
為K開發的一種特別有用的形式分析工具是可達性邏輯證明。 該證明接受K定義和一組邏輯可達性證明作為輸入作為證明。然後，證明將假設語義，嘗試在語言的執行空間上自動證明可達性定理。
16.6結論
本文的主要貢獻如下：
- K中的EVM語義：我們在K框架中定義了形式上嚴格的EVM語義的可執行實例，涵蓋了所有EVM指令。
- EVM參考解釋器：使用我們的形式語義，我們自動生成一個能夠執行EVM事務並相應更新EVM世界狀態的EVM參考解釋器。
- EVM程序驗證程序：我們使用上述內容創建了程序驗證程序，並演示了根據規範對示例EVM程序的完整驗證。
- 統一的工具集：以太坊生態系統存在許多軟件分析工具，每個軟件分析工具都對自己的EVM模型和語義進行編碼，他們都可以從我們的單一形式參考語義自動生成，從而減少由不同模型引起的工具錯誤的可能性。
所有這些工作都是開源的，並在https://github.com/kframework/evm-semantics上提供，我們希望以太坊社區將採用我們的方法來制定更嚴格，更安全的合同。
本文由南京大學軟件學院2016級本科生曹佳瑋轉述
閱讀更多 慕測科技 的文章
