形式化驗證：讓智能合約更安全
責編：gltian ｜2018-08-13 15:01:52區塊鏈是一種分布式賬本技術，其通過提供業務交易和數字資產的一致性、不可變性來提高參與方的可信度，還能通過交易中提供更大的透明度來減少參與方之間的摩擦，這些特性使得更多行業的應用場景得以重塑。區塊鏈技術的快速發展，促使企業架構和技術創新的領導人開始重新思考分布式信任世界里的價值交換概念，同時也因之而滋生了眾多新技術。從下圖中能夠看出，目前還有許多技術尚處于科技誕生的促動期，如智能合約。
目前數字經濟正在向可編程經濟時代演進，區塊鏈技術支持著智能資產和智能合約以編程方式促進、核實或執行合同條款，促使著可編程經濟的發展。智能合約對可編程經濟起著重要的推動作用，但在其應用卻面臨著種種問題。一直在跟蹤研究區塊鏈及其相關技術安全性問題的梆梆安全研究院，結合智能合約的技術發展歷程、應用特點和安全風險等，探索出了一套直指其核心本質的安全解決方案。
區塊鏈技術成熟度曲線（來自Gartner,2018）
一、智能合約與區塊鏈完美結合，應用廣泛
第二代區塊鏈技術與第一代的顯著區別是智能合約的使用，梆梆安全研究院發現智能合約(Smart contract)這個術語在區塊鏈出現之前已出現，至少可以追溯到1995年，由多產的跨領域法律學者、受到廣泛贊譽的密碼學家尼克·薩博(Nick Szabo)所提出，他在發表于自己網站的幾篇文章中提到了智能合約理念，定義如下：
一個智能合約是一套以數字形式定義的承諾（promises），包括合約參與方可以在上面執行這些承諾的協議。
智能合約理念幾乎與互聯網(world wide web)同時出現，從本質上講，這些自動合約的工作原理類似于其它計算機程序的if-then語句，一種旨在以信息化方式傳播、驗證或執行合同的計算機協議。允許在沒有第三方的情況下進行可信交易，這些交易可追蹤且不可逆轉。當一個預先編好的條件被觸發時，智能合約執行相應的合同條款。
在計算機上進行智能合約實際應用時，需要控制實物資產保證有效地執行合約，同時做到執行合約條款時，能獲取到的第三方審核的合約方的信息，即需要解決信息傳遞與信任問題。
在無法建立信任關系的互聯網上，區塊鏈技術依靠密碼學和巧妙的分布式算法，無需借助任何第三方中心機構的介入，用數學的方法使參與者達成共識，保證交易記錄的存在性、合約的有效性以及身份的不可抵賴性，解決了互聯網上信任和價值傳遞，為智能合約的廣泛應用提供了絕佳的溫床。第二代區塊鏈開源項目——以太坊ethereum使用了智能合約，Linux基金會主導推動區塊鏈跨行業應用的開源項目——hyperledge也支持智能合約。智能合約使很多不同類型的程序和操作得以自動化，最明顯的體現之處在于支付環節及付款時的步驟操作。
2016年底由智能合約聯盟支持下編寫的數字商務商會的白皮書介紹了數字身份、抵押、供應鏈、癌癥研究等 12 項智能合約商業使用案例，目前智能合約已在金融、醫療等多個領域實際應用，坊間認為2017年是智能合約元年。
二、智能合約代碼漏洞越來越多，頻遭攻擊
隨著人們越來越多地了解區塊鏈技術，以太坊的熱度逐漸增加。然而，最新的研究顯示基于以太坊架構，被稱作是“最安全、最可靠、最方便”的智能合約技術卻漏洞百出。來自新加坡國立大學、新加坡耶魯大學學院和倫敦大學學院的一組研究人員發布了一份報告，聲稱已經發現了超過34，200個不安全的智能合約。他們還聲稱其中大約3000個不安全的智能合約可能會造成600萬美元的ETH被盜，具體發生的智能合約攻擊事件有：
2016年6月18日，TheDAO遭黑客發起Renntrancy攻擊，導致300多萬以太幣資產被分離出DAO資產給自己。
2017年7月21日，智能合約編碼公司警告1.5版本及之后的錢包軟件存在漏洞，Etherscan.io的數據確認有價值3000萬美元的15萬以太幣被盜；
2017年11月8日，錢包再現重大Bug，多重簽名漏洞被黑客利用，導致上億美元資金被凍結。
2018年4月22日，BEC市場瞬間蒸發64億人民幣，黑客利用以太坊ERC-20智能合約中BatchOverFlow漏洞，攻擊了美鏈BEC的智能合約。
2018年4月25日，各大交易所暫停SmartMesh(SMT)的充值和提現交易， SMT也曝出存在安全漏洞；
2018年5月23日，EDU(EduCoin)被爆出現合約漏洞，多達數十億代幣被盜。
智能合約本質上是一段運行在區塊鏈網絡中的代碼，而代碼在設計和開發過程中，不可避免出現漏洞。部署在公鏈上的智能合約，由于暴露在開放網絡上，容易被黑客獲得，成為黑客的金礦和攻擊目標，造成無法彌補的損失。
三、形式化驗證方法保障智能合約安全
梆梆安全研究院在研究區塊鏈安全時發現，加強智能合約審計是提高區塊鏈安全的重要保證，其中形式化驗證是解決智能合約審計的一個有效方法。
所謂形式化驗證方法，即指在計算機科學領域，特別是軟件工程和硬件工程中，一種特殊的基于數學的技術，用于規范、開發和驗證軟件和硬件系統，以提高系統的安全性、可靠性和魯棒性。形式化方法可以形容為建立在相當廣泛的理論計算機科學基礎上的應用，特別是邏輯演算、形式語言、自動機理論、離散事件動態系統和程序的語義，還包括類型系統和代數數據類型等理論。一般這類研究主要應用于昂貴的航空、航天、軍事器材的操作系統、危險的醫療設備程序之中。
形式化驗證方法就是基于已建立的形式化規格，對所規格系統的相關特性進行分析和驗證，以評判系統是否滿足期望的特性。形式化驗證并不能完全確保系統的性能正確無誤，但是可以最大限度地理解和分析系統，并盡可能地發現其中不一致性、模糊性、不完備性等錯誤。形式化驗證可用來消除高風險代碼漏洞。
形式化驗證主要包括定理證明和模型驗證兩種技術：
現有的定理證明器包括：用戶導引自動推演工具、證明檢驗器和復合證明器。用戶導引自動推演工具有ACL2、Eves、LP、Nqthm、Reve和RRL，這些工具由引理或者定義序列導引，每一個定理采用已建立的推演、引理驅動重寫和簡化啟發式來自動證明；證明檢驗器有Coq、HOL、LEGO、LCF和Nuprl；復合證明器Analytica中將定理證明和符號代數系統Mathematica復合，PVS和Step將決策過程模型檢驗和交互式證明復合在一體。
模型檢驗是一種基于有限模型并檢驗該模型的期望特性的一種技術。粗略地講，檢驗就是狀態空間的蠻力搜索，模型的有限性確保了搜索可以終止。模型檢驗有兩種主要方法。其一是時態模型檢驗，該方法中規格以時態邏輯形式表述，系統模擬為有限狀態遷移系統。有效的搜索過程用來檢驗給定的有限狀態遷移系統是否是規格的一個模型。另一種方法中，規格以自動機方式給出，系統也模擬為一個自動機。系統的自動機模型和規格比較，以確定其行為是否與規格的自動機模型一致。基于模型檢驗的工具有描述語言為Promela 的SPIN和UPPAL等。
智能合約采用全生命周期的形式化驗證，在設計和開發過程都可用形式化驗證，代碼的形式化驗證在統一的環境可以采用源碼和編譯后的字節碼進行雙管齊下的驗證，源代碼進行轉換驗證，編譯后的字節碼進行反編譯驗證低級別性能，兩個驗證方法利用等價證明保證功能、運行上的一致。如以太坊可用在F*環境下進行驗證，反編譯字節驗證gas總量上限。
梆梆安全研究院于2016年就開始布局區塊鏈安全，最初著手于區塊鏈的私鑰安全研究，之后開始逐漸深入研究基于區塊鏈的數字貨幣交易系統、業務系統的安全性問題。在研究過程中梆梆安全研究院發現，作為區塊鏈第二代技術的核心創新點——智能合約，其安全性問題非常重要，需要用形式化驗證的方法保障其安全，由此來有效抵御利用智能合約安全漏洞所發起的惡意攻擊，并降低因此而產生的巨大經濟損失。