Luu L, Chu D H, Olickel H, et al. Making Smart Contracts Smarter[C]// Acm Sigsac Conference on Computer & Communications Security. 2016.
論文摘要：
加密貨幣在稱為區塊鏈的分散數據結構中記錄交易。兩種最流行的加密貨幣，即比特幣和以太坊，它們支持對處理交易的規則或腳本進行編碼的功能。此功能已經發展為實際形成智能合約或在區塊鏈上運行的完整程序的想法。 最近，以太坊的智能合約系統已經穩步採用，支持數以萬計的合約，持有價值數百萬美元的虛擬硬幣。
本文研究了基於以太坊的智能合約在加密貨幣等開放分佈式網絡中運行的安全性。我們引入了幾個新的安全問題，其中攻擊者可以操縱智能合約執行來獲取利潤。這些錯誤表明在理解底層平臺的分佈式語義方面存在細微的差距。作為一種改進，我們提出了增強以太坊操作語義的方法，以減少合同的脆弱性。對於為現有以太坊系統編寫合同的開發人員，我們構建一個名為Oyente的符號執行工具，以發現潛在的安全漏洞。在現有的19366份以太坊合同中，Oyente將其中8833份標為易受攻擊，包括導致2016年6月損失6000萬美元的TheDAO漏洞。我們還討論了幾個案例研究中其他攻擊的嚴重性，這些案例研究具有可用的源代碼，並確認了主要以太坊網絡中的攻擊（僅針對我們的帳戶）。
技術介紹：
在本文中，我們記錄了以太坊智能合約的幾個新安全漏洞（交易訂購依賴
、時間戳依賴性、錯誤處理的例外情況和可重入漏洞），並舉例說明了每個問題的實際實例。這些安全漏洞使合同容易被多方（包括礦工和合同用戶）濫用。我們認為這些缺陷在實踐中出現是因為合同編寫者對底層執行語義的假設與智能合約系統的實際語義之間存在語義差異。具體來說，我們將展示不同的各方如何利用具有不同輸出狀態的合同，具體取決於事務的順序和輸入塊時間戳。據我們所知，這些語義差距以前沒有被確定過。我們還記錄了其他嚴重但已知的問題，例如不正確處理的中止/異常和邏輯缺陷。以前的工作在概念上進行了討論，通常用簡單的自構建實例[1]。在我們的工作中，我們研究了它們對成千上萬的現實合同的影響，展示了這些漏洞如何被用來破壞或竊取良性用戶的硬幣。
更重要的是，我們的工作強調智能合約語義中的微妙和/或缺失的抽象，導致開發人員產生錯誤的安全感。我們建議改進以太坊的協議，不需要更改現有的智能合約。但是，此類解決方案確實需要網絡中的所有客戶端進行升級，因此存在無法看到實際部署的風險。如果這樣的要求是不可接受的，我們提供了一個名為Oyente的工具，供用戶在部署前緩解中檢測錯誤。 Oyente是一個專門用於分析以太坊智能合約的符號執行工具。它遵循以太坊智能合約的執行模型[2]，並直接與以太坊虛擬機（EVM）字節碼一起使用，無需訪問高級表示（例如，Solidity [3]，Serpent [4]）。這種設計選擇至關重要，因為以太坊區塊鏈只存儲合同的EVM字節代碼，而不是它們的來源。 Oyente是開源的，很快就會從我們的項目頁面上公開使用[5]。
Oyente工具來幫助：（1）開發人員編寫更好的合同; （2）用戶避免調用有問題的合同。 重要的是，其他分析也可以作為獨立插件實現，而不會干擾我們現有的功能。 例如，Oyente的直接擴展是計算更精確的合同最壞情況氣體消耗估算。
我們的分析工具基於符號執行[6]。符號執行將程序變量的值表示為輸入符號值的符號表達式。每個符號路徑都有一個路徑條件，它是通過累積約束構建的符號輸入的公式。那些輸入必須滿足，以便執行遵循該路徑。 如果路徑條件不可滿足，則路徑是不可行的。 否則，路徑是可行的。
我們選擇符號執行，因為它可以逐個路徑地靜態推理程序。 一方面，這優於動態測試，這是關於程序輸入的原因。對於以太坊，動態測試甚至需要更多的努力來模擬執行環境。 例如，為了檢測事務排序依賴性，我們必須比較不同執行路徑的交錯結果。考慮到區塊鏈行為的非確定性和複雜性，很難通過動態測試來解決這個問題。
另一方面，通過一次推理一條路徑，與使用靜態汙點分析或一般數據流分析的傳統方法相比，符號執行可以實現更好的精度（或更少的誤報）。 在這些方法中，抽象程序狀態經常被合併，承認從未在真實執行中發生的狀態，並最終導致高誤報。
圖1：概述Oyente的體系結構。主要部件位於虛線區域內。陰影框是公開的。
設計概述
圖1描繪了Oyente的架構概述。它需要兩個輸入，包括要分析的合同的字節碼和當前的以太坊全局狀態。 它回答合同是否存在任何安全問題（例如，TOD，時間戳依賴性，錯誤處理的異常），向用戶輸出“有問題”的符號路徑。 我們工具的一個副產品是合同字節碼的控制流圖（CFG）。 我們計劃在未來Oyente將能夠作為交互式調試器工作，因此我們將CFG和有問題的路徑提供給圖形可視化工具.
字節碼在區塊鏈上公開，Oyente解釋EVM指令集，以便將指令忠實地映射到約束，即位級精度。以太坊全局狀態提供契約變量的初始化（或當前）值，從而實現更精確的分析。包括值、消息調用數據在內的所有其他變量都被視為輸入符號值。
Oyente採用模塊化設計。 它由四個主要組件組成，即CFG Builder，Explorer，Core Analysis和Validator。 CFG Builder構造契約的控制流圖，其中節點是基本執行塊，邊表示塊之間的執行跳轉。 Explorer是我們的主要模塊，象徵性地執行合同。 然後將Explorer的輸出提供給Core Analysis，我們在其中實現我們的邏輯以針對第3節中確定的漏洞。最後，Validator在向用戶報告之前過濾掉一些誤報.
本文作出以下貢獻：
- 我們在以太坊智能合約中記錄了幾類新的安全漏洞。
- 我們將以太坊智能合約的語義形式化，並提出建議作為記錄錯誤的解決方案。
- 我們提供Oyente，一種象徵性執行工具，用於分析以太坊智能合約以檢測錯誤。
- 我們在真正的以太坊智能合約上運行Oyente並確認真實以太坊網絡中的攻擊。
參考文獻：
[1] Kevin Delmolino, Mitchell Arnett, Ahmed Kosba,Andrew Miller, and Elaine Shi. Step by step towards creating a safe smart contract: Lessons and insights from a cryptocurrency lab. Cryptology ePrint Archive,Report 2015/460, 2015. http://eprint.iacr.org/.
[2] Gavin Wood. Ethereum: A secure decentralized generalised transaction ledger.
http://gavwood.com/paper.pdf, 2014.
[3] Ethereum Foundation. The solidity contract-oriented programming language.
https://github.com/ethereum/solidity
[4] Ethereum Foundation. The serpent contract-oriented programming language.
https://github.com/ethereum/serpent
[5] Oyente project page.https://www.comp.nus.edu.sg/˜loiluu/oyente.html.
[6] James C. King. Symbolic execution and program testing. Commun. ACM, 19(7):385–394.
致謝
本文由南京大學軟件學院2019級碩士生劉芳瀟翻譯轉述
閱讀更多 慕測科技 的文章
