十大智慧合約檢測工具優缺點分析

DeFi安全事件多與智慧合約撰寫有關，其中閃電貸攻擊及利用重入(Reentrancy)漏洞進行跨合約攻擊佔了多數，以dForce受到ERC777重入攻擊為例，Lendf.Me與imBTC兩個合約本身程式碼無安全問題，而兩者組合產生的協議帶來系統性的風險，此類可組合性對DeFi的發展有極大的安全隱患。

為了解決這個問題，目前已有一些智慧合約檢測工具，多用以檢查智慧合約中程式碼之漏洞，然而每種工具都有其優缺點，因此在實際運用時必須對其功能及特性有更深入的了解，本文也將為大家介紹及分析目前較為常見的十種智慧合約檢測工具。

用於智慧合約的靜態分析框架，可以生成抽象語法樹(AST)，可以用以查看合約函數的關聯，重入、含有kill()的合約等漏洞可以被檢測，但無法測gas消耗量。

可用於掃描基於EVM智慧合約中的漏洞，與乙太坊平台兼容，分析後會生成一份分析報告，但僅能測出部分漏洞。

會將分析出之漏洞對應編號，並可以顯示gas之消耗，儘管對於多數漏洞能夠辨識，仍無法對外部呼叫的合約或函數進行檢查。

對智慧合約進行符號分析，可以分析二進制文件和乙太坊智慧合約。
可以測重入但不能測有kill() 的合約，TOD、可見性也無法測出。

Securify 2.0 是以太坊基金會 和ChainSecurity所支援的以太坊智慧合約安全掃描器 ，可以對EVM字節碼及Solidity所編寫的合約進行安全分析，利用靜態分析智慧合約中的路徑，Securify2.0可以測出37個漏洞。

會指出智慧合約中漏洞並描述及闡述漏洞產生之原因，無法檢查程序錯誤，kill()及重入等都無法精準檢查。

為智慧合約模糊測試之工具，模糊測試是一種安全測試方法，將無效或隨機的值輸入到程式中，以獲得意外行為來識別錯誤和潛在漏洞。Echidna提供清晰的UI，可以針對錯誤進行深入分析，但不能檢查合約程序。

檢查可能引發安全的錯誤並可以調查每條函數實際執行的路徑，可以檢查重入但不能檢查有kill()的合約，對於一些嚴重錯誤會低估。

可以將EVM字節碼轉換為語意邏輯關係，分析效率相當快，但只能檢查出五種安全問題。

涉及數學相關的屬性無法充分檢查，對智慧合約程式碼提供靜態分析，將智慧合約程式碼和策略規範轉換為LLVM位程式碼以強化合約行為，但不一定可以找出跨函數重入漏洞。

以上為目前較為常見之合約檢測工具的簡短介紹，檢測工具雖然可以幫助開發者發現潛在漏洞，但對於「精準」找出正確的漏洞及檢查商業或營運邏輯仍然存在一定的局限性，因此目前多數的項目方在項目發布並上線之前，還是會將合約送交專業的審計公司進行審計來確保系統的安全性。
此外，也建議項目方在每次的升級前都應該再次送交審計，以確保系統的安全性及保護機制，可以避免來自惡意攻擊者的濫用，並且確保該系統能夠符合最新的安全及功能需求。

作者Alice目前為區塊鏈安全從業人員，將來也會持續在Vocus以及medium上分享相關的研究，如果喜歡我的文章歡迎追蹤我的帳號喔！

另外，我已經加入由趨勢科技防詐達人所成立的方格子專題－《區塊鏈生存守則》，在那裡我會跟其他優質的創作者一起帶大家深入瞭解區塊鏈，並隨時向大家更新區塊鏈資安事件

＞ 追蹤《區塊鏈生存守則》學習如何在區塊鏈的世界保護自己

＞ 關注防詐達人獲得其他最新詐騙情報