什麼是智能合約的形式驗證？

2023-11-18 22:41 更新

本文由社群成員發佈。作者為David Tarditi，一家Web3智能合約審計公司CertiK的工程副總裁。

摘要

智慧合約進行形式驗證可避免它們出現錯誤、漏洞和其他不利的情況。在這個過程中，人類專家會將智慧合約的邏輯轉換為數學語句，然後透過自動化流程對照合約預期行為的模型檢查實際邏輯。將形式化驗證和人工審計結合，我們就可以對智慧合約的安全性進行全面評估。

簡介

智慧合約是部署在區塊鏈上的電腦程式，在滿足某些條件時會自動運作。智能合約可能非常簡單，也可能極其複雜，可以持有價值數百萬甚至數十億美元的資產。

智慧合約代碼如果有安全漏洞，就可能造成毀滅性後果，例如被不法分子竊取其持有的所有資產。 2021年，由於智能合約中的一個拼字錯誤，自動做市商(AMM)Uranium Finance被盜取了5,000萬美元。

同樣在2021年，由於單一代碼錯誤，Compound Finance錯誤發放了8000萬美元的獎勵。 2022年，因智能合約出現一個錯誤，Wormhole Bridge被偷走3.2億美元。

因此，一開始就把智能合約程式弄對很重要。智能合約採用開源模式，這意味著一旦合約部署後，程式碼就會公開。如果駭客發現其中的錯誤，就可以立即加以利用。此外，隨著時間的推移修補安全漏洞的常規操作派不上用場，因為智慧合約的程式碼在部署後通常無法修改。

智慧合約驗證是如何運作的？

智能合約的形式驗證是透過將智能合約的邏輯和預期行為呈現為數學語句來實現的。隨後，審計師會使用自動化工具檢查這些語句是否正確。

過程涉及：

運用數學推理，有助於確保經過形式化驗證的智能合約避免錯誤、漏洞和其他不利的情況。驗證也有助於增加對合約的信賴和信心，因為其特性已經過了嚴格檢驗，正確可靠。

以下這些範例大致說明了智能合約驗證如何幫助防止重大財務損失和其他災難性後果。

SafeMoon

大多數對SafeMoon V1分叉的人工審計都遺漏了這個錯誤，因為需要分析程式變數值的特定組合才能發現這個錯誤。人類很容易錯過這個問題，但機器卻能及時捕捉到它。

形式化驗證提供了一種系統化、自動化的辦法，來根據合約的預期特性檢查合約的邏輯和行為。這樣可以更輕鬆地識別和修復任何潛在的錯誤或漏洞。這對於人工檢查難以發現的複雜、細微的問題特別有用。

人工審計則包括專家對合約的程式碼、設計和部署進行審查。審計師會利用自己的經驗和專業知識，來識別安全風險並評估合約的整體安全狀況。他們還可以確認形式化驗證過程是否正確執行，並檢查是否有自動化工具可能無法檢測到的任何問題。

將形式化驗證和人工審計結合，我們就可以對智能合約的安全性進行全面評估。這可以提高發現和修復任何漏洞的幾率。這樣一來，我們就相當於採用了一種結合人類和機器各自專長的深度防禦安全措施。

為了確保智能合約的安全性，必須將形式化驗證和人工審計相結合，從而確保對智能合約的安全態勢進行全面而徹底的評估。

雖然形式化驗證對資源消耗較高，但對於具有高價值或高風險因素的合約來說，這是一項值得的投資。畢竟歸根結底，安全重於泰山，一定要優先考慮安全性並確保智能合約遠離錯誤、漏洞和不利的意外行為。