區(qū)塊鏈是一種分布式賬本技術，其通過提供業(yè)務交易和數(shù)字資產的一致性、不可變性來提高參與方的可信度，還能通過交易中提供更大的透明度來減少參與方之間的摩擦，這些特性使得更多行業(yè)的應用場景得以重塑。區(qū)塊鏈技術的快速發(fā)展，促使企業(yè)架構和技術創(chuàng)新的領導人開始重新思考分布式信任世界里的價值交換概念，同時也因之而滋生了眾多新技術。從下圖中能夠看出，目前還有許多技術尚處于科技誕生的促動期，如智能合約。
目前數(shù)字經濟正在向可編程經濟時代演進，區(qū)塊鏈技術支持著智能資產和智能合約以編程方式促進、核實或執(zhí)行合同條款，促使著可編程經濟的發(fā)展。智能合約對可編程經濟起著重要的推動作用，但在其應用卻面臨著種種問題。一直在跟蹤研究區(qū)塊鏈及其相關技術安全性問題的梆梆安全研究院，結合智能合約的技術發(fā)展歷程、應用特點和安全風險等，探索出了一套直指其核心本質的安全解決方案。
一、智能合約與區(qū)塊鏈完美結合，應用廣泛
第二代區(qū)塊鏈技術與第一代的顯著區(qū)別是智能合約的使用，梆梆安全研究院發(fā)現(xiàn)智能合約(Smart contract)這個術語在區(qū)塊鏈出現(xiàn)之前已出現(xiàn)，至少可以追溯到1995年，由多產的跨領域法律學者、受到廣泛贊譽的密碼學家尼克·薩博(Nick Szabo)所提出，他在發(fā)表于自己網站的幾篇文章中提到了智能合約理念，定義如下：
一個智能合約是一套以數(shù)字形式定義的承諾(promises)，包括合約參與方可以在上面執(zhí)行這些承諾的協(xié)議。
智能合約理念幾乎與互聯(lián)網(world wide web)同時出現(xiàn)，從本質上講，這些自動合約的工作原理類似于其它計算機程序的if-then語句，一種旨在以信息化方式傳播、驗證或執(zhí)行合同的計算機協(xié)議。允許在沒有第三方的情況下進行可信交易，這些交易可追蹤且不可逆轉。當一個預先編好的條件被觸發(fā)時，智能合約執(zhí)行相應的合同條款。
在計算機上進行智能合約實際應用時，需要控制實物資產保證有效地執(zhí)行合約，同時做到執(zhí)行合約條款時，能獲取到的第三方審核的合約方的信息，即需要解決信息傳遞與信任問題。
在無法建立信任關系的互聯(lián)網上，區(qū)塊鏈技術依靠密碼學和巧妙的分布式算法，無需借助任何第三方中心機構的介入，用數(shù)學的方法使參與者達成共識，保證交易記錄的存在性、合約的有效性以及身份的不可抵賴性，解決了互聯(lián)網上信任和價值傳遞，為智能合約的廣泛應用提供了絕佳的溫床。第二代區(qū)塊鏈開源項目——以太坊ethereum使用了智能合約，Linux基金會主導推動區(qū)塊鏈跨行業(yè)應用的開源項目——hyperledge也支持智能合約。智能合約使很多不同類型的程序和操作得以自動化，最明顯的體現(xiàn)之處在于支付環(huán)節(jié)及付款時的步驟操作。
2016年底由智能合約聯(lián)盟支持下編寫的數(shù)字商務商會的白皮書介紹了數(shù)字身份、抵押、供應鏈、癌癥研究等 12 項智能合約商業(yè)使用案例，目前智能合約已在金融、醫(yī)療等多個領域實際應用，坊間認為2017年是智能合約元年。
二、智能合約代碼漏洞越來越多，頻遭攻擊
隨著人們越來越多地了解區(qū)塊鏈技術，以太坊的熱度逐漸增加。然而，最新的研究顯示基于以太坊架構，被稱作是“最安全、最可靠、最方便”的智能合約技術卻漏洞百出。來自新加坡國立大學、新加坡耶魯大學學院和倫敦大學學院的一組研究人員發(fā)布了一份報告，聲稱已經發(fā)現(xiàn)了超過34，200個不安全的智能合約。他們還聲稱其中大約3000個不安全的智能合約可能會造成600萬美元的ETH被盜，具體發(fā)生的智能合約攻擊事件有：
2016年6月18日，TheDAO遭黑客發(fā)起Renntrancy攻擊，導致300多萬以太幣資產被分離出DAO資產給自己。
2017年7月21日，智能合約編碼公司警告1.5版本及之后的錢包軟件存在漏洞，Etherscan.io的數(shù)據(jù)確認有價值3000萬美元的15萬以太幣被盜;
2017年11月8日，錢包再現(xiàn)重大Bug，多重簽名漏洞被黑客利用，導致上億美元資金被凍結。
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ù)十億代幣被盜。
智能合約本質上是一段運行在區(qū)塊鏈網絡中的代碼，而代碼在設計和開發(fā)過程中，不可避免出現(xiàn)漏洞。部署在公鏈上的智能合約，由于暴露在開放網絡上，容易被黑客獲得，成為黑客的金礦和攻擊目標，造成無法彌補的損失。
三、形式化驗證方法保障智能合約安全
梆梆安全研究院在研究區(qū)塊鏈安全時發(fā)現(xiàn)，加強智能合約審計是提高區(qū)塊鏈安全的重要保證，其中形式化驗證是解決智能合約審計的一個有效方法。
所謂形式化驗證方法，即指在計算機科學領域，特別是軟件工程和硬件工程中，一種特殊的基于數(shù)學的技術，用于規(guī)范、開發(fā)和驗證軟件和硬件系統(tǒng)，以提高系統(tǒng)的安全性、可靠性和魯棒性。形式化方法可以形容為建立在相當廣泛的理論計算機科學基礎上的應用，特別是邏輯演算、形式語言、自動機理論、離散事件動態(tài)系統(tǒng)和程序的語義，還包括類型系統(tǒng)和代數(shù)數(shù)據(jù)類型等理論。一般這類研究主要應用于昂貴的航空、航天、軍事器材的操作系統(tǒng)、危險的醫(yī)療設備程序之中。
形式化驗證方法就是基于已建立的形式化規(guī)格，對所規(guī)格系統(tǒng)的相關特性進行分析和驗證，以評判系統(tǒng)是否滿足期望的特性。形式化驗證并不能完全確保系統(tǒng)的性能正確無誤，但是可以最大限度地理解和分析系統(tǒng)，并盡可能地發(fā)現(xiàn)其中不一致性、模糊性、不完備性等錯誤。形式化驗證可用來消除高風險代碼漏洞。
形式化驗證主要包括定理證明和模型驗證兩種技術：
現(xiàn)有的定理證明器包括：用戶導引自動推演工具、證明檢驗器和復合證明器。用戶導引自動推演工具有ACL2、Eves、LP、Nqthm、Reve和RRL，這些工具由引理或者定義序列導引，每一個定理采用已建立的推演、引理驅動重寫和簡化啟發(fā)式來自動證明;證明檢驗器有Coq、HOL、LEGO、LCF和Nuprl;復合證明器Analytica中將定理證明和符號代數(shù)系統(tǒng)Mathematica復合，PVS和Step將決策過程模型檢驗和交互式證明復合在一體。
模型檢驗是一種基于有限模型并檢驗該模型的期望特性的一種技術。粗略地講，檢驗就是狀態(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ī)格的自動機模型一致?；谀Ｐ蜋z驗的工具有描述語言為Promela 的SPIN和UPPAL等。
智能合約采用全生命周期的形式化驗證，在設計和開發(fā)過程都可用形式化驗證，代碼的形式化驗證在統(tǒng)一的環(huán)境可以采用源碼和編譯后的字節(jié)碼進行雙管齊下的驗證，源代碼進行轉換驗證，編譯后的字節(jié)碼進行反編譯驗證低級別性能，兩個驗證方法利用等價證明保證功能、運行上的一致。如以太坊可用在F*環(huán)境下進行驗證，反編譯字節(jié)驗證gas總量上限。
第三十四屆CIO班招生
國際CIO認證培訓
首席數(shù)據(jù)官（CDO）認證培訓
責編：kongwen
免責聲明：本網站（http://www.www.gypb.net/）內容主要來自原創(chuàng)、合作媒體供稿和第三方投稿，凡在本網站出現(xiàn)的信息，均僅供參考。本網站將盡力確保所提供信息的準確性及可靠性，但不保證有關資料的準確性及可靠性，讀者在使用前請進一步核實，并對任何自主決定的行為負責。本網站對有關資料所引致的錯誤、不確或遺漏，概不負任何法律責任。
本網站刊載的所有內容（包括但不僅限文字、圖片、LOGO、音頻、視頻、軟件、程序等）版權歸原作者所有。任何單位或個人認為本網站中的內容可能涉嫌侵犯其知識產權或存在不實內容時，請及時通知本站，予以刪除。
搶沙發(fā)
