IOGブログ記事「Applying formal methods at Input | Output: real-world examples」を公開し、Input Output（IO）がブロックチェーン技術、特にCardanoプロジェクトにおいてどのように「形式手法」を適用しているかを実例を交えて詳しく解説しています。形式手法とは、数学的根拠に基づいた技法を用いてシステムの正確性を証明するアプローチで、エラーが許されない環境で特に重要です。
この記事は、ブロックチェーン技術における形式手法の価値を深く理解し、それがもたらす安全性とスケーラビリティの向上を示すものです。特に、Cardanoの高い技術的基準とその継続的な進化に興味を持つ方々にとって、非常に有益な内容となっています。
形式手法の意義
IOは形式手法を活用して、設計段階から本番コードの開発までシステムの正確性を保証しています。これにより、高信頼性かつ安全なブロックチェーンソリューションを提供し、技術革新を促進しています。
形式手法の主要な実装例
1.仕様書（Specifications）
- システムの動作や特性を明確に定義。
- 例：「ADAの保存性」やステーブルコインのペッグ維持など。
- IOでは仕様書を実行可能にし、リファレンス実装やテストオラクルとして利用。
2.デジタルツイン
実システムと同じ挙動を再現する「デジタルツイン」を活用し、現実的な条件下での厳密なコードテストを実施。
3.形式検証済みの本番コード
AgdaやLeanといった形式検証ツールを活用し、スマートコントラクトや台帳コードを検証。
Cardanoプロジェクトでの活用事例
Cardano台帳層
ByronからConwayまで進化した台帳仕様は、Haskellで実行可能なリファレンス実装として提供されており、台帳の「価値の保存性」特性を保証。
Plutus Core
型付き・型なしのスマートコントラクト言語であるPlutus Coreは形式化され、最適化も実施。
現在、90,000以上のスマートコントラクトが稼働。
Cardanoネットワーク層
ネットワークプロトコルはHaskellの型システムを活用して正確性を保証。
2,200日以上の無停止稼働を実現。
Agda2hs
Agdaを使用して形式仕様と整合性のあるHaskellコードを生成。
Ouroboros Perasプロジェクトやウォレットコード検証に利用。
重要なメッセージ
形式手法は、システムの設計段階から本番環境まで、その安全性と信頼性を担保するための強力なツールです。IOはこの手法をCardanoプロジェクトに深く統合することで、技術的課題を克服しつつ、ブロックチェーン技術の発展に寄与しています。
以下はIOGブログ記事「Applying formal methods at Input | Output: real-world examples」を翻訳したものです。
Input | Outputにおけるフォーマルメソッドの適用：実例
Input | Outputにおけるフォーマルメソッドの適用：実例
エラーの影響が大きい環境において、IOはフォーマルメソッドを活用し、数学的に裏付けられた安全なブロックチェーンソリューションを提供しています。IOにおけるフォーマルメソッドに関する2部構成のブログの第2回では、実際の実装例についてより深く掘り下げます。
2024年11月26日 James Chapman 読了時間：8分
前回のブログ記事では、フォーマルメソッドとブロックチェーン開発における役割について説明しました。
フォーマルメソッドの重要性を踏まえ、Input | Output（IO）は実例を通じてその実践的な適用を示しています。これらの手法を開発プロセスに統合することで、IOはブロックチェーン技術におけるイノベーションを推進する堅牢で高い保証のあるシステムを実現しています。
IOにおけるフォーマルメソッドの実装
IOはCardanoの開発に貢献する際、システムのコアコンポーネントの機能的および非機能的な正確性について強力な保証を得るためにフォーマルメソッドを使用しています。
IOの戦略には以下が含まれます：
- 研究段階から早期に関与し、研究者と協力して結果を形式化する
- プロジェクトとともに成長し変化できる形式的な成果物（仕様、モデル、プロトタイプ、本番実装）を開発する
- プロジェクトに応じて形式化のレベルを調整する
- 継続的インテグレーション（CI）とテストを通じて開発ワークフローにフォーマルメソッドを組み込む
- 開発後期段階以降も関与を継続する
一般的に使用される3つの手法があります：
- 仕様
- デジタルツイン/形式的に検証されたモデル
- 形式的に検証された本番コード
仕様
仕様を作成することは不可欠です。システムがどのように機能することを意図しているかの概要を提供するためです。システムがどのように動作するべきかを指定しなければ、期待通りに動作しているかをテストすることはできません。仕様はシステムの設計と、満たすべき主要な特性と要件に対応します。例えば、ステーブルコインシステムでは、ペッグの維持が重要な特性となります。同時に、Cardanoレジャーでは、通常のシステム運用中にadaが誤って作成または破壊されないことが重要です – これは「adaの保存」として知られる特性です。
IOの仕様は単なるドキュメントを超えています – それらは実行可能で、本番実装を検証するためのリファレンス実装とテストオラクルとして機能します。IOのエンジニアは、adaの保存特性などのリファレンス実装の重要な特性も証明します。これにより、オリジナルの設計に忠実で、基本的な特性を捉えた、実際のシステムやコンポーネントの現実的なリファレンスバージョンが提供されます。また、設計特性がコードの保証に変換されることも確保されます。
デジタルツイン
デジタルツインと呼ばれることが多いこのセットアップは、実際のシステムのクローンのように機能し、同一の動作をするように設計されています。これは、IOのエンジニアがCardanoノードで広範に使用している適合性テストの概念を捉えており、現実的な「実験室条件」でコードを厳密にテストすることを可能にします。
形式的に検証された本番コード
次のステップは、リファレンス実装を本番で使用すること、あるいはむしろ本番コードを検証することです。これには、最高レベルの保証を提供する、完全に詳細化された高性能な検証済みコードが必要です。このアプローチは、Leanの定理証明器を活用してスマートコントラクトコードを検証するPlutus High Assuranceなどのプロジェクトで積極的に追求されています。Plutus Coreは既に本番コードの検証の恩恵を受けており、Agda定理証明器から生成されたコードが本番ツールチェーンで使用されています。Cardano財団も、まだデプロイされていないウォレットの本番コードを検証するためにagda2hsを使用しています。
Chrome関連のブラウザを使用してこの記事を読んでいる場合、おそらく検証済みの暗号コードを使用していることになります – これはIOも調査している分野です。
バランスの取れたアプローチ
異なるシステムや異なるコンポーネントでどの程度精密な手法を使用すべきかについては、バランスを取る必要があります。これは、コンポーネントの重要性、失敗した場合の結果、およびドメインがフォーマルメソッドにどの程度適しているかによって異なります。プロジェクトごとに異なります。幸いなことに、スタンドアロンの仕様、プロパティベースのテスト、モデル検査、静的解析、定理証明のための型、形式的に検証されたコードなど、様々なフォーマルメソッドのツールと方法論が利用可能です。目標は、プログラマーがプログラム、その要件、不変条件、保証を完全に定義し、それらすべてを機械的にチェックできるようにすることです。形式化のレベルは、必要性と適用可能性に基づいて調整されます。
以下でいくつかの例を見てみましょう。
[図1]は、ブロックのサイズがインターネット上での転送遅延にどのように影響するかを示しています。
上記の図は、ブロックサイズがインターネット上での転送遅延にどのように影響するかを示しています。
以下の台帳ルールの例は、トランザクションがバランスしているか、入力が未使用であるかなどを確認するものです。このルールはAgdaで形式化されており、整合性テストのための参照ドキュメントおよび参照実装として機能します。
[図2]のレジャールールの例は、トランザクションが残高を保ち、入力が未使用であることなどをチェックします。このルールはAgdaで形式化されており、適合性テストのためのリファレンスドキュメントおよびリファレンス実装として機能します。
[図3]の機械的に検証された定理は、レジャーが価値の保存を満たすことを示しています。これは、トランザクションが処理される前後でシステム内のadaの総量が同じであることを示しています。
フォーマルメソッドは急速に進化する分野であることに注目する価値があります。昨日は特異だったものが、今日では一般的になっています。可能な限り、時間を節約し、可能な限り強力な保証を確保するために、自動化された方法とツールのサポートを使用することが不可欠です。
Cardanoに適用されたフォーマルメソッドの例 to Cardano
Cardanoレジャー層
Cardanoレジャーの仕様は、ByronのためのレトロスペクティブなLaTeX仕様から始まり、Shelley開発以降と並行して進化してきました。Conway レジャー時代では、Agda仕様が使用されています。フォーマルメソッドは、レジャーの重要な特性、特に「価値の保存」を証明するのに役立ちます。これは、レジャーの状態が新しいブロックで更新される際にadaが誤って作成されたり破壊されたりしないことを保証します。仕様は読み取り用のPDFと実行用のHaskellにコンパイルされます。これは、本番実装に対する適合性テストのためのリファレンス実装として機能します。現在まで、このプロセスで失敗は発生していません。
Plutus Core
型付きおよび型なしPlutus Coreの形式化があり、これは仕様とリファレンス実装として機能します。フォーマルメソッドのエンジニアは、型の保存と進行の特性を証明し、スマートコントラクトの実行が停止しないこと、および型の消去が動作に影響を与えないことを保証します。型なしPlutus Coreの主要な最適化も検証され、結果のコードは本番コンパイラに統合されます。これは特に、型システムがコンパイラ開発者に限定的なサポートしか提供しない領域で重要です。現在、Cardanoは90,000以上のスマートコントラクト、160,000のネイティブアセットポリシー、700mのada（TVL）をホストしています。
[図4]は、型なしPlutus Coreの本質的に整理された制御、環境、継続（CEK）マシンの内部構造を示しています。
Figure 4. Plutus Core CEK machine
Cardanoネットワーク層
IOはパフォーマンスモデリングを使用して、パフォーマンスの範囲を決定し、Cardanoネットワークパラメータを設定します。型付きプロトコルは、実装における正確なプロトコル遵守を保証し、Haskellの型システムによって保証が提供されるため、追加の証明は必要ありません。ネットワーク層は2,200日以上の中断のないアップタイムを維持しています。
Agda2hs
IOのフォーマルメソッドチーム、デルフト工科大学、エディンバラ大学、チャルマース工科大学の研究者との共同で、検証済みHaskellコードを書くためのDSLを作成し、The Haskell Symposium 2022で発表しました。このツールはPlutusのテストジェネレータの検証に使用されており、一部の特性はテストするよりも証明する方が容易です。このツールはOuroboros Perasでも使用され、形式的な仕様に対して健全性が検証された検証済みHaskellテストモデルを定義します。さらに、このツールはCardano財団がウォレットコードを検証するために使用しており、IOのエンジニアはAgdaのRustバックエンドも構築しています。
[図5]は、agda2hsの検証済みプログラムの例を示しています。左側には、木の不変条件を維持することが保証された挿入と二分探索木の注釈付きコードが表示されています。この場合、特性は本質的に保証されており、追加の証明は必要ありません。右側には、注釈が削除された後の生成されたHaskellコードが表示されています。
Figure 5. Example of a verified Haskell program in agda2hs
Plutus High Assurance
Plutus High Assuranceでは、フォーマルメソッドチームはLeanでツールを開発しており、スマートコントラクト開発者が1回のクリックで特定の種類の問題を自動的に排除し、実際のコードで直接カスタム特性を証明できるようにしています。
Ouroboros Peras
Perasプロジェクトでは、IOはAgdaでのプロトコルの形式的な仕様、agda2hsを使用して生成された検証済みテストモデル、投票の拡散のパフォーマンスモデル、リテラルAgdaで書かれたCardano改善提案（CIP）、仕様に対して適合性テストされるHaskellのプロトタイプ実装を導入しています。Ouroboros Perasの次のフェーズはIntersectを通じて進行中で、科学論文が完成間近であり、Perasは2025年にメインネットでのローンチが予定されています。
Figure 6. Ouroboros Peras methodology
[図6]は、Perasプロジェクトの方法論が設計を仕様と実装にどのように接続しているかを示しています。
最後に
IOは、Cardanoプロジェクトでの広範な使用を通じてフォーマルメソッドの価値を証明しており、形式的な仕様と検証プロセスが重要な問題を特定し防止してきました。開発ライフサイクルにフォーマルメソッドを組み込むことで、IOはシステムが高い保証で目標を達成することを確実にし、より安全でスケーラブルなブロックチェーンソリューションへの道を開いています。
