2019-11-05 06:15:00 慕測科技

2.1 引用

Wang, Haijun, et al. "Vultron: catching vulnerable smart contracts once and for all." Proceedings of the 41st International Conference on Software Engineering: New Ideas and Emerging Results. IEEE Press, 2019.

2.2 摘要

儘管涉及高風險，但智能合約往往以無紀律的方式發展。漏洞的存在損害了智能合約的安全性和可靠性，並危及參與者對其正在進行的業務的信任。現有的漏洞檢測技術通常是逐個設計的，因此難以概括。在本文中，我們設計了檢測易受攻擊的智能合約的一般原則。我們的主要觀點是，幾乎所有與交易相關的漏洞都是由於實際轉移金額與合同內部簿記所反映的金額不匹配所致。基於此，我們提出了一種精確且普遍適用的技術 VULTRON，它可以檢測由於各種類型的對抗攻擊而導致的不規範交易。我們還報告了將我們的技術應用於實際案例研究的初步結果。

2.3 技術介紹

由於許多智能合約以無規律的方式開發，導致攻擊者容易利用漏洞，因此這種攻擊成為可能。一個臭名昭著的例子是“DAO”攻擊，即攻擊者從“DAO”合同中偷走了超過 350 萬以太幣（當時相當於約 4,500 萬美元）。從那以後，人們進行了大量嘗試來檢測智能合約中的漏洞。然而，這些技術都遵循逐案的方式：合同計劃被分析並與之前觀察到的攻擊模式相匹配。因此，這些技術的精確度和召回率在很大程度上取決於模式的指定程度以及模式集合的綜合程度。ContractFuzzer 提出了在合同計劃中觀察到的七種特定模式，以檢測七種漏洞。由於收集的模式是有限的並且它們在句法層面建模，因此分析既有假陰性也有誤報。

為了克服這些問題，我們的主要觀點是，幾乎所有現有的漏洞模式（在語法層面定義）都可以追溯（語義上）到交易中實際轉移金額與合同內部反映的金額之間的不匹配。基於此，我們提出了一種精確且通用的智能合約漏洞檢測技術 VULTRON，它可以深入研究問題的根源。VULTRON 的本質是構建一個能夠有效區分不規則事務（通常是惡意攻擊的結果）與正常事務的 oracle。我們的 oracle 足以覆蓋之前報告的漏洞，而不受任何特定智能合約編程語言或區塊鏈技術的限制。我們在以太坊平臺上展示了我們的方法，而且，我們的方法背後的原理可以很容易地在其他平臺上進行調整和實現。擬議的 oracle 改進並實現了廣泛的下游分析技術，包括靜態分析，如符號執行，程序驗證和動態技術（如測試和模糊測試）。

2.3.1漏洞檢測的oracle方法

智能合約中的漏洞通常是由實現與預期語義之間的不一致引起的。與交易相關的漏洞可能（其中大部分已經被利用）進行攻擊，例如從易受攻擊的合同中竊取資金。本文我們將討論檢測智能合約中與交易相關的漏洞的基本原則和具體挑戰。

現在我們討論將提議的不變量實現為 oracle 的自身工具所涉及的挑戰以及用於檢測由於漏洞導致的不規則事務的自動化工具。兩個不變量的關鍵因素是幾乎所有在多方之間執行有意義交易的合約都包含這樣一個變量，通常帶有名稱餘額或 balanceOf。有些合同沒有簿記變量，例如King of the Ether。在這些情況下，我們的分析可以插入 ghost 變量及其相應的更新。簿記變量既可以由用戶給出，也可以作為我們方法的輸入，或者使用汙點分析自動識別。我們的想法是首先執行幾個正常的務並觀察合同程序中的所有全局變量如何變化，以找到一個總是與執行的事務匹配的變量。處理非貨幣資產。某些合同的簿記餘額可能不直接指向加密貨幣。在符合 ERC20 的合同中通常就是這種情況。在這些合同中，參與者的數字資產反映在可用令牌而非以太幣的數量上。這些非貨幣資產可以通過乘以其價格轉換為以太幣。所述資產的當前價格存儲在某個位置（例如，可變價格），其可以用用於定位簿記變量的類似技術來識別。驗證不變量。然後將不變量轉換為程序斷言，然後靜態動態驗證。在翻譯中也應考慮交易的燃氣消耗，這不包括在我們的合同模型和不變量中。斷言可以插入到編譯的以太坊虛擬機（EVM）字節碼中，在每個函數的末尾，然後可以通過現有的驗證工具進行檢查。或者，我們可以檢測 EVM 本身以在運行時強制執行不變量。即使部署的合同計劃容易受到攻擊，這也可以防止不正常的交易發生。

我們已經為我們的方法實現了原型，並在 Truffle Suite 上進行了測試。然後，我們回顧以前報告的以太坊智能合約的漏洞，並展示我們的方法如何幫助檢測並重入這些漏洞。事務的原子性和順序性可能讓程序員相信，當調用非遞歸函數時，它不能在終止之前重新進入。

2.3.2潛在的應用

在智能合約上應用傳統安全分析技術（例如，測試，驗證，監控和自動修復）時的根本困難是缺乏通用測試指導。這再次歸因於智能合約運作的特殊方式，它們不會崩潰，並且在違規情況下可以默默地恢復執行。我們將描述 VULTRON 在應用於智能合約時如何啟用和改進這些技術。

測試和驗證。

測試和模糊測試是用於檢測安全漏洞的重要動態技術，這兩種技術都需要測試 oracle 來確定程序是根據預期行為執行。類似地，程序驗證依賴於一組給定的屬性來檢查程序是否與屬性對齊。為通用計算機程序提供這樣的指導和屬性可能很麻煩並且需要大量的專業知識。對於智能合約，我們提出的不變量可以很容易地轉換為 oracles 和斷言，這使得下游分析無需額外的努力。我們還設想，當配備 VULTRON 時，模糊測試可能會發現新類型的攻擊，因為我們的測試指導是通用的，並深入到與事務相關的漏洞的根源。

監控和維護。

我們可以通過適當檢查來檢測 EVM，以便對合同執行進行運行時監控。在執行期間檢測到故障時，我們可能會阻止正在進行的交易，甚至可以對易受攻擊的合同進行修復。VULTRON 產生的信息可用於指導自動程序修復技術為檢測到的漏洞構建補丁。

超越漏洞。

VULTRON 的未來不僅僅是檢測弱勢合同。有另一種類型的合同是故意設計的，以利用參與者。我們將它們歸類為惡意合同（有時在文獻中稱為不公平合同）。儘管此類合同是公開的，但大多數參與者無法仔細檢查和分析合同代碼，以便提前發現所有惡意行為。這種合同的共同之處在於，某些參與者（通常是合同所有者）比其他參與者具有顯著的優勢，而這背後隱藏著晦澀的語言語法和合同邏輯。VULTRON 可以擴展到考慮公平性方面，這將智能合約的分析帶入一個全新的層面。