構造形式化證明，解決智能合約安全問題——你的合約亟待證明

智能合約安全問題始終是縈繞在數字貨幣各個項目方、開發者和投資者心頭的一顆定時炸彈。越來越多的安全團隊積极參与，試圖通過更完備手段來解決合約安全問題。安比（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 verificationis 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_after_initialization: 合約初始化完成後，token 總量不變

Property_totalSupply_fixed_delegate_transfer： 合約執行完成 transferFrom() 轉賬操作以後，token 總量不變

Property_from_to_balances_change: 轉賬操作後，合約中僅餘額轉出和轉入的賬戶發生改變，其它賬戶不變

證明過程簡述

1.合約solidity源碼：ERC20 的合約代碼，為標準的 ERC20 合約。包含六個函數：構造函數，transfer()，transferFrom()，balanceOf()，approve()，allowance()。

2.合約規範：

Aspecification languageis 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 合約的六個函數的規範。

每個函數的執行都可能涉及多種情況，函數在一類情況下的行為可以通過一條規則描述，所以通常函數的規範由一條或者多條規則組成。以  函數的規範的為例，它由兩條規則  和  組成，分別對應允許轉賬額度小於  和等於  的情況。

以  為例，每條規範規則由以下幾個部分組成。

定義了在該類情況下執行該函數前必需滿足的條件：

定義了函數成功執行所產生的所有事件：

其中，

對應  事件；

是一個偽事件，用於標記函數的返回以及返回值。

定義了函數成功執行對合約狀態的改變，例如哪些 storage 變數發生的改變：

即， 和  的相應項發生了預期的變化，而其它 storage variable 保持不變。

3.證明合約滿足規範

證明高層性質的過程是基於以上定義的規範完成的，但在性質證明之前，我們需要保證 Solidity 源碼本身需滿足我們定義的規範。首先我們要將合約的 Solidity 實現表示在 Coq 中。為此我們在 Coq 中實現了一個 Domain Specific Language (DSL)，用於在 Coq 中表示 Solidity 代碼。例如 ERC20 中的  的實現在DSL.v中被表示成如下形式：

然後，我們需要證明以 DSL 表示的各個合約函數滿足對應的合約規範。例如， 滿足規範  可由DSL.v中的如下引理證明：

4.高層性質的定義和證明

上述規範描述了合約中單個函數的單次執行的行為。高層性質描述的是合約作為一個整體，在接受任意的 message call 的情況下，仍然具備的性質。例如Prop.v中定義的ERC20 中所有賬戶不會存在 token 丟失，個賬戶 token 總量始終和總發行量一致的性質：

5.包括該性質在內的所有高層性質的詳細定義和證明過程，請參見Spec.v。

未來的計劃

與傳統的安全問題不同，智能合約的安全問題危害更嚴重，波及範圍更廣，造成的經濟損失更大。形式化驗證無疑是解決智能合約安全問題的一把利劍。

在一定的邊界條件內，形式化驗證可以保證代碼的絕對安全可信，根本上杜絕了某一類漏洞問題。本倉庫對以ERC20 token 合約的幾個簡單性質為例，初步介紹了形式化驗證如何應用在智能合約領域，但僅此還不足以突顯形式化驗證的巨大價值。但隨著智能合約應用範圍的擴大，業務邏輯複雜度進一步增加，更甚者當涉及更深層次的經濟學，博弈論問題，藉助於形式化驗證背後完備的數學理論和哲學思想，加以驗證和證明，必將帶來更多的驚喜。

儘管形式化證明是保證智能合約安全極其有效的手段，但目前國內這一領域專業人才較少，相關的研究還比較匱乏，也缺少相應的工具支撐。安比（SECBIT）實驗室成員依託形式化驗證領域十餘年的研究經驗，致力於把該項技術更廣泛應用於智能合約安全。

·我們將會證明更多的通用性質，規避常見漏洞和風險

·我們將證明功能更加豐富的 Token 合約，如凍結、升級、許可權管理、增加控制等。

·我們將研究如何證明一些博弈論相關的高層性質，如公平性，最優策略與納什均衡等。

同時我們更希望越來越多的技術愛好者可以參與進來，共同為形式化驗證和智能合約的發展貢獻一份力量。如果有任何問題或者想法，歡迎加入我們的 Gitter 進行討論。

Gitter地址: https://gitter.im/sec-bit/Lobby

參考文獻

[1] DSLs for Ethereum Contracts https://www.michaelburge.us/2018/05/15/ethereum-chess-engine.html

[2] Formal verification https://en.wikipedia.org/wiki/Formal_verification

[3] Domain-specific language https://en.wikipedia.org/wiki/Domain-specific_language

[4] 安?（SECBIT）實驗室攜?路印（Loopring）共同發布智能合約風險列表 https://mp.weixin.qq.com/s/XbXlrmt0fi9IgxicmdAF0w

[5]【推薦】王健：說說形式化驗證（Formal Verification）吧 http://chainb.com/?P=Cont&id=1957

[6] C. A. R. Hoare. An axiomatic basis for computer programming.Communications of the ACM, 26(1):53-56, Jan. 1983.

[7] L. Lamport. Proving the correctness of multiprocess programs.IEEE Transactions on Software EngineeringSE-3, 2 (March 1977), 125-143.

[8] G. Necula. Proof-carrying code. InProc.24th ACMsymposium on Principles of programming languages (POPL』97). pages 106-119, New York, Jan. 1997.

[9] Inria: The Coq Proof Assistant. https://coq.inria.fr/

[10] Cadar, C., Dunbar, D., Engler, D.R., et al.: Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: OSDI. Volume 8. (2008) 209–224

[11] Gaudel, M.C.: Testing from formal specifications, a generic approach. In: International Conference on Reliable Software Technologies, Springer (2001) 35–48

[12] Nielson, F., Nielson, H.R., Hankin, C.: Principles of program analysis. Springer (2015)

[13] Gaudel, M.C.: Testing from formal specifications, a generic approach. In: International Conference on Reliable Software Technologies, Springer (2001) 35–48

[14] Inria: The Gallina specification language. https://coq.inria.fr/distrib/current/refman/language/gallina-specification-language.html

[15] 基於邏輯的形式化驗證方法:進展及應用  http://xbna.pku.edu.cn/html/2016-2-363.htm

【關於安比（SECBIT）實驗室】

安比（SECBIT）實驗室專註於區塊鏈與智能合約安全問題，全方位監控智能合約安全漏洞、提供專業合約安全審計服務，在智能合約安全技術上開展全方位深入研究，致力於參與共建共識、可信、有序的區塊鏈經濟體。

（本文首發自 安比實驗室SECBIT，巴比特資訊經授權轉載）

喜歡這篇文章嗎？立刻分享出去讓更多人知道吧！