最近のTechFlowからのニュースによると、ブロックチェーンセキュリティ企業であるCertoraがSolanaトークン拡張の形式検証レビューを完了しました。彼らは深い形式検証ツールを使用して主要なコードプロパティを記述および検証しました。Certoraチームの主な調査結果には、プログラムのパフォーマンスを20%向上させる機会を特定すること、Solanaの最新のアップデートのセキュリティ対策を強化するためのルールの開発、複数の命令を検証するための再利用可能な仕様の作成、すべての監査人によって以前に気付かれなかった問題を明らかにすることが含まれます。具体的には、Certoraはsol_memcmpの使用を避け、Rustのプラットフォームに依存しない比較方法を採用することを推奨しており、これによりTransferChecked命令の計算単位が約20%削減されます。さらに、Certoraの検証では、未検査の転送と検査済みの転送に関する整合性の問題の修正を発見および確認しました。最後に、チームはburn命令(BurnおよびBurnChecked)の転送命令の修正が不足していることを発見し、これはSPL開発者によって認識され修正されました。