Cardano高保証

取り組みを支えるチーム

この機会について

Cardanoは自動形式検証が本番規模で機能することをすでに証明しています。IOのLean 4向け形式検証ツールBlasterは、DjedやUSDCxを含む本番dAppの正確性特性を証明し、一般的なCardanoの脆弱性を完全に自動化された方法で検出する能力を実証しました。これは真の競争優位性であり、この取り組みはそれをエコシステム内のすべての開発者に広げることを目的としています。

スケールアップの準備ができている2つの能力があります。第一に形式検証自体：Blasterは現在、個々のスクリプトで動作し、専門知識の恩恵を受けています。機会は、完全なdAppレベルの検証への拡張、複数のスマートコントラクト言語への統合、VS Codeなど馴染みのある開発者ツールを通じたアクセシビリティの向上にあります。第二に開発者環境：経験豊富なエンジニアも最初のコントラクトコードを書く前にツールとライブラリの設定に多大な時間を費やしています。コンテナ化されたあらかじめ設定された環境により、そのような摩擦が解消され、初日から高保証ツールキットの全機能をすぐに利用できるようになります。

イニシアティブ

Cardano高保証

この提案は、Cardano高保証の傘下にある2つの密接に補完し合うワークストリームに資金を提供します。

ワークストリーム1：Blaster形式検証。BlasterをシングルコントラクトからフルDAppレベルの検証へと拡張します。Aiken（Midgard Labsと共同）、Pebble（Harmonic Labsと共同）、Scalus（Lantrと共同）、Futura（SAIBと共同）の4つのスマートコントラクト言語に形式検証を統合します。ビジュアルな反例探索機能を備えたVisual Studio Code拡張機能、主要なDAppカテゴリ向けの事前構築済みプロパティテンプレートを含む共通脆弱性ライブラリ、2つのUPLCプログラムが意味的に同一であることを形式的に証明する等価性チェックツール、およびBlasterを信頼済みコードベースから除外する証明再構成モジュール（TxPipeおよびNo.Witness Labsと共同）を提供します。
ワークストリーム2：高保証ツールキット向け開発者環境。完全なPlinthツールチェーン（コンパイラ、ライブラリ、プロパティベーステスト、静的解析、形式検証、プロファイリング）を検証済みの互換バージョンですべて含む、シングルコマンドで事前設定されたコンテナベース開発者環境（CBDE）を提供します。また、IOの高保証ツールをcardano-init（TWGA 1で資金提供される場合）に統合し、各ツールの事前設定とテンプレートにより簡単に開始できるようにします。

形式検証ワークストリームはコンソーシアムとして構成されています。Lantr、Harmonic Labs、SAIB、Midgard Labs、No.Witness Labs、TxPipeがそれぞれ定義された作業パッケージを担当し、デリバリーと長期メンテナンスの責任をエコシステム全体に分散させています。IOは深いプロトコル知識とBlasterの検証コアを提供し、各パートナーは専任の運用フォーカスと独自の開発者コミュニティをもたらします。

トレジャリー要求額：₳13,078,578

誰が構築しているか

この取り組みは、Input OutputのStefano LeoneとRomain Soulatが主導し、エコシステムのコラボレーターのコンソーシアムであるLantr、Harmonic Labs、SAIB、Midgard Labs、No.Witness Labs、TxPipeと共に進めています。

「Cardanoの強みは、常に正確性にあります。本提案はそれを高価な例外ではなく、デフォルトにするものです。ワンクリックで、すべての開発者に、5つの言語で。」

Stefano LeoneInitiative Owner

「Cardanoエコシステムが必要としているのは監査だけではありません。すべての開発者が自身のワークフローで手に届く検証ツールが必要です。Blasterはまさにそれを実現し、自動形式検証をCardano上での構築の第一級要素にしています。No.Witness Labsでは、それを次世代の高品質保証dAppの基盤と見ており、だからこそDevXと汎用セキュリティプロパティの作業パッケージに貢献しています。」

Jonathan RodriguezCo-Founder, No.Witness Labs

「自動形式検証ツール「Blaster」により、Cardanoスマートコントラクトの重要なセキュリティ特性を明示・数学的に証明することが可能となり、テストだけでは到達できないレベルの保証を提供します。プロパティベーステストと比較して、形式的証明は格段に強力です。サンプリングされたケースではなく、あらゆる入力パターンに対して正確性を保証するため、より堅牢でセキュアなコントラクトの実現につながります。TxPipeでは、開発フェーズ・監査フェーズの双方において、この手法が高い信頼性をもたらしています。」

Manu Guntherテクニカルチームリーダー、TxPipe

期待される成果

自動形式検証が単一コントラクトから完全なdAppレベルのプロトコル検証へと拡張され、Aiken、Pebble、Scalus、Futuraの開発者が証明された正確性特性にアクセスできるようになります。
視覚的な反例探索とソースレベルの検証フィードバックを備え、形式検証を開発者のIDEに直接もたらすVS Code拡張機能。
開発者がアグレッシブなUPLC最適化を適用しながら、動作が変わらないことを機械検証済みの証明で確認できる等価性チェックツール。
DEX、レンディングプロトコル、ブリッジなどの主要なDAppカテゴリ向けに、監査パートナーとの共同制作による既製のプロパティテンプレートを備えた共通脆弱性ライブラリ。
現在の数日間のセットアッププロセスを60秒の初期化に変換し、完全なPlinthツールチェーンが事前設定され使用可能な状態のコンテナ化開発者環境（CBDE）。