Certora完成Solana代幣擴展正式驗證，發現多項優化和安全改進

深潮 TechFlow 消息，區塊鏈安全公司Certora近日完成了對Solana代幣擴展的正式驗證審查，使用其深度形式驗證工具對代碼關鍵屬性進行了規範編寫和驗證。Certora團隊的主要發現包括：識別出一項可將程序性能提升20%的優化機會；開發了驗證Solana團隊近期更新的規則，以加強現有安全措施；編寫了可重用的規範，用於驗證多個指令，發現了之前所有審計人員都未察覺的問題。具體而言，Certora建議不使用sol_memcmp，而採用Rust提供的平臺無關比較方法，這一改進使TransferChecked指令的計算單元減少了約20%。此外，Certora的驗證還發現並確認了一個涉及未經檢查轉賬和經過檢查轉賬一致性的問題的修復。最後，團隊發現燒燬指令（Burn和BurnChecked）中缺少針對轉賬指令實施的修復，這一問題已得到SPL開發者的確認並修復。