第1部分。Uniswap合約的高階概覽
Uniswap exchange是一組智慧合約，允許任何人在不向訂單簿提交訂單的情況下交易以太幣和ERC20代幣。單個Uniswap交換合約支援特定的以太幣/ERC20代幣，任何人都可以使用Uniswap合約建立新的代幣對。一旦交易所成立，它就會自主運作:
· 流動性的創造。流動資金提供者將首先按當前匯率提供以太幣和代幣。可以在任何時候新增/刪除更多。
· 交易。然後，市場參與者可以直接使用Uniswap交易所合同進行交易。
· 定價演算法。給定交易的價格是使用“常數產品做市商”模型自動確定的。在給定的貿易期間，Uniswap將設定價格，以便儲存產品(x * y = k)的以太幣量和給定的代幣。
· 流動性的費用。小額費用被徵收並分配給流動性提供者。
第2部分。如何測試區塊鏈系統的安全性
要想知道Uniswap這樣的系統是否安全，我們需要回答兩個問題:
· 正確性。程式碼是否遵循我們預期的模型(作為規範或其他形式編寫)?
· 有效性。我們想要的模型會激勵我們想要的行為嗎?
形式驗證只對前者有一些幫助，而對後者幾乎沒有幫助。像“我們應該如何設定費率”這樣的問題根本無法透過形式驗證來回答。
第3部分。Uniswap智慧合約的形式驗證歷史
形式驗證
許多專案都嘗試使用形式驗證技術來證明他們的合約是正確的。對於相對簡單的智慧合約，這是非常可行的。形式驗證和程式分析技術可以確定程式碼是否遵循給定的規範，而且常常會出現致命的反例。
之前的工作
Uniswap現有的輕量級形式驗證就是使用這些技術可以實現的一個很好的例子。利用KEVM框架驗證了做市商(x * y = k)模型及其透過addLiquidity、removeliquity、ethToTokenSwapInput和ethToTokenSwapOutput的實現。假設現有的ERC20合約“表現良好”。
在共識系統調查公司(consensus sys Diligence)的後續審計中，該團隊能夠推斷出如果打破這一假設會發生什麼。他們發現，ERC20代幣的惡意實現可以用來欺騙市場參與者，讓攻擊者重新進入Uniswap合約，以同樣的成本消耗更多的資金。
原則上，可以將此擴充套件規範捕獲為程式碼模板。可以表示和呼叫一個半ERC20相容的合約(相同的介面，但不一定是ERC20行為)，並嘗試使用形式驗證來發現攻擊。在實踐中，這使得形式驗證問題在計算上更加複雜，因為當用於發現任意程式時，底層SMT解決程式中的分支會增加。這種技術有時被稱為“程式綜合”。微軟研究院的這項調查是瞭解更多資訊的良好起點。
這些挑戰說明了與形式驗證(包括程式綜合)相關的另外兩個限制:
· 完整的規範在編寫和表達方面可能具有挑戰性。
· 目前的形式驗證器只適用於簡單的合約和簡單的規範。
第4部分。我們如何應用形式驗證
制定問題
為了測試合約在一組代理的影響下的行為，我們首先嚐試使用符號分析將其應用於自動化操作發現。符號分析將程式碼轉換成一組可以由SMT求解器求解的公式。SMT求解器是SAT求解器的擴充套件，它超越了布林公式(對簡單命題進行陳述)到包含inte的公式
符號分析將程式碼轉換成一組可以由SMT求解器求解的公式。SMT求解器是SAT求解器的擴充套件，它超越了布林公式(對簡單命題進行陳述)，涉及整數、位向量、陣列和程式設計中常見的其他資料形式的公式。
一種看待符號分析的簡單方法是，它可以被用來正式指定一個關於給定的智慧合約的假設，證明假設為真，或者生成一個反例。
例如，在形式驗證中，假設通常是關於合約的斷言，例如，“double函式返回的值總是偶數”。
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的驗證。
為了使用符號分析進行操作發現，我們設定了以下假設:“Uniswap合約不支援有效的交易”。如果這被證明是錯誤的，那麼反例將是生成有效合約交易的一組輸入。
具有象徵意義的分析
我們提供了一個黑盒符號直譯器，其中包含一個經過修改的Uniswap交換合約、一個可用資金支援的一條縫帳戶代理池和一組受限制的操作(與合約功能匹配)。在兩個測試鏈上重播完成的操作——一致測試鏈和一個純EVM副本(為了儲存對契約儲存的更改而進行維護)。目標是發現一組有效的引數來完成交易並推進當前狀態。
第5部分。我們的結果以及為什麼我們不認為形式正式的驗證是測試安全性的完整解決方案
這種方法是站住腳的，但是我們發現了這個特殊合同的三個限制，這表明了符號分析和一般形式驗證的挑戰:
1. 表現不佳
2. 應用最佳化來選擇操作的難度
3. 修改合同/設定的必要性，在這種情況下是為了執行:內聯呼叫、刪除截止日期考慮事項和傳送操作
我們相信挑戰1-2可以透過使用隨機模擬來克服，因此我們得出結論，符號分析最好用於戰術上驗證合約/模型的某些方面，或者支援其理解。下面我們詳細介紹我們的方法並解釋我們的發現。
1. 表現不佳
我們使用一個基於重寫的有界模型檢查器來進行符號分析，它在EVM位元組碼級別上執行。它與Mythril和Manticore等基於狀態的符號直譯器的不同之處在於，它在合約塊完全擴充套件之後一次性應用SMT-solver，而不是在發現每個塊時增量地應用。另一個區別是，假陰性是不能容忍的。我們使用的底層SMT解決程式是Z3。直譯器包含幾個最佳化，我們將在下面詳細介紹。
作為輸出，我們提取了引數陣列(也稱為CALLDATA)並使用合約介面，將其轉換為相關合約函式的一組有效的高階引數。
我們從位元組碼合約直開始，並實現了幾個最佳化:
· 一個多級反編譯器與塊修剪
· Z3上的自定義包裝器，帶有用於非決定論的運算子
· 公共資料的模組化表示
· EVM級別的二進位制型別
· 先進的具體化
這是每個功能/動作的效能:
[所有時間在2013年MacBook Air上測量，i7 8GB]
最後一個加星的例子是直接實現Z3的流動性函式，例如，一個代表性的“理論最小值”。操作空間表示哪些合約函式可用作代理的操作。Add代表addLiquidity，等等。
為了解釋這些結果，我們必須解釋符號分析器的效能特徵。在我們的示例中，超過90%的計算時間直接花費在SMT求解程式中。因此，效能最佳化的大部分工作都花在最佳化如何重寫SMT求解程式的合約上。
不幸的是，位向量乘法對目前的SMT求解器是一個挑戰。讓我們假設SMT求解器的效能(非常)鬆散地與所需的命題項數量相關。為了說明這一點，EVM中的每個數字都表示為一個256位的單詞。在Z3中，這些單詞進一步“分解”為表示每個位的256個命題變數。表示位向量乘法需要多達256個部分和，每個部分和表示另一個256位單詞，需要65,000個變數。移除性函式包含四個乘法
這些單詞被進一步“分解”為表示每個位的256個命題變數。表示位向量乘法需要多達256個部分和，每個部分和表示另一個256位單詞，需要65,000個變數。流動性函式總共包含四次乘法。
雖然SMT求解器的效能無法以任何直接或算術的方式預測，但是乘法和除法對該契約的影響也透過從源中刪除它得到了獨立的驗證(產生的執行時可以忽略不計)。
這是一個很好的例子，在這個例子中，概念簡單的合約可能需要不可預測的大量解決方案時間。一般來說，非專業人員很難預測SMT-solver的效能，正如我們所看到的，它並不一定與所使用的程式碼行或其他容易識別的指標相關。
2. 應用最佳化來選擇操作的難度
使SMT解決方案對這個應用程式具有吸引力的是它發現最優操作的潛力。最佳化SMT求解器“vZ”作為Z3的一部分，支援根據最佳化的變數求解有效的最優反例。它結合了各種子問題的最佳化演算法。
