本文為社群提交內容。作者為 Web3 智能合約審計公司 CertiK 的工程副總裁 David Tarditi。
摘要
智能合約的正式驗證可確保合約不會出現錯誤、漏洞和其他意外行為。一位人類專家會以數學式呈現智能合約的邏輯，然後透過自動化流程來執行合約，在該流程中針對合約的預期行為模型檢查實際邏輯。正式驗證和人工審計的結合可為智能合約的安全性提供全面評估。
前言
智能合約是部署在區塊鏈上的計算機程式，會在滿足某些條件時自動執行。它們的涵蓋範圍從簡單到極其複雜的內容，並且可持有價值數百萬甚至數十億美元的資產。
智能合約程式碼中的安全漏洞可能會產生毀滅性後果，包括竊取智能合約持有的全部資產。2021 年，由於智能合約中的一個錯字，自動做市商 (AMM) Uranium Finance 被盜取了 5,000 萬美元。
同樣在 2021 年，Compound Finance 由於一個字元錯誤而發出了 8,000 萬美元的非賺取獎勵。2022 年，由於其智能合約中的一個錯誤，Wormhole Bridge 被盜取了 3.2 億美元。
第一次就正確擬定智能合約程式非常重要。智能合約是開源的，代表一旦部署合約，該程式碼就可供公開使用。如果駭客發現錯誤，他們可以立即利用它。此外，隨著時間修補安全漏洞無法成為選項，因為智能合約的程式碼通常在部署後就無法修改。
智能合約驗證如何運作？
透過以數學式呈現智能合約的邏輯和所需行為，即可正式驗證智能合約。審計人員會接著使用自動化工具來檢查這些數學式是否正確。
此流程包含：
以正式語言定義合約的規範和所需屬性。
將合約的程式碼轉譯成正式表示法，如數學模型或邏輯。
使用自動化定理證明器或模型檢查器來驗證合約的規範和屬性。
重複驗證流程以尋找並修正所需屬性的任何錯誤或偏差。
為什麼智能合約驗證很重要
使用數學推理有助於確保通過正式驗證的智能合約不會出現錯誤、漏洞和其他意外行為。它還有助於增加對合約的信任和信心，因為其屬性已經過嚴格證明正確無誤。
以下是智能合約驗證如何幫助防止重大財務損失和其他災難性結果的一些範例。
Uniswap
Uniswap 是著名的 AMM。當 Uniswap V1 智能合約開發時，已通過正式驗證。在推出之前，此正式驗證已經發現並修復了可能導致 Uniswap V1 資金耗盡的進位錯誤。
Balancer
Balancer V2 也是通過正式驗證的 AMM。正式驗證已發現並修復了涉及智能合約中閃電貸功能的不正確費用計算，這個錯誤可能使交易所容易遭竊。
SafeMoon
SafeMoon V1 含有一個細微的錯誤，在其部署後由正式驗證發現。如果在放棄所有權前完成特定操作，擁有者就可以放棄合約的所有權，然後重新獲得合約所有權。
SafeMoon V1 分叉的人工審計沒有抓到這個錯誤，因為要抓到這個錯誤需要分析特定程式變數值組合。這是人類容易錯過而機器可輕易抓到的錯誤。
正式驗證和人工審計如何攜手合作
正式驗證提供系統化和自動化的方式，針對其所需的屬性來檢查合約的邏輯和行為。這使得識別和修復任何潛在錯誤更加容易。如果要透過人工檢查可能難以偵測的複雜細微問題，這個方式特別實用。
人工審計指由專家審查合約程式碼、設計和部署。審計人員運用他們的經驗和專業知識辨識安全風險，並評估合約的整體安全狀況。他們還可以確認正式驗證流程是否正確執行，並檢查是否有自動化工具可能未偵測到的任何問題。
結合正式驗證和人工審計可為智能合約的安全性提供全面且徹底的評估。這樣就有更多機會可以發現和修復任何漏洞。其結果就是利用人類和機器的特性來實現安全性的深度防禦方法。
總結
為了確保智能合約的安全性，必須同時使用正式驗證和人工審計，以確保對智能合約的安全狀態進行全面且徹底的評估。
雖然正式驗證可能會非常消耗資源，但對於具有高價值或高風險因素的合約來說，仍是一項值得的投資。總而言之，優先考慮安全性並確保智能合約沒有錯誤、漏洞和意外行為至關重要。
延伸閱讀
免責聲明和風險警告：本內容按「如實」原則呈現給您，僅用於一般資訊和教育目的，不作任何形式的陳述或保證。請勿將其視為財務建議，亦未企圖推薦購買任何特定產品或服務。數位資產價格可能會波動。您的投資價值可能會下跌或上漲，您可能無法收回投資金額。您要對自己的投資決策負全部責任，幣安學院對於您可能遭受的任何損失概不負責。本內容不應視為財務建議。