構造形式化證明，解決智能合約安全問題——你的合約亟待證明區塊鏈
智能合約的可信度是來源于不可篡改性，以太坊的智能合約一旦部署上線后就無法再修改。一旦合約存在安全漏洞，任何人都可以發起攻擊，并且在攻擊發生后，假如合約沒有一定的防御措施，將會無法阻止安全問題的進一步惡化。這無論是對合約本身的經濟價值（如Token）還是公眾對項目的信任，都會造成嚴重的損害。
智能合約安全問題始終是縈繞在數字貨幣各個項目方、開發者和投資者心頭的一顆定時炸彈。越來越多的安全團隊積極參與，試圖通過更完備手段來解決合約安全問題。安比（SECBIT）實驗室認為，形式化驗證與傳統的“測試 審計”方式相結合，將會是保證智能合約安全強有力的手段。
7月7日，安比（SECBIT）實驗室聯合 ConsenSys 正式發布 ERC20 合約的形式化證明源碼。該合約代碼來源于 ConsenSys 官方提供的 ERC20 合約模板，形式化證明代碼已上傳至 Github 倉庫（tokenlibs-with-proofs），地址如下：
https://github.com/sec-bit/tokenlibs-with-proofs
ConsenSys 官方源碼地址：
https://github.com/ConsenSys/Tokens/blob/master/contracts/eip20
我們針對 ERC20 合約常見問題和特性展開了證明，證明性質分為以下幾個部分
漏洞溢出
合約中 Token 總量
轉賬操作對任意賬戶的影響
我們希望以本項目為切入點，展示形式化驗證是如何應用到智能合約領域的，進而幫助更多的技術人員學習或參與到智能合約的形式化驗證中。
我們也希望利用形式化證明，剔除漏洞合約，為大家篩選出更多較為安全的合約模板。
同時，安比實驗室也將致力于使用形式化驗證的方法，從業務實現，技術安全和經濟學等維度，構建更加可信安全的智能合約。
什么是形式化驗證？
下面是來自維基百科的一個形式化驗證的定義：
In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics.
The verification of these systems is done by providing a formal proof on an abstract mathematical model of the system, the correspondence between the mathematical model and the nature of the system being otherwise known by construction. Examples of mathematical objects often used to model systems are: finite state machines, labelled transition systems, Petri nets, vector addition systems, timed automata, hybrid automata, process algebra, formal semantics of programming languages such as operational semantics, denotational semantics, axiomatic semantics and Hoare logic.
從上述定義，我們可以看到，形式化驗證事實上包含了各種不同的驗證理論技術。但是，萬變不離其宗，形式化驗證簡單說就是一個基于數學模型的驗證。驗證的過程是為了保證這個數學模型滿足一定的性質。
本文后面所采用的形式化驗證理論技術，是將智能合約語言編寫的代碼作為數學模型，將智能合約所需要滿足的要求作為性質進行證明。通俗的來講，就是使用數學語言來描述合約代碼，并證明其具有一些好的性質，例如不存在整數溢出漏洞。
更深一步講，我們是通過形式化的程序邏輯(Program Logic)，來證明一個智能合約程序（Code）是否滿足已給定的形式化規范（Formal Specification），然后，在規范的基礎上，證明智能合約的行為始終滿足一些高層性質（High-level Property），并且通過顯式的證明（Proof Object）來使用戶確信驗證結果的正確性。
當我們在討論任何形式化驗證理論或者技術時，都繞不開下面三個關鍵點：
任何證明都是在一定的前提假設下的證明；
證明過程是依賴形式化邏輯理論的正確推理；
證明的最終結果（定理）是大家能夠取得共識的結論；
安比實驗室（SECBIT）所采用的形式化驗證方法中，第一點需要保證一些基本的定義是正確的；第二點需要保證證明過程的合法性，這里我們采用流行的證明輔助工具 Coq 來表示證明和檢查證明；第三點我們證明的結論正確表達了大家共同關心的 ERC20 性質。
注意：這三點內容是形式化證明的前提條件，是我們對保證合約安全的必須信任的前提條件，是智能合約形式化證明的信任基礎（Trusted Computing Base）。任何安全都必須基于一定的信任基礎，一個系統的信任基礎越小，那么它就越安全。本文所采用的形式化證明方法將信任基礎降到了最小集合。
智能合約為何需要形式化證明
以比特幣為首的區塊鏈技術將智能合約的構想落地，隨之以太坊將智能合約發揚光大。以太坊將比特幣交易中的腳本變成了一種通用的圖靈完備的編程語言。（注：所謂圖靈完備是指編程語言的表達能力得到了最大程度的釋放），但是過于自由的以太坊智能合約編程語言也使智能合約會和傳統軟件一樣，被無處不在的安全漏洞和Bug所困擾。自從以太坊正式上線以來，由于智能合約漏洞/缺陷所帶來的經濟損失數以億記。
安比實驗室目前已經對以太坊上所有部署的 Token 合約進行掃描，將已披露的合約漏洞與安全風險進行了全景分析，披露問題合約的總數量達到 4,172 個，其中被 CoinMarketCap 收錄的合約數量達 101 個。問題合約列表被 ConsensysLabs 收錄到推薦開發者工具列表中。
推薦開發者工具列表地址：
https://github.com/ConsenSysLabs/ethereum-developer-tools-list
安比實驗室在審計過大量的智能合約之后，發現相比傳統軟件而言，智能合約的安全問題更加棘手，現實情況也更加嚴峻：
智能合約的可信度是來源于不可篡改性，以太坊的智能合約一旦部署上線后就無法再修改。一旦合約存在安全漏洞，任何人都可以發起攻擊，并且在攻擊發生后，假如合約沒有一定的防御措施，將會無法阻止安全問題的進一步惡化。這無論是對合約本身的經濟價值（如Token）還是公眾對項目的信任，都會造成嚴重的損害。
智能合約部署上線后，一部分項目會公開合約源碼。源碼的公開一方面是增強用戶對合約的信任度，但是另一方面也大幅度降低了黑客攻擊的成本，代碼中的任何一個小問題都有可能被黑客捕捉到并且加以利用。
智能合約開發過程涉及的問題更是方方面面，而智能合約發展時間比較短其本身還存在很多的不足；同時市面上專業的技術人員嚴重缺乏，無法避免人為因素引起的漏洞，因此稍有不慎就有可能留下致命的安全隱患。
合約測試安全團隊開發自動化測試工具，自動生成大量的測試用例執行合約來進行測試，檢測在盡量多的條件下，合約是否能夠正確執行。但由于測試用例無法保證100%覆蓋所有的情況，所以，即使測試結果沒有發現問題，也不能保證合約的實現一定沒有漏洞。
合約審計安全審計人員對合約源碼從代碼實現和業務邏輯等多個角度進行審計。安全團隊通過專業的手段檢查出大部分的合約漏洞和隱患，并在業務邏輯的實現上給與項目方指導或者建議。盡管安全審計可以發現并規避大部分常見的漏洞和風險，但由于審計工作在一定程度上依賴于審計人員的自身經驗和主觀判斷，并不能100%完全杜絕安全風險和漏洞。
而形式化證明是通過形式化邏輯的方式來表示合約代碼，并加以嚴格地推理證明。這個過程依賴于數學邏輯推理的嚴密性，保證 100% 覆蓋到到代碼的運行期行為，可以明確保證在一定范圍內的絕對正確，能彌補以上兩種傳統方式的局限。因此形式化證明在一些安全攸關的領域，如航天、高鐵、核電、航空，已經逐步得到應用，并且取得了非常好的效果。
而智能合約代碼，同樣也是對安全要求極高，一旦出現問題，造成的經濟損失更是不可估量。另外一些較為復雜的業務邏輯以及更高階的性質，如經濟學，博弈論范疇的問題，通過測試或者審計的方式更是難以有效驗證。因而對于規模相對較小而設計復雜的智能合約而言，形式化程序驗證無疑是保證其安全可靠的有效方法之一。
如何為智能合約構造形式化證明
盡管形式化驗證是保證智能合約安全極其有效的手段，但目前相關的研究還比較匱乏，也缺少相應的工具支撐。安比實驗室發布了 ERC20 合約的形式化證明，一方面希望能夠為大家篩選出一份安全的合約模板；另一方面也希望能夠借此讓更多的人了解并學習形式化驗證，共同參與到智能合約的形式化驗證領域中來。
證明結構
Token形式化證明大致可以分為四個部分：合約源碼，代碼規范，合約性質，證明。
形式化驗證需要按照形式化方法的步驟來實現。
合約源碼：Solidity 源碼即我們要證明的代碼
代碼規范：代碼規范定義每一個合約函數的預期行為。
合約性質：合約的性質是形式化證明最終需要保證的性質，如Token發行總量保持不變。
證明：基于代碼規范，對合約特定的性質進行證明。
到底證明了哪些性質
Token 合約主要包含以下幾種性質的證明過程：
nat_nooverflow_dsl_nooverflow：transfer() 和 transferFrom() 操作不存在溢出漏洞
Property_totalSupply_equal_to_sum_balances：在合約中，任意執行完成一步后，合約中 totalSupply 的值與所有賬戶的余額的總和相等
Property_totalSupply_fixed_transfer : 合約執行完成 transfer() 轉賬操作以后，token 總量不變
Property_totalSupply_fixed_delegate_transfer ： 合約執行完成 transferFrom() 轉賬操作以后，token 總量不變
Property_from_to_balances_change : 轉賬操作后，合約中僅余額轉出和轉入的賬戶發生改變，其它賬戶不變
證明過程簡述
1.合約solidity源碼：ERC20 的合約代碼，為標準的 ERC20 合約。包含六個函數：構造函數，transfer()，transferFrom()，balanceOf()，approve()，allowance()。
2.合約規范：
A specification language is a formal language in computer science used during systems analysis, requirements analysis and systems design to describe a system at a much higher level than a programming language, which is used to produce the executable code for a system.
Spec.v 文件中定義了 ERC20 合約的六個函數的規范。
每個函數的執行都可能涉及多種情況，函數在一類情況下的行為可以通過一條規則描述，所以通常函數的規范由一條或者多條規則組成。以 transferFrom() 函數的規范的為例，它由兩條規則 funspec_transferFrom_1 和 funcspec_transferFrom_2 組成，分別對應允許轉賬額度小于 2**256-1 和等于 2**256-1 的情況。
以 funcspec_transferFrom_1 為例，每條規范規則由以下幾個部分組成。
spec_require 定義了在該類情況下執行該函數前必需滿足的條件：
spec_events 定義了函數成功執行所產生的所有事件：
其中，
ev_Transfer 對應 Transfer 事件；
ev_return 是一個偽事件，用于標記函數的返回以及返回值。
spec_trans 定義了函數成功執行對合約狀態的改變，例如哪些 storage 變量發生的改變：
即，balances 和 allowed 的相應項發生了預期的變化，而其它 storage variable 保持不變。
3.證明合約滿足規范
證明高層性質的過程是基于以上定義的規范完成的，但在性質證明之前，我們需要保證 Solidity 源碼本身需滿足我們定義的規范。首先我們要將合約的 Solidity 實現表示在 Coq 中。為此我們在 Coq 中實現了一個 Domain Specific Language (DSL)，用于在 Coq 中表示 Solidity 代碼。例如 ERC20 中的 transfer() 的實現在 DSL.v 中被表示成如下形式：
然后，我們需要證明以 DSL 表示的各個合約函數滿足對應的合約規范。例如，transfer() 滿足規范 funcspec_transfer 可由 DSL.v 中的如下引理證明：
4.高層性質的定義和證明
上述規范描述了合約中單個函數的單次執行的行為。高層性質描述的是合約作為一個整體，在接受任意的 message call 的情況下，仍然具備的性質。例如 Prop.v 中定義的 ERC20 中所有賬戶不會存在 token 丟失，個賬戶 token 總量始終和總發行量一致 的性質：
5.包括該性質在內的所有高層性質的詳細定義和證明過程，請參見 Spec.v。
未來的計劃
與傳統的安全問題不同，智能合約的安全問題危害更嚴重，波及范圍更廣，造成的經濟損失更大。形式化驗證無疑是解決智能合約安全問題的一把利劍。
在一定的邊界條件內，形式化驗證可以保證代碼的絕對安全可信，根本上杜絕了某一類漏洞問題。本倉庫對以ERC20 token 合約的幾個簡單性質為例，初步介紹了形式化驗證如何應用在智能合約領域，但僅此還不足以突顯形式化驗證的巨大價值。但隨著智能合約應用范圍的擴大，業務邏輯復雜度進一步增加，更甚者當涉及更深層次的經濟學，博弈論問題，借助于形式化驗證背后完備的數學理論和哲學思想，加以驗證和證明，必將帶來更多的驚喜。
盡管形式化證明是保證智能合約安全極其有效的手段，但目前國內這一領域專業人才較少，相關的研究還比較匱乏，也缺少相應的工具支撐。安比（SECBIT）實驗室成員依托形式化驗證領域十余年的研究經驗，致力于把該項技術更廣泛應用于智能合約安全。
我們將會證明更多的通用性質，規避常見漏洞和風險
我們將證明功能更加豐富的 Token 合約，如凍結、升級、權限管理、增加控制等。
我們將研究如何證明一些博弈論相關的高層性質，如公平性，最優策略與納什均衡等。
同時我們更希望越來越多的技術愛好者可以參與進來，共同為形式化驗證和智能合約的發展貢獻一份力量。如果有任何問題或者想法，歡迎加入我們的 Gitter 進行討論。
1.TMT觀察網遵循行業規范，任何轉載的稿件都會明確標注作者和來源；
2.TMT觀察網的原創文章，請轉載時務必注明文章作者和"來源：TMT觀察網"，不尊重原創的行為TMT觀察網或將追究責任；
3.作者投稿可能會經TMT觀察網編輯修改或補充。
