Breakpoint 2023: Safe SBF Programsセッションのまとめ
この記事はSolana Advent Calendar 2023 13日目の記事です。
本記事ではBreakpoint 2023のSafe SBF Programsセッションの動画をChatGPTでテキスト化を行った記事になります。動画を見る時間がない、視覚優位で動画が苦手、動画の補助としてテキストと両方みたいという方向けになります。
元のTranscriptの品質、ChatGPTの精度により不正確な記述がありえることにご注意ください。
セッションの概要
本セッションでは、分散型金融（DeFi）分野におけるスマートコントラクトのセキュリティを強化する方法として、「形式的検証」を取り上げます。まず、形式的検証の定義、その重要性、そして実施にあたって直面する課題について詳しく説明します。その上で、複雑なDeFiのコードの安全性を確保している企業の実践的なアプローチと技術について紹介し、安全なプロトコルの開発への理解を深めることを目指します。
加えて、ライブデモンストレーションを用いて、形式的検証手法を実践的に理解できるように、マルチシグウォレットのセキュリティ検証を事例として紹介します。最後には、形式的検証の将来の展望についても議論します。
セッションのハイライト
スマートコントラクトのセキュリティ向上: 分散型金融（DeFi）において中心となるスマートコントラクトの安全性確保が大きな課題であり、ハッキングや盗難の増加がこれを示している。CA社は形式的検証という数学的な手法を用いてプログラムの信頼性を保証し、セキュリティ向上を目指している。
形式的検証の障害と革新: 形式的検証の実行には複雑な仕様の記述や論理構造の抽出が必要であり、この困難さを解決するためにCA社は開発者向けに使用が容易な新しい言語と自動化ツールの開発を進めている。
マルチシグウォレットの事例研究: セキュリティ面で重要なマルチシグネチャウォレットの検証を行い、そのプロセスには「Prover」という検証ツールやスクワッドマルチシグウォレット検証などの具体例がある。これにより、DeFiプロトコルの不変条件の検証が可能となり、安全性と正確さが強化される。
セッション内容
はじめに
本日の議題は、分散型金融（DeFi）におけるスマートコントラクトの安全性向上策についてです。セキュリティは暗号通貨の広範な普及を阻む重要な課題ですが、DeFiはこれがとくに問題になっています。この点を強調するため、過去6年から7年間で盗難された暗号通貨の量やハッキングの件数が増加しているデータをご紹介します。
私たちの企業（CA社）が推奨する対策は「形式的検証」の採用です。これは与えられたプログラムPが特定の仕様Sを満たしていることを数学的証明で示す手法か、もしくは仕様に反する具体例を発見する方法です。この手法はプログラムの信頼性を保証するものであり、同時に不具合を特定して修正する際にも利用できます。
しかし、形式的検証には実行に際して幾つかの困難が伴います。実際には仕様の記述が複雑で、長い時間がかかる上、プログラムの論理構造を抽出する作業は簡単ではありません。これを解決するため、私たちは開発者が仕様を容易に記述できるような新しい言語とツールを提供し、形式的検証のプロセスを自動化するためのツールの開発を進めています。この戦略で、DeFiプログラムの安全性を大幅に向上させることが目的です。
暗号資産とDeFiにおけるセキュリティの課題
Seror株式会社は、2018年の設立以来、瞬く間に世界的な影響力を持つ企業へと成長しました。当社では、EVMの分野で豊富な実績を誇り、SolidityやVyperで開発された200万行を超えるコードの検証経験を有しています。この専門知識を活かし、プルリクエストが実装される事前段階での膨大なバグの特定と予防に貢献してきたことが、当社の重要な業績の1つです。とくに2022年には、当社の焦点をSolanaに移行することで、分野を拡大しました。
コードの安全性を確保するために、与えられたコードとその仕様、および「不変条件」と称する要素に着目し、これらを「Prover」という専用ツールで検証します。このツールはコードの安全性の証明を構築し、脆弱性や弱点を発見すると、それを報告します。ただし、問題が決定不能なケースは存在し、そういった場合はタイムアウトを迎えることがあります。当社では、最新のテクノロジーを用いながら、ソフトウェアの安全性と品質を高めるサービスを提供することに努めております。
形式的検証という解決策
当社は、システムのタイムアウト発生を防止することを重点的に取り組んでいます。
次に、Solanaプラットフォームの検証方法に焦点を当てます。Solanaでの検証には複数の抽象レベルがあり、どのレベルで検証作業を行うかを選択する必要があります。一般的なアプローチとして、Rust言語の中間表現（Intermediate Representation, IR）レベルでの検証があります。このレベルでは、検証に役立つ型、ポインタ、所有権情報などが豊富に提供されます。しかし、この方法ではSolana仮想マシン（SVM）の細部が見過ごされる可能性があります。
代替手段として、LLVMビットコードレベルでの検証も考慮されますが、これも同様にSVMの特有の要素を見落とすリスクがあります。ソースコードがない場合やLLVM以外の言語で書かれている場合でも対応可能なのはSolanaバイナリ形式（Solana Binary Format, SBF）レベルの検証です。SBFレベルでの検証はSVMの全ての詳細を考慮に入れる利点があり、コンパイラやコード生成のバグを発見する際にも有用です。これにより、コンパイラを盲信する必要がなくなります。
ただし、このアプローチはコンパイルの過程で多くの情報が失われるため、複雑さが増します。Solanaのバイトコードを理解するためには、仮想マシンの構成を簡潔に示した図を用いることが有効です。この図はレジスターやスタック、ヒープ、アカウント関連情報を扱う4つの異なるメモリ領域を表します。しかしながら、私たちは高レベルの抽象化を重視せず、低レベルでの徹底した検証を実践しています。
Certoraのアプローチと背景
私たちのチームは、パブリックリレーションズの取り組みを最大限に活用するためのパイプラインを開発しました。このパイプラインは、Rustというプログラミング言語で記述された仕様に基づいたオリジナルのRustコードを扱うことが主な目的です。また、C言語など他のプログラミング言語による入力にも対応していますが、重点はRustに置かれています。
処理過程において、コードはAlanコンパイラによって変換され、Albanビットコードとして出力されます。その後、最終的な成果物としてSBFファイルが生成されます。このSBFファイルは、我々のツールが分析するための入力データとして用いられ、ここで逆コンパイルのプロセスを遂行します。このプロセスを通じて、我々はコードの動作をより深く理解し、その知見をPR活動に役立てることを目的としています。
検証パイプラインと抽象化レヴェル
該当のプロセスでは、まず失われたポインタ情報や型情報などの膨大な情報を復元する作業を行います。復元された情報は内部表現へと変換され、これによりプログラムの意味論を体現する公式の形成が可能になります。
次に、市販されている満足可能性問題モジュロ理論（SMT）ソルバーを使用し、公式の充足可能性を検証します。この検証結果を通じて、対象とするRAS契約が仕様に沿った安全かつ正確なものであるかどうかを判断します。
以上が、本プロセスの概要になります。目的は、RAS契約の安全性と正確さを確認することです。
事例研究：スクワッドマルチシグウォレットの検証
本日は、当社が保有する独自の技術の重要性を再確認していただくために、関連する取り組みについてご説明いたします。当社の技術チームは、デコンパイルや逆コンパイルといった技術の特性に適応するため、複雑な式の設計と開発にとくに多大な労力を割いてまいりました。
次に、具体例としてケーススタディを紹介します。2ヶ月前、Squatsプロジェクトとの共同作業を開始しました。Squatsの最新版であるバージョン4は、6億ドル以上の資産を保護する高度なマルチシグネチャウォレットであり、細心の注意を払って作成されており、複数の手動監査を経ています。
当該プロジェクトでは、マルチシグネチャコンポーネントや提案メカニズムなど、プロトコルのいくつかの重要な側面について正式な検証を行うことが私たちの責務でした。これには、タイムロック機能をはじめとする新たな機能の統合も含まれます。
今から、これらの詳細をさらに分かりやすく説明していきます。
ライブデモンストレーション：検証プロセス
当社は、提案のメカニズムを精緻化する過程にあります。このシステムは、マルチシグネチャという概念に基づいて構築されており、トランザクションに対して複数のメンバーの承認が事前に必要とされます。このプロセスにおいては、トランザクションを実施するかどうかを決定するために、特定の閾値が設けられています。
一般的な流れは以下の通りです。まず、提案者が提案を作成します。その後、投票者がこの提案に賛成するか反対するか投票し、提案が所定の支持を集めた場合にのみ、最終的な実行に移されます。このメカニズムは意思決定をより正式で慎重なものにすることを目的としています。
結論と今後の展望
本プレゼンテーションでは、提案されたメカニズムの概念的な機能を説明しました。このメカニズムにおける各状態を黒い箱で、特定の状態を緑の箱で表現し、それらの間の遷移を他の要素で示しています。
まず、メカニズムを活用するためには「proposal_activate」関数を活用し、次に提案に対する投票として「proposal_reject」または「proposal_approve」を適用します。提案が設定された閾値を達成すると、承認され実行される可能性がある一方、取り消される場合もあります。
本メカニズムの検証では、提示したオートマトンの遷移が完全であるか、全ての状態が到達可能で「デッド」状態が存在しないか、重複投票が排除されているかなど、複数の特性を検証することが重要です。
ライブデモでは、これらの性質をどのように証明するかを紹介しました。具体的には、検証対象となる性質に合わせた環境である「検証ハーネス」を用いてシミュレーションを行い、メンバーの提案承認や拒否といった挙動を再現します。実施後は望ましい性質が保持されていることを検証し、提案の承認時には閾値に相応する数の承認が得られていることを確認します。
その上で、決定不能性問題に対処しながら、SBFファイルを処理し規則を検証するスクリプトの実行方法を説明しました。検証ハーネスと通常のテストハーネスの差異を強調し、非決定的な値生成に依存し全てのシナリオを象徴的に網羅する検証ハーネスの利点を明らかにしました。
検証結果として性質の保持と違反の無さを公表し、バグが存在する状況下での挙動も示しました。
本プレゼンテーションの目的は、SBFコードを形式的に検証するツールを紹介し、セキュリティ保証の強化を提供することであり、興味を持つクライアントへの協力とツールの機能向上に努めることを目指しています。
ご理解とご関心を賜り、ありがとうございました。
セッションのまとめ
本セッションでは、分散型金融（DeFi）におけるスマートコントラクトの安全性を高める手段として、形式的検証の活用が取り上げられました。形式的検証は、数学的な証明手法を使ってプログラムの正確性を検証し、エラーを発見し修正する効率的なアプローチです。ただし、形式的検証の実施は複雑さと時間を要するという問題を抱えています。
この問題に対処するため、新たなプログラミング言語とツールの開発が進められています。具体的には、マルチシグネチャウォレットに関するケーススタディや、新たに提案されるメカニズムの検証プロセスが詳述されました。
将来的には、形式的検証ツールを駆使してDeFiのセキュリティを確保し、機能を拡張することが期待されています。
みんな大好き形式手法の話でした。どうしてもSolanaのプログラム（スマートコントラクト）開発ではRustの静的型付けだけではカバーしきれない範囲があるため、気になっている分野だったのでとても面白いセッションでした。
合わせていくつか記事も見つけたのでよければどうぞ。
この記事が気に入ったらサポートをしてみませんか？