形式化驗證——合約安全的終局解決方案
發表於 2023-09-12 09:49 作者： 金色財經
作者：@dvzhangtz；來源：作者推特@dvzhangtz
最近看了一些形式化驗證的項目，感覺在新周期中其依舊會是有趣的敘事。
但該技術作爲合約安全中最重要的組成，卻在推上幾乎看不到中文帖。所以總結了一下學習中得到的認知...
現在，你可以用五分鐘拿走這些認知。
背景：智能合約是區塊鏈世界核心之一，合約發生安全問題，Dapp 中的錢就全部涼涼。 根據 Rekt 榜上可以看到，因爲合約安全造成的直接損失單次最高達 $ 600M，間接損失更加嚴重，合約不安全會令社區對項目失去信心。 https://rekt.news/leaderboard/
傳統上如果爲了讓合約更安全，思路是疊甲，比如：
1 使用標准函數包如 @OpenZeppelin 的包來寫代碼，讓代碼更安全
2 寫完後使用一些工具進行初步篩查，看有沒有問題
3 寫一些測試程序，對合約分模塊用樣本數據測試
4 ......
但鎧甲再厚也總會有漏洞，測試程序也只能用一些樣本進行測試，不可能窮盡所有可能性。所以這些方法都只能降低出現安全問題的可能性，不能保證合約沒有問題 有沒有一種辦法能像預言家驗狼人一樣，能確保合約沒有某方面安全漏洞？ 答案是——形式化驗證
想進行一次形式化驗證，需要幾步：
1. 寫形式化規範，裏面定義我們想要驗證的東西
2. 使用形式化分析框架驗證，這類工具會自動驗證合約是否符合我們定義的規範
3. 發現某些情況下出現問題
4. 改代碼解決問題
一個真實案例：巫師決鬥 @CHZWZRDS
https://github.com/dapperlabs/cheezyverse/blob/fef271db4c18c00949de291da0b46a1397216306/contracts/BasicTournament.sol#L2059…
下面的代碼時說：在遊戲超時時，巫師 1 會吸走巫師 2 的能量，巫師 2 能量清零。
作爲一個 gamefi，這個能量自然很重要。
理論上這個能量只能在兩個巫師之間轉移，但如果黑客發現這段程序的漏洞，可以讓能量憑空增加 / 消失，無疑會對這個 Gamefi 造成重大影響。
使用正常的安全驗證方式，我們用了幾個測試數據，發現一切都運行的很 nice，我們甚至准備直接上鏈部署了。 不過等等，爲什么不試試形式化驗證？
第一步：定義形式化規範
我們希望能量只會在巫師之間相互轉移，不會憑空增加/消失，也就是： wiz1.power + wiz2.power = old_wiz1.power + old_wiz2.power 。
第二步：形式化分析框架自動驗證
這類工具實質上是一種用於探索合約執行的所有可能路徑的技術，以確保在所有可能的執行路徑上都滿足規範。
第三步：發現問題
發現了一個問題！一個神奇的問題，如果決鬥的兩個巫師是一個人，也就是決鬥雙方的地址一致，就會讓該用戶的能量清零！ 第四步：改正問題 既然發現了問題，其實很容易改，我們只需要加一行代碼，預先審核，確保決鬥雙方不是一個人就好啦～
類似的問題還有經典的 K 值校驗問題。Uniswap 的核心是恆定乘積模型 K=x*y，其中的 K 值是該 pair 合約持有代幣數量的乘積，且要求之後的每一筆交易完成後 K 值須增加(手續費) 如果有黑客發現了合約中的漏洞，可以使得自己的交易不用符合恆定乘積，這樣合約就是提款機了，用上文思路也可避免該問題。
從上文可以感受到形式化驗證的幾個特點：
1. 終局性：在所驗證問題上可以證出合約不存在某些問題；
2. 對規範的依賴(嚴重)：上文只是驗證了一個規範，但實際合約會面臨的問題很多，我們可能會漏掉某些規範，而書寫規範本身也是比較耗人力的，所以形式化驗證主要是對合約一些關鍵屬性進行驗證。
3. 性能問題(嚴重)：使用形式化分析框架自動驗證，本質上是探索合約執行的所有可能路徑上都符合規範，這有可能會遇到狀態爆炸和路徑爆炸問題，同時其底層使用 SMT 求解器和其他約束求解器，這些求解器也是耗算力的大戶。 所以，未來將這件事以一個什么樣的方式外包出去降低成本，也許能促進其發展。
如果想進行形式化驗證，相關工具如下：
書寫形式化規範的語言
Act: https://github.com/ethereum/act
Scribble: https://docs.scribble.codes
Dafny: https://github.com/dafny-lang/dafny…
用於檢驗正確性的驗證器
Certora Prover: https://docs.certora.com/en/latest/index.html…
Solidity SMTChecker: https://github.com/ethereum/solidity…
solc-verify: https://github.com/SRI-CSL/solidity…
KEVM: https://github.com/runtimeverification/evm-semantics…
標題：形式化驗證——合約安全的終局解決方案
地址：https://www.coinsdeep.com/article/43382.html
鄭重聲明：本文版權歸原作者所有，轉載文章僅為傳播信息之目的，不構成任何投資建議，如有侵權行為，請第一時間聯絡我們修改或刪除，多謝。