Input Output が Cardano スマートコントラクト検証用の Blaster を実演

Cardano Community は、Cardano のスマートコントラクトが定められた規則に従っているかを検査するために設計された自動検証ツール Blaster のプレゼンテーションを公開した。Input Output のエンジニアである Romain Soulat と Jean-Frédéric Etienne は、ツールがそれらの特性をどのように調べ、違反を検出した際に反例を生成できるかを実演した。さらに、証明再構成に関する進行中の取り組みや、結果をより検査しやすくする方法についても議論した。

Cardano のコントラクトが何をすべきかを定義する

スマートコントラクトはブロックチェーン上のトランザクションに条件を設定し、アプリケーションが資産をどのように扱うかを決定する。例えば、開発者はコントラクトに保持された資金をアンロックできるのは認可されたユーザーだけだと定義する場合がある。形式検証は、仕様に記述された特性をシステムが満たしているかを数学的手法で確認する。従来のテストが選択した事例を調べるのに対し、形式検証はモデルで網羅される事例全体にわたって所与の特性が成り立つかを確かめることを目指す。

Cardano High Assurance のテクニカルリードである Soulat は、Blaster は証明作業の多くを自動化することを意図していると説明した。開発者は依然として、検査したい振る舞いを定義し、それに対応する仕様を用意する必要がある。ツールが違反を見つけると、検査用の反例を生成できる。Soulat は、認可されたユーザー以外の者が出力をアンロックしてしまうことを示すトランザクション、またはトランザクションの連なりを例示した。

Blaster がコントラクトの特性をどのように検査するか

Blaster は、数学的な命題の表現と証明操作のためのシステムである Lean 4 と、自動ソルバーを併用する。まず問題を単純化し、その段階で特性が解決されない場合は、残った問題をソルバーに送る。Cardano にとって意味のある検査にするため、チームはスクリプトの実行やトランザクション規則を含む、コントラクトが動作する環境の一部を形式化している。

シニアフォーマルメソッドエンジニアである Etienne は、考えられる結果は三つだと述べた。特性が有効、反証、または未確定として報告される。反証となった結果に付随する反例は、コントラクトのバグ、欠落した前提、仕様の誤りの特定に役立つ。未確定とは、特性が成り立つかどうかをソルバーが確定できなかったことを意味する。検査の範囲は、開発者が表現することを選んだ特性に依存する。

[NEWSBREAK]

証明再構成は開発中

開発者は、Plinth、Aiken、Plutarch などの言語で書かれたコントラクトを、Cardano のスクリプト実行に用いられる表現である Untyped Plutus Core にコンパイルできる。その後、コンパイル済みコードを Lean 4 に取り込み、検査する特性を指定できる。Input Output は以前、このプロセスのための Cardano 特有のモデルを提供するオープンソースライブラリを二つ公開している。過去のデモでは、チームはセキュリティチャレンジの練習用コントラクトにこのパイプラインを適用し、コントラクトがどのように悪用され得るかを示すトランザクションコンテキストを生成した。

Etienne は、証明再構成は依然として開発中だと説明した。目的は、有効とされた結果を支える根拠を Lean が独立に検査できるようにすることだ。現在のツールは、ソルバーがその結果を返した場合でも、再構成された Lean の証明をまだ生成しない。Soulat はまた、より明確な反例ビューの計画を示し、開発者が失敗した特性の背後にあるトランザクションの詳細を確認できるようにすると述べた。