形式検証企業Certoraは3日、ソラナ財団の委託を受けて実施したP-Tokenアップグレードの形式検証を完了し、技術ブログで結果を公開した。検証の結果、P-TokenはソラナSOLの既存トークンプログラム「SPL Token」のドロップイン置換として正しく機能することが証明され、悪用可能な脆弱性は発見されなかった。P-Tokenは5月にソラナメインネットへ実装済みで、今回の検証はその事後セキュリティ保証として位置づけられる。

形式検証の対象と意義

SPL Tokenプログラムは、ソラナ上のほぼ全ての代替可能トークンの発行、口座管理、転送などを担う中核プログラムである。Certoraによれば、SPL Tokenはソラナの全トランザクションの約半数に関与し、週次のトークン転送は数億件規模に達している。

P-Token（SIMD-0266）はPinocchioフレームワークを基盤としたSPL Tokenの再実装で、計算ユニット（CU）消費の大幅削減を目的に設計された。ソラナ公式アップグレードページによれば、命令によっては最大98%のCU削減が確認されており、Transfer命令は4,645 CUから76 CUへ、TransferCheckedは6,200 CUから105 CUへとそれぞれSPL Token消費量の約1.6%まで縮小されている。ネットワーク全体ではブロックスペース約10%の削減が見込まれている。

このアップグレードは既存ウォレットやDeFiプロトコルが修正なしで動作する「ドロップイン置換」として設計されているため、新旧プログラムの挙動が完全に等価であることを厳密に証明する必要があった。

3つの等価性プロパティと検証結果

Certoraは独自の形式検証ツール「Certora Solana Prover」を用い、CVLR（Certora Verification Language for Rust）で記述した仕様に基づき、SMT（充足可能性モデュロ理論）で全ての可能な入力に対する等価性を網羅的に検証した。検証対象は両プログラムが共有する全命令で、以下の3プロパティが定義された。

• No Panics：いずれのプログラムもパニック（異常終了）を起こさないこと
• Equivalence on Ok：SPL TokenがOk(())を返す場合、P-TokenもOk(())を返し、操作後のアカウント状態がバイト単位で同一であること
• Equivalence on Err：P-TokenがErr(e)を返す場合、SPL Tokenも同じエラーで失敗すること

検証の結果、対象範囲内の全命令で上記3プロパティすべてが成立し、悪用可能な脆弱性は発見されなかった。ただしP-Tokenが意図的に導入した3つの動作拡張（デリゲートの自己リボーク、Token-2022マルチシグ権限の受け入れ、零コピーローディングに伴うエラー順序の違い）については仕様として文書化され、形式仕様の仮定として明示的に取り扱われた。

ネットワーク全体への影響

P-Tokenには既存命令に加えて、batch（複数転送のバッチ化）、withdraw_excess_lamports（mint・マルチシグ口座からの余剰SOL回収）、unwrap_lamports（ネイティブSOLトークン口座からの直接送金）の3つの新規命令が追加されている。これらは検証対象範囲外だが、既存命令の等価性が形式的に保証されたことで、開発者やユーザーが安心して最適化プログラムへ移行できる環境が整った。検証結果と修正プロセスを含む詳細レポートは、Certora公式サイトで全文が公開されている。

関連：ソラナ新基盤SDPの決済パートナーにモダン・トレジャリー──マスターカードらも参加
関連：ソラナ財団、AIエージェント向け開発キット「Solana Agent Skills」発表

関連銘柄：SOL