システムの正しさを確認するFormal Verification (形式的検証）についてのウェビナーが行われ、その参考資料を頂きましたのでその翻訳を共有します。
形式的検証(formal verification)は、ソフトウェアやハードウェアのシステムの正しさを数学的に証明する手法です。ブロックチェーンプロトコルの安全性と堅牢性を確保するための強力なツールであり、ブロックチェーン技術がより重要で価値のあるアプリケーションに採用されるにつれて、その重要性はますます高まってきています。
形式的検証の主な目的は、システムの正しさを数学的に証明する方法を提供することです。これは、システムの動作と特性を正式な数学的記述で表現し、自動化されたツールを使ってその記述が正しいことを検証することによって行われます。
形式的検証のプロセスは、システムが仕様に適合していること、ある種のエラーがないこと、ある種の攻撃に対して安全であることを証明するために使用することができます。
しかし、形式的検証は生成された仕様に対してのみ、アプリケーションの動作を検証することができることに留意することが重要です。形式検証では、仕様を適切に生成することが極めて重要です。仕様とは、システムの望ましい特性や動作を定義したもので、検証プロセスの基礎となるものです。もし仕様に誤りがあったり不完全であったりすると、検証プロセスはシステムの実際の特性や動作を正確に反映しない可能性があり、誤検出や誤否定につながります。したがって、検証プロセスを開始する前に、仕様が正確で、完全で、一貫性があることを確認しておくことが重要です。
例えば、新しい家を建てるとき、その家が構造的に正しく、必要な建築基準法をすべて満たしていることを確認したいとします。家の設計図が仕様であり、構造エンジニアが検証者です。もし設計図が不正確または不完全であれば、構造エンジニアは家の強度と安全性を適切に評価することができません。例えば、もし耐力壁の位置が設計図に記載されていなければ、エンジニアはその家が倒壊する危険性があることに気づかないかもしれません。同様に、形式的検証においても、仕様が不正確だったり不完全だったりすると、検証者はシステムの特性や挙動を十分に評価できず、重大な問題に発展する可能性があります。
形式的検証のために最も有望なブロックチェーンプロトコルの1つがCardanoです。Cardanoはセキュリティと形式的検証にも力を入れており、プロトコルの堅牢性と安全性を保証するのに役立っています。Cardanoチームは、形式的検証に適して特別に設計されたスマートコントラクトのプログラミング言語であるPlutusに取り組んできました。
Plutusは、Haskellをベースにした関数型プログラミング言語で、表現力、安全性、予測可能性を重視して設計されています。そのため、カルダノ・ブロックチェーン上に展開されるスマートコントラクトを書くのに適しています。
形式的検証は、開発者がスマートコントラクトのセマンティクスを形式的に表現し、自動化ツールを使ってそのセマンティクスが正しいかどうかをチェックすることを可能にします。これにより、Plutusで書かれたスマートコントラクトは、悪意のあるアクターが存在する場合でも、常に意図したとおりに動作することを証明することが可能になります。
スマートコントラクトの実行を様々なアプローチで保証する
ユニットテスト、プロパティベーステスト、形式的検証の3つは、スマートコントラクトの正しさと安全性を保証するために使用できる3つの異なる方法です。これらの方法はそれぞれ、スマートコントラクトの実行に対し異なるタイプの保証を提供します。
ユニットテスト：ユニットテストとは、関数やメソッドなど、コードの個々の単位をテストし、それらが期待通りに動作することを確認する手法のことです。ユニットテストは通常、開発者によって書かれ、コードが正しく動作していることを確認するために使用されます。
ユニットテストは、コードの個々のユニットが意図したとおりに動作し、コードへの変更が既存の機能を破壊しないことを保証するものです。
プロパティベーステスト：プロパティベーステストとは、システムが満たすべきプロパティのセットを指定することでシステムをテストする方法です。
そして、多数のランダムな入力を生成し、これらの入力すべてに対してシステムがプロパティを満たすかどうかをチェックすることでシステムをテストします。プロパティベースのテストは、様々な入力に対してシステムが正しく動作すること、またシステムの変更によって新たなバグが発生しないことを保証します。
形式的検証：形式的検証は、ソフトウェアやハードウェアのシステムの正しさを数学的に証明する手法です。スマートコントラクトのセキュリティと堅牢性を確保するための強力なツールです。形式的検証は、悪意のあるアクターが存在する場合でも、スマートコントラクトが常に意図
したとおりに動作することを保証するものです。これは、スマートコントラクトの動作とプロパティを形式的な数学的ステートメントとして表現し、自動化ツールを使ってこれらのステートメントが真であることを検証することで実現されます。
形式的検証におけるツールの役割
Isabelle、Coq、Agdaは、ソフトウェアやハードウェアシステムの形式的検証を行うために使用できる対話型の定理証明です。これらは、開発者がシステムの特性や動作を形式的な数学的言語で表現し、自動化されたツールを使ってその特性や動作が正しいことを検証できる形式的証明支援ツールです。
Isabelle: Isabelleは、汎用的な証明支援言語で、ほとんどのプログラミング言語の特性を捉えることができる強力な論理である高次論理（HOL）を含む幅広い論理をサポートしており、スマートコントラクトの特性を表現することに適しています。Isabelleを使用することで、開発者はスマートコントラクトのプロパティと動作を高次ロジック（HOL）と呼ばれる論理で表現し、Isabelleの自動定理証明機能を使用して仕様の一貫性と完全性をチェックすることができます。
Coq: Coqはもう一つの形式検証ツールで、開発者がシステムの特性や動作を正確かつ形式的に表現できる強力で表現力豊かな論理であるCalculus of Inductive Constructions (CIC) をサポートする対話型定理証明系です。Coqを使用することで、開発者はスマートコントラクトの特性や動作をCICで表現し、Coqの証明支援によりスマートコントラクトの特性の証明を記述・確認することができます。
Agda：Agdaは依存型プログラミング言語であり、対話型定理証明系です。開発者はデータや関数の型をより正確に表現することができます。これにより、スマートコントラクトをより正確に仕様化することができ、スマートコントラクトの特性についての推論が容易になり、それが正しいことを証明することが容易になります。また、Agdaには証明支援が組み込まれており、開発者はスマートコントラクトの特性の証明を記述したり、チェックしたりすることができます。
要約すると、Isabelle、Coq、Agdaは、ソフトウェアおよびハードウェアシステムの形式的検証を行うために使用できる対話型の定理証明系です。これらのツールにより、開発者はシステムの様々な特性や挙動を形式的な数学言語で表現し、自動化されたツールを用いて、それらの特性や挙動が正しいことを検証することができます。これにより、悪意のある行為者が存在する場合でも、スマートコントラクトが常に意図したとおりに動作することを証明することが可能になります。