智慧合約極大地擴充套件了區塊鏈的應用場景與現實意義，但頻發的安全事故嚴重阻礙了它的發展，智慧合約安全性問題的研究就顯得尤為關鍵。本文討論了形式化驗證、模糊測試和符號執行等主流的智慧合約漏洞檢測手段，對於象鏈科技當前聯盟鏈安全性問題的研究方向有著深遠的指導意義，並明確了下一步工作的目標，採用不同的檢測方法組合，著力提高漏洞挖掘的準確性、效率和自動化程度，滿足智慧合約規模和複雜度與日俱增的漏洞挖掘需求。
1智慧合約安全性問題
隨著智慧合約數量的增多，去中心化應用（Decentralized Application， DApp）的推廣，智慧合約涉及的數字資產呈指數級別增長。相比傳統軟體，智慧合約的安全問題更加棘手，現實情況也更加嚴峻。
1）智慧合約的可信度源自其不可篡改性，一旦被部署上線便無法修改。任何人都可對合約存在的安全漏洞發起攻擊，如果合約沒有相應的防禦措施，便將無法遏止安全問題的惡化，從而嚴重損害合約本身的經濟價值以及公眾對專案的信任。
2）很多專案會公開智慧合約原始碼。原始碼的公開透明雖能提升使用者對合約的信任度，卻也大幅度降低了駭客攻擊的成本，每一個暴露在開放網路上的智慧合約都有可能成為專業駭客團隊的金礦和攻擊目標。
3）智慧合約的開發過程存在紕漏。由於起步晚，發展時間短，智慧合約本身就有很多不足;同時市面上專業的技術人員嚴重匱乏，不嚴謹的程式碼參考、複製和修改等人為因素都會引起漏洞。
智慧合約中出現頻率最高的10類安全問題為分別：程式碼重入、訪問控制、整數溢位、未嚴格判斷不安全函式呼叫返回值、拒絕服務（Denial of Service， DoS）、可預測的隨機處理、競爭條件/非法預先交易、時間戳依賴、短地址攻擊以及其他未知漏洞型別。
2智慧合約漏洞檢測手段及相關工作
出於“程式碼即規則”，智慧合約一旦被部署便不可更改，即便有惡意交易被記錄下來，也不可以將其從區塊鏈中刪除。回滾交易的唯一方法是執行硬分叉，即透過修改區塊鏈中的共識協議把區塊鏈中的資料恢復到過去某一狀態，而這無法迴避開發者客觀上存在濫用“專業壟斷”的質疑，一定程度上衝擊了區塊鏈系統去中心化的理念。
因此必須在智慧合約上線之前，對其進行全面深入的程式碼安全審計與測試，充分分析潛在的安全威脅，儘可能規避漏洞。
針對智慧合約安全問題，應該從開發人員使用安全庫進行開發、安全團隊開展合約測試、合約審計這三個角度採取措施。
2.1 形式化驗證
形式化驗證用邏輯語言對智慧合約文件和程式碼進行形式化建模，透過嚴密的數學推理邏輯和證明，檢查智慧合約的功能正確性和安全屬性，克服了用傳統測試手段無法窮舉所有可能輸入的缺陷，能完全覆蓋程式碼的執行期行為，可以確保在一定範圍內的絕對正確，彌補了合約測試和合約審計工作的侷限性，因此形式化驗證已初步應用於高鐵、航天、核電等安全攸關的領域，並且取得了非常好的效果。
Bhargavan等提出了一個智慧合約分析和驗證框架，該框架透過Solidity*和EVM*工具將智慧合約原始碼和位元組碼轉化成函式程式語言F*，以便分析和驗證合約執行時安全性和功能正確性。目前，Coq、Isabelle/HOL、Why3等工具也實現了EVM的語義表示，並做了一些形式化驗證智慧合約的工作。
2.2 模糊測試
模糊測試是一種透過構造非預期的輸入資料並監視目標軟體在執行過程中的異常結果來發現軟體故障的方法。對智慧合約進行模糊測試時，利用隨機引擎生成大量的隨機資料，構成可執行交易，參考測試結果的反饋，隨機引擎動態調整生成的資料，從而探索儘可能多的智慧合約狀態空間。基於有限狀態機分析每一筆交易的狀態，檢測是否存在攻擊威脅。自動化工具Echidna採用了模糊測試技術來對EVM位元組碼進行檢測，但是不能保證API功能的穩定性。
2.3 符號執行
符號執行的核心思想是使用符號值代替具體值執行程式。對於程式分析過程中任意不確定值的變數，包括環境變數和輸入等，都可以用符號值代替。符號執行中的“執行”是指解析程式可執行路徑上的指令，根據其語義更新程式執行狀態，等同於解釋執行[19]。藉助符號執行檢測智慧合約漏洞的一般過程為，首先將按需將智慧合約中不確定值的變數符號化，然後逐條解釋執行程式中的指令，在解釋執行過程中更新執行狀態、蒐集路徑約束，並在分支節點處做fork執行，以完成程式中所有可執行路徑的探索，發現安全問題。約束求解技術能夠對符號執行中搜集的路徑約束進行求解，判斷路徑是否可達，並在特定的程式點上檢測變數的取值是否符合程式安全的規定或者可能滿足漏洞存在的條件。
2.4 汙點分析
本質上來說，汙點分析是針對汙點變數的資料流分析技術。汙點分析的一般流程為：首先識別汙點資訊在智慧合約中的產生點並對其進行標記;然後按照實際需求和汙點傳播規則進行前向或後向資料依賴分析，得到汙點的資料依賴和被依賴關係的指令集合;最終在一些關鍵的程式點檢查關鍵的操作是否會受到汙點資訊的影響。
3未來研究方向與改進思路
1）擴充套件形式化驗證的應用範圍。
對於目前學術界頗為關注的形式化驗證方法，用數學推演來驗證複雜系統，安全有效但難度很高。未來的研究應針對不同的業務目標定製對應的驗證規範描述，突破成本昂貴、不適應大規模合約等技術限制，並擴充套件形式化驗證的應用範圍，從驗證一般功能屬性和安全屬性、檢測常見漏洞到逐步實現經濟學、博弈論範疇中複雜業務邏輯及公平性等高階性質的證明。
2）提取重點路徑，縮減路徑空間。
基於攻擊者目標是非法竊取加密貨幣的假設，結合現有智慧合約審計經驗和已曝漏洞分析，尋找智慧合約中易產生漏洞的高危指令，如SUICIDE、CALL、ORIGIN、ASSERT_FAIL等，定義涉及這些操作碼的路徑為重點路徑。為了提高漏洞挖掘效率，實踐中不必對所有可能的執行路徑進行檢查，僅符合執行關注的重點路徑並進行漏洞驗證，可以有效地縮減路徑空間。
3）符號執行輔助的模糊測試。
現有的工具通常是對一種典型方法的具體實現，但是在執行具體漏洞挖掘任務時，因需求和重點不同，使用不同的輔助工具或者不同的檢測方法組合往往能達到更好的效果。
未來可以研究動態符號執行輔助的模糊測試技術，使用動態符號執行彌補模糊測試理解語義的缺失，推斷出到達特定程式狀態的約束條件，透過約束求解產生能夠觸發測試者所關注邏輯的合理輸入。據此恰當地改變模糊測試的輸入，提供額外的測試用例，觸發先前未覆蓋的程式碼區域，因此本文設計一種符號執行輔助的智慧合約模糊測試框架。
4）完善智慧合約漏洞庫，建立漏洞挖掘工具效率評價方法。
當前關於智慧合約的測試尚未有標準的案例集，因此，為了驗證智慧合約漏洞挖掘工具的有效性，同時給智慧合約的安全開發提供參考，下一步工作需要根據已爆發的安全事件以及合約審計經驗，總結歸納出涵蓋型別完善的智慧合約漏洞庫。
參考文獻：
[1] NCC Group. Decentralized application security project top 10 of 2018 [EB/OL]. （2018-07-08） [2018-09-08]. https：//www.dasp.co/index. html.
[2] SECBIT. Frequent smart contracts events， security development requires standardization [EB/OL]. （2018-05-07） [2018-10-20]. https：//www.jianshu.com/p/9d78f5110af1.
[3] MANNING A. Solidity security：comprehensive list of known attack vectors and common anti-patterns [EB/OL]. （2018-05-30） [2019-01-03]. https：//blog.sigmapri-me.io/solidity-security.html.
[4] ARIAS L， SPAGNUOLO F， GIORDANO F， et al. OpenZeppelin [EB/OL]. （2016-07-31）[2018-12-06]. https：//github.com/ OpenZeppelin/openzeppelin-Solidity.
[5] ATZEI N， BARTOLETTI M， CIMOLI T. A survey of attacks on Ethereum smart contracts （SoK） [C]// Proceedings of the 2017 International Conference on Principles of Security and Trust. Berlin：Springer， 2017：164-186.
[6] FEY G. Assessing system vulnerability using formal verification techniques[C]// Proceedings of the 2011 International Conference on Mathematical and Engineering Methods in Computer Science. Berlin：Springer， 2011：47-56.
[7] CSDN Research and Development Technology. Formal verification is a sharp weapon for smart contracts safety [EB/OL]. （2018-06-12） [2018-09-08]. https：//blog.csdn.net /CDLianan/article/details/80665162.
[8] BHARGAVAN K， SWAMY N， ZANELLA B S， et al. Formal verification of smart contracts：short paper[C]// Proceedings of the 2016 Association for Computing Machinery Workshop. New York：ACM， 2016：91-96.
[9] YANG X， YANG Z， SUN H Y， et al. Formal verification for Ethereum smart contract using Coq[J]. International Journal of Information and Communication Engineering， 2018， 12（6）：125-130
- END-
