為什么說形式驗證不是測試安全性的完整解決方案

時間：2020-05-26 08:12:01

關(guān)鍵字：智能合約測試 NI SMT

手機看文章

掃描二維碼
隨時隨地手機看文章

[導(dǎo)讀] 我們相信基于代理的仿真可以幫助分析智能合約和協(xié)議行為。但也存在其他方法，比如形式驗證。形式驗證使邏輯保證比模擬的統(tǒng)計保證更強。在回答我們關(guān)心的安全問題方面，它是否優(yōu)于激勵模擬？在這篇文章中，我們

我們相信基于代理的仿真可以幫助分析智能合約和協(xié)議行為。但也存在其他方法，比如形式驗證。形式驗證使邏輯保證比模擬的統(tǒng)計保證更強。在回答我們關(guān)心的安全問題方面，它是否優(yōu)于激勵模擬？在這篇文章中，我們探討了形式化驗證，并認為它是對模擬的有力補充。

概述

形式驗證可以提供對智能合約邏輯和安全性的獨特見解。然而，當試圖對一份智能合約的財務(wù)結(jié)果進行陳述時，形式是不夠的。

基于代理的模擬允許一組模擬代理與合約交互。們的目標是應(yīng)用形式驗證技術(shù)來自動發(fā)現(xiàn)Uniswap交換上的有效合約操作，并分析一系列交易。

使用代理的目的有兩方面：它允許我們預(yù)測協(xié)議設(shè)計階段的實際使用，并支持在實現(xiàn)階段進行驗證。代理模擬允許我們預(yù)測真實用戶與合約交互時的行為。

后續(xù)的博客文章將展示如何在激勵模擬中使用更有效的隨機技術(shù)來獲得關(guān)于Uniswap的一些見解。

第1部分。Uniswap合約的高級概覽

Uniswap exchange是一組智能合約，允許任何人在不向訂單簿提交訂單的情況下交易以太幣和ERC20代幣。單個Uniswap交換合約支持特定的以太幣/ERC20代幣，任何人都可以使用Uniswap合約創(chuàng)建新的代幣對。一旦交易所成立，它就會自主運作：

· 流動性的創(chuàng)造。流動資金提供者將首先按當前匯率提供以太幣和代幣?？梢栽谌魏螘r候添加/刪除更多。

· 交易。然后，市場參與者可以直接使用Uniswap交易所合同進行交易。

· 定價算法。給定交易的價格是使用“常數(shù)產(chǎn)品做市商”模型自動確定的。在給定的貿(mào)易期間，Uniswap將設(shè)置價格，以便保存產(chǎn)品（x * y = k）的以太幣量和給定的代幣。

· 流動性的費用。小額費用被征收并分配給流動性提供者。

第2部分。如何測試區(qū)塊鏈系統(tǒng)的安全性

要想知道Uniswap這樣的系統(tǒng)是否安全，我們需要回答兩個問題：

· 正確性。代碼是否遵循我們預(yù)期的模型（作為規(guī)范或其他形式編寫）？

· 有效性。我們想要的模型會激勵我們想要的行為嗎？

形式驗證只對前者有一些幫助，而對后者幾乎沒有幫助。像“我們應(yīng)該如何設(shè)置費率”這樣的問題根本無法通過形式驗證來回答。

第3部分。Uniswap智能合約的形式驗證歷史

形式驗證

許多項目都嘗試使用形式驗證技術(shù)來證明他們的合約是正確的。對于相對簡單的智能合約，這是非?？尚械?。形式驗證和程序分析技術(shù)可以確定代碼是否遵循給定的規(guī)范，而且常常會出現(xiàn)致命的反例。

之前的工作

Uniswap現(xiàn)有的輕量級形式驗證就是使用這些技術(shù)可以實現(xiàn)的一個很好的例子。利用KEVM框架驗證了做市商（x * y = k）模型及其通過addLiquidity、removeliquity、ethToTokenSwapInput和ethToTokenSwapOutput的實現(xiàn)。假設(shè)現(xiàn)有的ERC20合約“表現(xiàn)良好”。

在共識系統(tǒng)調(diào)查公司（consensus sys Diligence）的后續(xù)審計中，該團隊能夠推斷出如果打破這一假設(shè)會發(fā)生什么。他們發(fā)現(xiàn)，ERC20代幣的惡意實現(xiàn)可以用來欺騙市場參與者，讓攻擊者重新進入Uniswap合約，以同樣的成本消耗更多的資金。

原則上，可以將此擴展規(guī)范捕獲為代碼模板。可以表示和調(diào)用一個半ERC20兼容的合約（相同的接口，但不一定是ERC20行為），并嘗試使用形式驗證來發(fā)現(xiàn)攻擊。在實踐中，這使得形式驗證問題在計算上更加復(fù)雜，因為當用于發(fā)現(xiàn)任意程序時，底層SMT解決程序中的分支會增加。這種技術(shù)有時被稱為“程序綜合”。微軟研究院的這項調(diào)查是了解更多信息的良好起點。

這些挑戰(zhàn)說明了與形式驗證（包括程序綜合）相關(guān)的另外兩個限制：

· 完整的規(guī)范在編寫和表達方面可能具有挑戰(zhàn)性。

· 目前的形式驗證器只適用于簡單的合約和簡單的規(guī)范。

第4部分。我們?nèi)绾螒?yīng)用形式驗證

制定問題

為了測試合約在一組代理的影響下的行為，我們首先嘗試使用符號分析將其應(yīng)用于自動化操作發(fā)現(xiàn)。符號分析將代碼轉(zhuǎn)換成一組可以由SMT求解器求解的公式。SMT求解器是SAT求解器的擴展，它超越了布爾公式（對簡單命題進行陳述）到包含inte的公式

符號分析將代碼轉(zhuǎn)換成一組可以由SMT求解器求解的公式。SMT求解器是SAT求解器的擴展，它超越了布爾公式（對簡單命題進行陳述），涉及整數(shù)、位向量、數(shù)組和編程中常見的其他數(shù)據(jù)形式的公式。

一種看待符號分析的簡單方法是，它可以被用來正式指定一個關(guān)于給定的智能合約的假設(shè)，證明假設(shè)為真，或者生成一個反例。

例如，在形式驗證中，假設(shè)通常是關(guān)于合約的斷言，例如，“double函數(shù)返回的值總是偶數(shù)”。

pragma solidity ^0.5.1

contract Doubler {

function double（uint x） pure public returns （uint） {

uint y = 2 * x;

require （y % 2 == 0）; // This asserTIon could be checked via FV

return y;

}

我們正在尋找在某些交易集中給定斷言是否為true的驗證。

為了使用符號分析進行操作發(fā)現(xiàn)，我們設(shè)置了以下假設(shè)：“Uniswap合約不支持有效的交易”。如果這被證明是錯誤的，那么反例將是生成有效合約交易的一組輸入。

具有象征意義的分析

我們提供了一個黑盒符號解釋器，其中包含一個經(jīng)過修改的Uniswap交換合約、一個可用資金支持的一條縫帳戶代理池和一組受限制的操作（與合約功能匹配）。在兩個測試鏈上重播完成的操作——一致測試鏈和一個純EVM副本（為了保存對契約存儲的更改而進行維護）。目標是發(fā)現(xiàn)一組有效的參數(shù)來完成交易并推進當前狀態(tài)。

第5部分。我們的結(jié)果以及為什么我們不認為形式正式的驗證是測試安全性的完整解決方案

這種方法是站住腳的，但是我們發(fā)現(xiàn)了這個特殊合同的三個限制，這表明了符號分析和一般形式驗證的挑戰(zhàn)：

1. 表現(xiàn)不佳

2. 應(yīng)用優(yōu)化來選擇操作的難度

3. 修改合同/設(shè)置的必要性，在這種情況下是為了執(zhí)行：內(nèi)聯(lián)調(diào)用、刪除截止日期考慮事項和發(fā)送操作

我們相信挑戰(zhàn)1-2可以通過使用隨機模擬來克服，因此我們得出結(jié)論，符號分析最好用于戰(zhàn)術(shù)上驗證合約/模型的某些方面，或者支持其理解。下面我們詳細介紹我們的方法并解釋我們的發(fā)現(xiàn)。

1. 表現(xiàn)不佳

我們使用一個基于重寫的有界模型檢查器來進行符號分析，它在EVM字節(jié)碼級別上運行。它與Mythril和ManTIcore等基于狀態(tài)的符號解釋器的不同之處在于，它在合約塊完全擴展之后一次性應(yīng)用SMT-solver，而不是在發(fā)現(xiàn)每個塊時增量地應(yīng)用。另一個區(qū)別是，假陰性是不能容忍的。我們使用的底層SMT解決程序是Z3。解釋器包含幾個優(yōu)化，我們將在下面詳細介紹。

作為輸出，我們提取了參數(shù)數(shù)組（也稱為CALLDATA）并使用合約接口，將其轉(zhuǎn)換為相關(guān)合約函數(shù)的一組有效的高級參數(shù)。

我們從字節(jié)碼合約直開始，并實現(xiàn)了幾個優(yōu)化：

· 一個多級反編譯器與塊修剪

· Z3上的自定義包裝器，帶有用于非決定論的操作符

· 公共數(shù)據(jù)的模塊化表示

· EVM級別的二進制類型

· 先進的具體化

這是每個功能/動作的性能：

［所有時間在2013年MacBook Air上測量，i7 8GB］

最后一個加星的例子是直接實現(xiàn)Z3的流動性函數(shù)，例如，一個代表性的“理論最小值”。操作空間表示哪些合約函數(shù)可用作代理的操作。Add代表addLiquidity，等等。

為了解釋這些結(jié)果，我們必須解釋符號分析器的性能特征。在我們的示例中，超過90%的計算時間直接花費在SMT求解程序中。因此，性能優(yōu)化的大部分工作都花在優(yōu)化如何重寫SMT求解程序的合約上。

不幸的是，位向量乘法對目前的SMT求解器是一個挑戰(zhàn)。讓我們假設(shè)SMT求解器的性能（非常）松散地與所需的命題項數(shù)量相關(guān)。為了說明這一點，EVM中的每個數(shù)字都表示為一個256位的單詞。在Z3中，這些單詞進一步“分解”為表示每個位的256個命題變量。表示位向量乘法需要多達256個部分和，每個部分和表示另一個256位單詞，需要65，000個變量。移除性函數(shù)包含四個乘法

這些單詞被進一步“分解”為表示每個位的256個命題變量。表示位向量乘法需要多達256個部分和，每個部分和表示另一個256位單詞，需要65，000個變量。流動性函數(shù)總共包含四次乘法。

雖然SMT求解器的性能無法以任何直接或算術(shù)的方式預(yù)測，但是乘法和除法對該契約的影響也通過從源中刪除它得到了獨立的驗證（產(chǎn)生的運行時可以忽略不計）。

這是一個很好的例子，在這個例子中，概念簡單的合約可能需要不可預(yù)測的大量解決方案時間。一般來說，非專業(yè)人員很難預(yù)測SMT-solver的性能，正如我們所看到的，它并不一定與所使用的代碼行或其他容易識別的指標相關(guān)。

2. 應(yīng)用優(yōu)化來選擇操作的難度

使SMT解決方案對這個應(yīng)用程序具有吸引力的是它發(fā)現(xiàn)最優(yōu)操作的潛力。優(yōu)化SMT求解器“vZ”作為Z3的一部分，支持根據(jù)優(yōu)化的變量求解有效的最優(yōu)反例。它結(jié)合了各種子問題的優(yōu)化算法。

優(yōu)化vZ的求解器接口--Bj?rner等人的優(yōu)化SMT求解器。

我們完成了實驗，以確定優(yōu)化求解器是否可以用來發(fā)現(xiàn)最優(yōu)的交易，根據(jù)給定的價格時間表，但不幸的是，求解器運行會超過24小時。

我們認為優(yōu)化在特定的情況下仍然是計算上可行的，比如合約更簡單，優(yōu)化問題很容易映射到“vZ”中可用的算法，例如線性問題的單純形法。

3.修改合約的必要性

在形式驗證中，降低合約復(fù)雜度（特別是在字節(jié)碼級別）對于性能至關(guān)重要，或者是應(yīng)用依賴于輸入結(jié)構(gòu)的形式化驗證器的先決條件。

我們對Uniswap合約所做的關(guān)鍵修改是去掉與子調(diào)用和外部調(diào)用相關(guān)的復(fù)雜性，并將重點放在交換邏輯上：

·刪除內(nèi)部和外部子調(diào)用，內(nèi)聯(lián)內(nèi)部調(diào)用，并在合同內(nèi)部建模ERC20帳戶持有