正式な検証 — 数学的方法を使用して任意の数の入力にわたってプログラムまたはスマート コントラクトを「検査」するプロセス — は、一般的に、より高品質で安全なコードを記述するための従来のテストに代わる、より簡潔で包括的な代替手段と見なされています。 しかし実際には、正式な検証は自由でインタラクティブなプロセスです。 単体テストと同様に、開発者は正式な仕様を動的に定義してレイヤー化し、コードと分析の進化に合わせてアプローチを反復する必要があります。 さらに、正式な検証はその仕様と同じくらい効果的であり、仕様を記述するのに時間がかかる可能性があります (そして、多くの場合、急な学習曲線が伴います)。 

プロセスに困難を感じている多くの開発者にとって、単体テストは、多くの場合、プログラムの正確性を判断するための費用対効果と時間効率の高い方法です。 実際には、正式な検証は単体テストのより包括的な代替手段ではなく、補完的なものです。 これらのプロセスにはさまざまな長所と制限があり、一緒に使用するとさらに大きな保証が得られます。 開発者は常に単体テストを作成する必要があります — では、正式な検証に同じプロパティを使用できるとしたらどうでしょうか?

ハルモス、私たちのオープンソースの正式な検証ツールは、開発者が 再利用 記号テストによる形式仕様の単体テスト用に記述された同じプロパティ。 最初から堅牢な一連のプロパティを作成する必要はなく、開発者は重複作業を回避し、ゼロから始めることなく一度にいくつかの仕様をテストを改善できます。 このツールは、フォーマル検証プロセスの他のツールと一緒に、フォーマル検証への入り口として使用できるように設計されています。 開発者は、プロセスの後半でさらに追加する前に、最小限の労力でいくつかの分析から始めることができます。

この投稿では、フォーマル検証の課題と、単体テストとフォーマル検証の間のギャップをシンボリック テストで埋める可能性について説明します。 次に、既存のスマート コントラクト コードを使用して Halmos のデモを行い、開発者が利用できる他の正式な検証ツール (多くのオープン ソース) を簡単に見ていきます。

正式な検証とテスト

正式な確認 — 一般に、その厳密さと包括性のためにブロックチェーン開発者に好まれています — は、プログラムが特定の正しさの特性を満たしていることを検証することによって、プログラムの正しさを証明するプロセスです。 プログラムに固有のプロパティは、通常、外部から提供され、使用する検証ツールでサポートされている正式な言語または表記法を使用して表現されます。 開発者は、フォーマル検証を、考えられるすべてのシナリオでプロパティを自動的にテストするためのボタンを押すだけのソリューションと見なすことがよくありますが、実際には、フォーマル検証は労働集約的で高度にインタラクティブなプロセスになる可能性があります。

正式な検証と同様に、単体テストには、プログラムが期待どおりに機能するかどうかの評価が含まれます。 ただし、テストはプログラムの動作をチェックするだけです 一部 入力、フォーマル検証はそれをチェックできます を 可能な入力。 テストとフォーマル検証の両方で、プログラムの予想される動作の記述が必要です (テストではテスト ケースが使用され、フォーマル検証ではフォーマル仕様が使用されます)。 ただし、一緒に使用すると、プログラムをより徹底的に調べることができます。 たとえば、テストは単純なバグや間違いを見つけるのに効果的ですが、一般的にはより迅速かつ簡単に実行できます。 正式な検証は、使用するのが面倒ですが、エラーがないことを証明したり、テストやコード レビューで見落としがちな微妙なバグを明らかにしたりするのに十分強力です。

仕様のオーバーヘッド

正式な検証の主な課題の XNUMX つは、正式な仕様の記述と保守のオーバーヘッドです。 多くの場合、このプロセスには、特殊な言語 (多くの開発者が最初に学習する必要がある言語) を使用して手動で仕様を記述するという時間のかかる作業が伴います。 このプロセスも漸進的であり、通常は単純なプロパティを記述して検証することから始めて、徐々に複雑なプロパティを上に追加します。 テストと同様に、これは制限のないプロセスであり、明確な停止ポイントがなく、利用可能な時間枠内でできるだけ多くのプロパティのみを追加できます。 さらに、開発者が検証中にコードを変更すると、既存の仕様も更新する必要があり、余分なメンテナンス作業が必要になります。 これらの要因により、追加のオーバーヘッドにコミットすることをためらう一部の開発者にとって、正式な検証は困難な作業になる可能性があります。

また、テストと正式な検証を併用するとコードの品質を向上させることができますが、両方とも、異なる言語と形式でプログラムの予想される動作を (場合によっては同様に) 記述する必要があります。 これらの説明を書いて維持することは労力を要し、同じ説明の XNUMX つの異なる形式を維持することは、重複した作業のように感じられる場合があります。 これにより、次の疑問が生じます。開発者がテストと検証の両方に使用できる方法で、予想される動作を記述することは可能ですか?

シンボリック テストと Halmos を使用して、テストと正式な検証の間のギャップを埋める

シンボリック入力を使用してテストを実行するシンボリック テストは、仕様のオーバーヘッドを削減する効果的な正式な検証方法です。 このアプローチにより、テストと正式な検証の両方に同じテスト ケースを使用できます。 限られた入力セットに対してプログラムが正しく動作することを検証する従来のテストとは異なり、シンボリック テストでは、可能なすべての入力に対してプログラムがチェックされるため、シンボリック テストに合格したプログラムは正式に検証されたと見なすことができます。

Halmos は、シンボリック テスト用に設計された正式な検証ツールです。 個別の仕様を要求したり、新しい言語を学習したりする代わりに、Halmos は既存のテストを正式な仕様として使用します。 Halmos を介してテストを実行すると、可能なすべての入力に対してテストが合格することが自動的に検証されるか、反例が提供されます。 これにより、追加の仕様書を作成する必要がなくなるだけでなく、正式な検証の目的で、単体テストまたはファジング用に作成されたテストを再利用できます。

したがって、開発者は、現在のニーズに応じて、単体テスト、ファジング、正式な検証など、さまざまな品質保証オプションから柔軟に選択できます。 たとえば、ランダムな入力を生成するファザーの助けを借りて、単純な間違いをテストですばやく特定できます。Halmos を使用すると、すべての入力に対するプログラムの正確性に対する信頼をさらに高めることができます。

例: テスト isPowerOfTwo() function

例として、次のことを検討してください。 isPowerOfTwo() この関数は、与えられた数値が XNUMX のべき乗であるかどうかを判断します。 この関数は ビット操作アルゴリズム しかし、特に入力が XNUMX の累乗でない場合、その正しさを証明するのは困難な場合があります。

次のテストを想像してください isPowerOfTwo() 関数: 関数の実際の出力を、指定された入力に対する期待される出力と比較します。 これはパラメーター化されたテスト (プロパティ ベースのテストとも呼ばれます) です。つまり、Foundry などのファジング ツールを使用して、さまざまな入力値で簡単に実行できます。

このテストを使用して、 isPowerOfTwo() ユニットテストまたはファズテストを通じて機能し、選択した入力で実行します。 このようなテストは、可能なすべての入力に対してテストを実行することは計算上不可能であるため、関数の正しさを正式に証明することはできません。

ただし、Halmos を使用すると、開発者はこれらの既存のテストを公式の検証に再利用できます。追加の労力はわずかです。 このツールは、テストのシンボリック実行を実行し、アサーションが決して違反されていないことを検証することによって、可能なすべての入力に対してテストが合格することを確認します (または、アサーションが is 違反、反例を提供することにより）。 これは、テストが Halmos に合格した場合、関数の正確性が正式に検証されたことを意味します。これは、アルゴリズムが正しく実装され、コンパイラによってバイトコードに正確に変換されたことを意味します。

制限: 限定されたシンボリック実行

通常、完全に自動化された完全なシンボリック テストを実行することはできません。 止まる問題であることが知られています。 決められない. この理由の XNUMX つは、ループをシンボリックに反復する回数を自動的に決定することができないことが多いためです。 その結果、完全に自動化された正式な検証は一般的に判断できません。

これらの基本的な制限を考慮して、Halmos は完全性よりも自動化を優先します。 この目的のために、Halmos は、制限のないループ (反復回数はプログラムの入力に依存する) または可変長配列 (文字列を含む) に対して制限のあるシンボリック推論を実行するように設計されています。 これにより、完全性がいくらか犠牲になりますが、Halmos はユーザーがループ不変条件などの追加の注釈を提供する必要がなくなります。

たとえば、次の反復バージョンの isPowerOfTwo() この関数は無制限の while ループを備えており、ループの反復回数は、入力数値を表すのに必要な最小ビット数によって決定されます。

Halmos は、指定された境界までのみ、この無限ループを記号的に反復します。 たとえば、境界が 3 に設定されている場合、Halmos はループを最大 3 回反復し、ループを 3 回以上反復させる入力値 (つまり、2^3 以上の値) を考慮しません。 ）。 この特定のケースでは、境界を 256 以上に設定すると、Halmos を完全にすることができます。

デモ: Halmos を使用した ERC721A の正式な検証

Halmos の機能を実証するために、Halmos を使用して象徴的にテストし、正式に検証しました。 ERC721Aこれは、ERC721 標準の高度にガス最適化された実装であり、シングル ミントとほぼ同じコストでバッチ ミントを可能にします。 ERC721Aにはいくつかの革新的な機能が含まれています 最適化 この効率を達成するために; たとえば、ガスは、トークン所有権データの更新を、発行時ではなく、トークンが転送されるまで遅らせることで節約できます。 これには、複雑なデータ構造とアルゴリズムを使用して、遅延データ構造から所有権情報を効率的に取得する必要があります。 この最適化によりガス効率は向上しますが、コードの複雑さも増し、実装の正確性を証明することが困難になります。 これにより、ERC721A は、実装の信頼性を高め、潜在的なユーザーに利益をもたらす可能性があるため、正式な検証に適しています。

シンボリック テスト プロパティ

ERC721A の既存のテストは Hardhat を使用して JavaScript で記述されていたため (これは現在 Halmos ではサポートされていません)、主要なエントリ ポイント関数に対して Solidity で新しいテストを記述しました。 mint(), burn(), transfer(). これらのテストでは、各関数がトークンの所有権と残高を正しく更新し、他のユーザーの残高や所有権を変更することなく、関連するユーザーにのみ影響を与えることを確認しました。 後者は、ERC721A で遅延データ構造アルゴリズムが使用されているため、証明するのは簡単ではありません。 たとえば、次のテストでは、 transfer() 関数は、指定されたトークンの所有権を正しく更新します。

別のテストでは、 transfer() 関数は他のアドレスの残高を変更しません。これは、前述のように証明するのが困難です。

検証結果

ERC721A スマートコントラクトに Halmos を用いた検証実験を行い、合計 19テスト. テストは、Halmos を介して実行され、ループ アンローリング バウンドは 3 で、完了までに 16 分かかりました。 検証時間の内訳は、以下の表で確認できます。 実験は、M1 Pro チップと 16 GB のメモリを搭載した MacBook Pro で実施されました。

ほとんどのテストは数秒で完了しましたが、一部のテストは数分かかりました。 これらの時間のかかるテストは、考慮すべきケースの複雑な性質のために検証が困難であり、遅延データ構造アルゴリズムの正確さに密接に関連していました。

全体として、この実験の結果は、Halmos がスマート コントラクト コードの正確性を効果的に検証できることを示しています。 スマート コントラクトの複雑さと潜在的なエッジ ケースにもかかわらず、コードの整合性に対する信頼が高まります。

注入されたバグで実験する

Halmos の限定推論の有効性を実証するために、ERC721A コントラクトの以前のバージョンのバグを検出するためにそれを使用しました。 このバージョンには、算術オーバーフローの処理を誤るという問題があり、多数のトークンをバッチ ミンティングできる可能性がありました。これにより、遅延データ構造の整合性が損なわれ、一部のユーザーがトークンの所有権を失う可能性がありました (問題 解決 現在のバージョンで）。 バグのあるバージョンの ERC19A に対して同じ 721 のテスト セットを実行したところ、Halmos はその特性の反例を見つけることができました。 mint() 関数。 具体的には、Halmos は、上記のエクスプロイト シナリオにつながる入力値を提供しました。 この実験の結果は、その不完全性にもかかわらず、Halmos の制限付き推論が、スマート コントラクトの悪用可能なバグを検出および防止する効果的な方法である可能性があることを示しています。

関連作業

Ethereum スマート コントラクト バイトコードの正式な検証ツールは、さまざまなチームによって開発されています。 Halmos を含むこれらのツールは、スマート コントラクトのセキュリティと正確性を確保するために使用できます。 これらのツールのさまざまな機能、能力、および制限を比較して理解することは、開発者が独自のニーズに最も適したツールを選択するのに役立ちます。

Halmos は、スマート コントラクトの検証に使用できるツールセットに追加される貴重なツールですが、既存のツールを補完する (置き換えるのではなく) ことを目的としています。 開発者は、Halmos を他のツールと組み合わせて、契約のより高いレベルの保証を実現できます。 以下では、EVM バイトコードをサポートするいくつかの公式ツールと Halmos を比較します。

• K 演繹的検証とインタラクティブな定理証明を可能にする強力な正式検証フレームワークです。 その基礎となる理論と実装により、高度な表現力が提供されるため、複雑なプログラムやアルゴリズムの検証に適しています。 ただし、K は自動検証に重点を置いて設計されておらず、検証プロセス中に手作業が必要になる特定の自動化機能が欠けていることに注意してください。 K フレームワークを使用するには、正式な仕様が K 言語で記述されているため、使用する前に学習する必要があります。 その強みは、自動推論を使用した分析が困難な複雑なシステムの検証に特に役立ちます。
• セルトラ Halmos と同様に、自動化された検証に焦点を当て、境界モデルのチェックをサポートする、スマート コントラクト用の正式な検証ツールです。 Certora を使用するには、開発者は新しい言語を習得する必要があります。 CVL、仕様書を書くために。 この言語では、Halmos が現在サポートしていない機能であるコントラクト不変条件を使用して、多くの重要なプロパティを簡潔に記述することができます。 クローズド ソースのプロプライエタリ ツールであるにもかかわらず、Certora は堅牢な正式検証ツールを提供し、継続的な開発と優れたユーザー サポートを提供します。
  
  一方、Halmos はオープンソースのツールであり、規模が小さく、現在 Certora が提供する機能の一部が欠けていますが、公共財として機能することを意図しており、スマート コントラクトを迅速に検証するためのニッチ ソリューションとして意図されています。大規模なセットアップとメンテナンスの必要性。
• HEVM は、Halmos に似た別の正式な検証ツールです。 以前は、Foundry の前身である DappTools の一部でした。 HEVM と Halmos はどちらも個別の仕様を必要としないという特徴があり、アサーション違反を特定するために既存のテストをシンボリックに実行できます。 これにより、ユーザーは両方のツールを交互に使用したり、同じテストに対して並行して実行したりできるため、シンボリック テストの複数のオプションが提供されます。
  
  類似点にもかかわらず、HEVM と Halmos は独立して開発されており、実装の詳細が異なることに注意してください。 特に最適化と記号的推論戦略に関して。 さらに、HEVM は Haskell で記述されているのに対し、Halmos は Python で記述されているため、豊富な Python エコシステムを利用できます。 両方のツールを使用できるようにすることで、ユーザーは、スマート コントラクトのセキュリティと正確性を確保するための柔軟性とオプションを得ることができます。

ハルモス はオープン ソースであり、現在ベータ段階にあります。 新規事業にも積極的に取り組んでいます 機能を使用 Foundryチートコードやその他のいくつかの重要なユーザビリティ機能を含む機能。 どの機能が最も重要かについてのご意見をお待ちしております。また、Halmos をすべての人にとってより良いツールにするためのフィードバック、提案、および貢献を歓迎します。

**

ここに示されている見解は、引用された個々の AH Capital Management, LLC (「a16z」) の見解であり、a16z またはその関連会社の見解ではありません。 ここに含まれる特定の情報は、a16z が管理するファンドのポートフォリオ企業を含む第三者の情報源から入手したものです。 a16z は、信頼できると思われる情報源から取得したものですが、そのような情報を独自に検証しておらず、情報の現在または永続的な正確性、または特定の状況に対するその適切性について表明するものではありません。 さらに、このコンテンツにはサードパーティの広告が含まれる場合があります。 a16z はそのような広告を確認しておらず、そこに含まれる広告コンテンツを推奨していません。

このコンテンツは情報提供のみを目的として提供されており、法律、ビジネス、投資、または税務に関するアドバイスとして信頼されるべきではありません。 これらの問題については、ご自身のアドバイザーにご相談ください。 証券またはデジタル資産への言及は、説明のみを目的としたものであり、投資の推奨または投資顧問サービスの提供を構成するものではありません。 さらに、このコンテンツは、投資家または将来の投資家による使用を目的としたものではなく、a16zが管理するファンドへの投資を決定する際にいかなる状況においても信頼されない場合があります。 （a16zファンドへの投資の申し出は、私募覚書、サブスクリプション契約、およびそのようなファンドの他の関連文書によってのみ行われ、その全体を読む必要があります。）言及、参照、または記載されているのは、a16zが管理する車両へのすべての投資を代表するものではなく、投資が有益である、または将来行われる他の投資が同様の特性または結果をもたらすという保証はありません。 アンドリーセンホロウィッツが管理するファンドが行った投資のリスト（発行者がa16zに公開を許可していない投資、および公開されているデジタル資産への未発表の投資を除く）は、https：//a16z.com/investmentsで入手できます。 /。

記載されているチャートおよびグラフは、情報提供のみを目的としており、投資を決定する際に信頼することはできません。 過去の実績は将来の結果を示すものではありません。 内容は、示された日付の時点でのみ話されています。 これらの資料に記載されている予測、推定、予測、目標、見通し、および/または意見は、予告なしに変更される場合があり、他の人が表明した意見と異なる場合があります。 その他の重要な情報については、https：//a16z.com/disclosuresを参照してください。