區(qū)塊鏈是一種分布式賬本技術(shù)，其通過提供業(yè)務(wù)交易和數(shù)字資產(chǎn)的一致性、不可變性來提高參與方的可信度，還能通過交易中提供更大的透明度來減少參與方之間的摩擦，這些特性使得更多行業(yè)的應(yīng)用場景得以重塑。區(qū)塊鏈技術(shù)的快速發(fā)展，促使企業(yè)架構(gòu)和技術(shù)創(chuàng)新的領(lǐng)導(dǎo)人開始重新思考分布式信任世界里的價值交換概念，同時也因之而滋生了眾多新技術(shù)。從下圖中能夠看出，目前還有許多技術(shù)尚處于科技誕生的促動期，如智能合約。

[[240128]]

目前數(shù)字經(jīng)濟正在向可編程經(jīng)濟時代演進，區(qū)塊鏈技術(shù)支持著智能資產(chǎn)和智能合約以編程方式促進、核實或執(zhí)行合同條款，促使著可編程經(jīng)濟的發(fā)展。智能合約對可編程經(jīng)濟起著重要的推動作用，但在其應(yīng)用卻面臨著種種問題。一直在跟蹤研究區(qū)塊鏈及其相關(guān)技術(shù)安全性問題的梆梆安全研究院，結(jié)合智能合約的技術(shù)發(fā)展歷程、應(yīng)用特點和安全風險等，探索出了一套直指其核心本質(zhì)的安全解決方案。

區(qū)塊鏈技術(shù)成熟度曲線(來自Gartner,2018)

一、智能合約與區(qū)塊鏈完美結(jié)合，應(yīng)用廣泛

第二代區(qū)塊鏈技術(shù)與第一代的顯著區(qū)別是智能合約的使用，梆梆安全研究院發(fā)現(xiàn)智能合約(Smart contract)這個術(shù)語在區(qū)塊鏈出現(xiàn)之前已出現(xiàn)，至少可以追溯到1995年，由多產(chǎn)的跨領(lǐng)域法律學者、受到廣泛贊譽的密碼學家尼克·薩博(Nick Szabo)所提出，他在發(fā)表于自己網(wǎng)站的幾篇文章中提到了智能合約理念，定義如下：

智能合約理念幾乎與互聯(lián)網(wǎng)(world wide web)同時出現(xiàn)，從本質(zhì)上講，這些自動合約的工作原理類似于其它計算機程序的if-then語句，一種旨在以信息化方式傳播、驗證或執(zhí)行合同的計算機協(xié)議。允許在沒有第三方的情況下進行可信交易，這些交易可追蹤且不可逆轉(zhuǎn)。當一個預(yù)先編好的條件被觸發(fā)時，智能合約執(zhí)行相應(yīng)的合同條款。

在計算機上進行智能合約實際應(yīng)用時，需要控制實物資產(chǎn)保證有效地執(zhí)行合約，同時做到執(zhí)行合約條款時，能獲取到的第三方審核的合約方的信息，即需要解決信息傳遞與信任問題。

在無法建立信任關(guān)系的互聯(lián)網(wǎng)上，區(qū)塊鏈技術(shù)依靠密碼學和巧妙的分布式算法，無需借助任何第三方中心機構(gòu)的介入，用數(shù)學的方法使參與者達成共識，保證交易記錄的存在性、合約的有效性以及身份的不可抵賴性，解決了互聯(lián)網(wǎng)上信任和價值傳遞，為智能合約的廣泛應(yīng)用提供了絕佳的溫床。第二代區(qū)塊鏈開源項目——以太坊ethereum使用了智能合約，Linux基金會主導(dǎo)推動區(qū)塊鏈跨行業(yè)應(yīng)用的開源項目——hyperledge也支持智能合約。智能合約使很多不同類型的程序和操作得以自動化，最明顯的體現(xiàn)之處在于支付環(huán)節(jié)及付款時的步驟操作。

2016年底由智能合約聯(lián)盟支持下編寫的數(shù)字商務(wù)商會的白皮書介紹了數(shù)字身份、抵押、供應(yīng)鏈、癌癥研究等 12 項智能合約商業(yè)使用案例，目前智能合約已在金融、醫(yī)療等多個領(lǐng)域?qū)嶋H應(yīng)用，坊間認為2017年是智能合約元年。

二、智能合約代碼漏洞越來越多，頻遭攻擊

隨著人們越來越多地了解區(qū)塊鏈技術(shù)，以太坊的熱度逐漸增加。然而，最新的研究顯示基于以太坊架構(gòu)，被稱作是“最安全、最可靠、最方便”的智能合約技術(shù)卻漏洞百出。來自新加坡國立大學、新加坡耶魯大學學院和倫敦大學學院的一組研究人員發(fā)布了一份報告，聲稱已經(jīng)發(fā)現(xiàn)了超過34，200個不安全的智能合約。他們還聲稱其中大約3000個不安全的智能合約可能會造成600萬美元的ETH被盜，具體發(fā)生的智能合約攻擊事件有：

• 2016年6月18日，TheDAO遭黑客發(fā)起Renntrancy攻擊，導(dǎo)致300多萬以太幣資產(chǎn)被分離出DAO資產(chǎn)給自己。
• 2017年7月21日，智能合約編碼公司警告1.5版本及之后的錢包軟件存在漏洞，Etherscan.io的數(shù)據(jù)確認有價值3000萬美元的15萬以太幣被盜;
• 2017年11月8日，錢包再現(xiàn)重大Bug，多重簽名漏洞被黑客利用，導(dǎo)致上億美元資金被凍結(jié)。
• 2018年4月22日，BEC市場瞬間蒸發(fā)64億人民幣，黑客利用以太坊ERC-20智能合約中BatchOverFlow漏洞，攻擊了美鏈BEC的智能合約。
• 2018年4月25日，各大交易所暫停SmartMesh(SMT)的充值和提現(xiàn)交易， SMT也曝出存在安全漏洞;
• 2018年5月23日，EDU(EduCoin)被爆出現(xiàn)合約漏洞，多達數(shù)十億代幣被盜。

智能合約本質(zhì)上是一段運行在區(qū)塊鏈網(wǎng)絡(luò)中的代碼，而代碼在設(shè)計和開發(fā)過程中，不可避免出現(xiàn)漏洞。部署在公鏈上的智能合約，由于暴露在開放網(wǎng)絡(luò)上，容易被黑客獲得，成為黑客的金礦和攻擊目標，造成無法彌補的損失。

三、形式化驗證方法保障智能合約安全

梆梆安全研究院在研究區(qū)塊鏈安全時發(fā)現(xiàn)，加強智能合約審計是提高區(qū)塊鏈安全的重要保證，其中形式化驗證是解決智能合約審計的一個有效方法。

所謂形式化驗證方法，即指在計算機科學領(lǐng)域，特別是軟件工程和硬件工程中，一種特殊的基于數(shù)學的技術(shù)，用于規(guī)范、開發(fā)和驗證軟件和硬件系統(tǒng)，以提高系統(tǒng)的安全性、可靠性和魯棒性。形式化方法可以形容為建立在相當廣泛的理論計算機科學基礎(chǔ)上的應(yīng)用，特別是邏輯演算、形式語言、自動機理論、離散事件動態(tài)系統(tǒng)和程序的語義，還包括類型系統(tǒng)和代數(shù)數(shù)據(jù)類型等理論。一般這類研究主要應(yīng)用于昂貴的航空、航天、軍事器材的操作系統(tǒng)、危險的醫(yī)療設(shè)備程序之中。

形式化驗證方法就是基于已建立的形式化規(guī)格，對所規(guī)格系統(tǒng)的相關(guān)特性進行分析和驗證，以評判系統(tǒng)是否滿足期望的特性。形式化驗證并不能完全確保系統(tǒng)的性能正確無誤，但是可以最大限度地理解和分析系統(tǒng)，并盡可能地發(fā)現(xiàn)其中不一致性、模糊性、不完備性等錯誤。形式化驗證可用來消除高風險代碼漏洞。

形式化驗證主要包括定理證明和模型驗證兩種技術(shù)：

• 現(xiàn)有的定理證明器包括：用戶導(dǎo)引自動推演工具、證明檢驗器和復(fù)合證明器。用戶導(dǎo)引自動推演工具有ACL2、Eves、LP、Nqthm、Reve和RRL，這些工具由引理或者定義序列導(dǎo)引，每一個定理采用已建立的推演、引理驅(qū)動重寫和簡化啟發(fā)式來自動證明;證明檢驗器有Coq、HOL、LEGO、LCF和Nuprl;復(fù)合證明器Analytica中將定理證明和符號代數(shù)系統(tǒng)Mathematica復(fù)合，PVS和Step將決策過程模型檢驗和交互式證明復(fù)合在一體。
• 模型檢驗是一種基于有限模型并檢驗該模型的期望特性的一種技術(shù)。粗略地講，檢驗就是狀態(tài)空間的蠻力搜索，模型的有限性確保了搜索可以終止。模型檢驗有兩種主要方法。其一是時態(tài)模型檢驗，該方法中規(guī)格以時態(tài)邏輯形式表述，系統(tǒng)模擬為有限狀態(tài)遷移系統(tǒng)。有效的搜索過程用來檢驗給定的有限狀態(tài)遷移系統(tǒng)是否是規(guī)格的一個模型。另一種方法中，規(guī)格以自動機方式給出，系統(tǒng)也模擬為一個自動機。系統(tǒng)的自動機模型和規(guī)格比較，以確定其行為是否與規(guī)格的自動機模型一致。基于模型檢驗的工具有描述語言為Promela 的SPIN和UPPAL等。

智能合約采用全生命周期的形式化驗證，在設(shè)計和開發(fā)過程都可用形式化驗證，代碼的形式化驗證在統(tǒng)一的環(huán)境可以采用源碼和編譯后的字節(jié)碼進行雙管齊下的驗證，源代碼進行轉(zhuǎn)換驗證，編譯后的字節(jié)碼進行反編譯驗證低級別性能，兩個驗證方法利用等價證明保證功能、運行上的一致。如以太坊可用在F*環(huán)境下進行驗證，反編譯字節(jié)驗證gas總量上限。

【本文是51CTO專欄作者“”李少鵬“”的原創(chuàng)文章，轉(zhuǎn)載請通過安全牛（微信公眾號id:gooann-sectv）獲取授權(quán)】

戳這里，看該作者更多好文