為什么說形式驗(yàn)證不是測(cè)試安全性的完整解決方案

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

概述

形式驗(yàn)證可以提供對(duì)智能合約邏輯和安全性的獨(dú)特見解。然而，當(dāng)試圖對(duì)一份智能合約的財(cái)務(wù)結(jié)果進(jìn)行陳述時(shí)，形式是不夠的。

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

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

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

第1部分。Uniswap合約的高級(jí)概覽

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

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

· 交易。然后，市場(chǎng)參與者可以直接使用Uniswap交易所合同進(jìn)行交易。

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

· 流動(dòng)性的費(fèi)用。小額費(fèi)用被征收并分配給流動(dòng)性提供者。

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

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

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

· 有效性。我們想要的模型會(huì)激勵(lì)我們想要的行為嗎？

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

第3部分。Uniswap智能合約的形式驗(yàn)證歷史

形式驗(yàn)證

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

之前的工作

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

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

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

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

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

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

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

制定問題

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

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

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

例如，在形式驗(yàn)證中，假設(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的驗(yàn)證。

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

具有象征意義的分析

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

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

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

1. 表現(xiàn)不佳

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

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

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

1. 表現(xiàn)不佳

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

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

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

· 一個(gè)多級(jí)反編譯器與塊修剪

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

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

· EVM級(jí)別的二進(jìn)制類型

· 先進(jìn)的具體化

這是每個(gè)功能/動(dòng)作的性能：

［所有時(shí)間在2013年MacBook Air上測(cè)量，i7 8GB］

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

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

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

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

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

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

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

使SMT解決方案對(duì)這個(gè)應(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求解器。

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

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

3.修改合約的必要性

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

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

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

·刪除發(fā)送行為

·刪除時(shí)間戳的截止日期約束

符號(hào)分析在激勵(lì)仿真中的作用

在這篇博客文章中，我們展示了與基于代理的模擬相比，符號(hào)分析在分析像Uniswap這樣的復(fù)雜系統(tǒng)時(shí)是多么的不足。也就是說，形式驗(yàn)證是一個(gè)重要和有力的工具。但它在戰(zhàn)術(shù)上最好是作為更廣泛的激勵(lì)模擬的補(bǔ)充：

·模型驗(yàn)證。驗(yàn)證一個(gè)簡化的仿真模型

·提取模型。通過驗(yàn)證操作，幫助從代碼中自動(dòng)提取模型

·官方的建議。為仿真提供新的或極端的啟動(dòng)狀態(tài)

·局部優(yōu)化。使用內(nèi)置的優(yōu)化器驗(yàn)證關(guān)于局部最優(yōu)性的假設(shè)