DeFi專案正式部署前，透過合約的安全審計，不僅可以對專案的程式碼規範、漏洞情況以及業務邏輯等方面進行全域性核查。同時，專案審計對於專案方在投資市場的形象也具有一定塑造作用。
市場投資者在遴選專案時，如有專案方加持合約審計經歷，並對審計方、審計報告等資訊進行公開披露，投資可信度無疑會大幅提高。並且，專案方完善的安全立場建設意識，在無形中也將賦予專案額外的價值。
與此同時，DeFi專案方在運營過程中，保持與安全審計公司的長期業務合作，不論是對安全管理還是業務擴充套件都將大有裨益。畢竟，在專案長期發展過程中，階段性安全審計機制能夠及時發現和有效助力解決整體、區域性的風險問題。
那麼，DeFi合約審計的主要流程、內容以及特點，那些“套路”又是什麼呢？
套路一：前期“把脈”
與DeFi專案方的合約審計合作關係達成後，在瞭解專案整體情況，包括構架、業務設計等方面的基礎上，指派具有相關專案審計經驗的安全測試團隊進行專項服務，同時，明確專案檢測範圍以及相應需求側重點。做好前期“把脈”，其主要內容包括：
1、 DeFi專案方提供真實、有效且為審計所需的各項技術、程式碼、文件等資料。
2、 正式進入檢測環節前，安全團隊將對提供的材料進行全面評估，以確定週期。
3、 確定測試服務範圍，包括定向模組、區域性程式碼、全面安全審計等。
4、 完成相關需求對接，即對原始碼、應用程式、檔案資訊、測試環境的最終確認。
為了對DeFi專案合約的程式碼規範性、安全性以及業務邏輯等方面進行嚴格的安全審計，在測試明確後，處理合約審計的常規方式有：
·形式化驗證
·靜態分析
·動態分析
·典型案例
·人工稽覈
套路二：形式化驗證
形式化方法是實現安全、可信軟體的最可靠的手段，它利用基於數學的符號系統給出軟體正確性、安全性的嚴格定義和形式證明。其中，嚴格定義被稱為形式化規範，是一種用清晰、簡明的手段來刻畫軟體功能或特性的邏輯表示式。
在合約審計中，形式化方法透過的是定性需求屬性，從而證明程式不存在某類安全漏洞。另一方面，傳統測試方法則是透過檢查程式碼在一組選定的輸入上是否按照預期執行，以此說明程式是否存在安全漏洞，但這無法證明同型別安全漏洞不存在。
此外，傳統測試方法很容易漏掉在罕見或惡意構造場景下觸發的錯誤，以及由於大量“不可能事件”連續發生導致的錯誤。然而，形式化方法則可透過明確程式碼意圖、提供輸入空間的完整覆蓋來發現上述微妙錯誤，進而實現程式的安全性、可靠性增強。
成都鏈安創始人、多年形式化驗證研究專家楊霞教授表示，
“傳統驗證手段無法窮盡可能的情況，而形式化驗證則可以做到窮舉，對智慧合約漏洞檢測而言，該方法最為可信和有效。
作為針對以太坊智慧合約安全檢測開發的定製化工具，成都鏈安的Beosin-VaaS一鍵式智慧合約自動形式化驗證工具，可精確定位到含有風險的程式碼位置並指出風險原因，有效檢測智慧合約常規安全漏洞的精確度高達97%以上，為智慧合約程式碼提供‘軍事級’的安全驗證。”
套路三：程式碼規範審計
在程式碼規範審計中，主要測試專案有：
編譯器的版本問題可能會導致各種已知安全問題，開發者應在程式碼中指定合約程式碼採用最新的編譯器版本，並消除編譯器告警。
同時，Solidity智慧合約開發語言處於快速迭代中，部分關鍵字已被新版本的編譯器棄用，如throw、years等，為消除其可能導致的隱患，當前編譯器版本已經棄用的關鍵字應被禁用。
在智慧合約中，冗餘程式碼會降低程式碼可讀性，並可能需要消耗更多的gas用於合約部署，因此，必須找出並消除冗餘程式碼。此外，合約中是否正確使用SafeMath庫內的函式進行數學運算需要嚴格檢查。
Solidity使用狀態恢復異常來處理錯誤，該機制將會撤消對當前呼叫及其所有子呼叫中的狀態所做的所有更改，並向呼叫者標記錯誤。
函式assert和require可用於檢查條件並在條件不滿足時丟擲異常。assert函式只能用於測試內部錯誤，並檢查非變數。require函式用於確認條件有效性，例如輸入變數，或合約狀態變數是否滿足條件，或驗證外部合約呼叫的返回值。
以太坊虛擬機器執行合約程式碼需要消耗gas，當gas不足時，程式碼執行會丟擲out of gas異常，並撤銷所有狀態變更。合約開發者需要控制程式碼的gas消耗，避免因為gas不足導致函式執行一直失敗。
另外，合約函式的可見性是否符合設計要求，以及在當前合約中是否正確使用了fallback函式都需要進行嚴格檢查。
套路四：DeFi安全漏洞審計
目前，業務邏輯漏洞在DeFi專案中最為常見。由於專案業務邏輯設計的不嚴謹，極可能導致專案在特定情況下出現內部失衡。
需要注意的是，DeFi專案基於區塊鏈智慧合約開發，具有很多傳統金融體系以外的特性，比如：
·單筆交易可發起多個內部交易，失敗可回滾
·具有通縮性質的代幣
·合約程式碼不可修改
同時，審計中常見的還有合約許可權錯誤，即合約中函式的可見性修飾錯誤。通常，這是由於呼叫者和引數沒有進行有效驗證，導致函式被惡意使用者呼叫，從而釀成巨大的損失。
類似傳統安全問題，錯誤的許可權配置和無效的安全檢查都會給系統帶來巨大的風險。但不同的是，智慧合約的不可修改性使得此類問題即便被發現也不一定能得到有效修復。
另外，重入漏洞也是審計的重點。具體而言，當合約向外發起call呼叫後，攻擊者可利用合約呼叫的特性反覆呼叫函式，導致合約預期的執行順序發生錯誤，以此竊取目標賬戶的資產。
在審計中，程式碼錯誤出現頻率也很高。這主要是由於開發人員失誤導致的一些程式碼編寫錯誤。常見的有單位錯誤、忘記乘以精度、&使用錯誤等。在YAM漏洞事件中，程式碼在進行彈性調整rebase時，其程式碼正是忘記乘以精度，如圖所示：
在確保程式碼和漏洞深度檢測的同時，專案業務方面也設定有業務邏輯和實現方面的相關審計，包括對DeFi專案中涉及代幣基本資訊的檢查，以及代幣標準相關的函式的確認，特別是對鑄幣、銷燬代幣、更改owner及其它特殊許可權的審查和風險分析。
很多專案中都存在代理轉賬的邏輯，在處理此類邏輯時，很多專案方會直接要求使用者授權最大值代幣給專案方的合約，如下圖所示：
如此一來，合約就有權將使用者資金全部轉走。此外，還有雙重授權的問題，專案方網站在進行授權時，發起了兩筆授權，一筆授權給合約地址，一筆授權給外部地址，如使用者對此沒有提防，將會面臨極大的資金風險。
套路五：審計報告
合約審計最終服務於DeFi專案中的資金安全，而這方面諸多問題的出現都與函式、演算法的不當存在關聯。因此，合約審計就是要指出可能引發資金風險的內容，也就是潛藏隱患以及亟需修正的程式碼、漏洞、邏輯等問題。
在審計報告中，除了審計時間、歷時以及審計人等基本資訊外，還會體現對專案的投資預警提示。審計報告的核心內容，是體現受檢智慧合約在設計和程式碼實現等多方面、多維度的審計結果。同時，報告將指出發現的各類風險問題，並將其告知專案方以便修復。
透過審計報告，合約的風險成分，包括潛在可遭遇的攻擊，不同級別、層面的漏洞將被詳盡提示。只不過，安全審計報告中醒目的“透過”二字，不應該作為投資者僅有的投資判斷依據。
結語
合約審計並不屬於專案本身的利好訊息，而是上線前必要的一項安全工作，無論是對專案方還是投資者都具有重大的意義。
投機市場或是狂暴或是蕭條，行走其間不按套路出牌，終將也會受制於“套路”。略瞥其中，唯有防患於未然的安全之峰，巍然。
