フォーマル検証

ウィキペディアから、無料の百科事典
ナビゲーションにジャンプ 検索にジャンプ

ハードウェアおよびソフトウェアシステムのコンテキストでは、フォーマル検証は、数学のフォーマルな方法を使用して、特定のフォーマルな仕様またはプロパティに関して、システムの基礎となる意図されたアルゴリズムの正当性を証明または反証する行為です[1]

フォーマル検証は、暗号化プロトコル組み合わせ回路、内部メモリを備えたデジタル回路、ソースコードとして表現されたソフトウェア などのシステムの正当性を証明するのに役立ちます。

これらのシステムの検証は、システムの抽象的な数学的モデルに関する正式な証明を提供することによって行われます。数学的モデルとシステムの性質との対応は、他の方法では構築によって知られています。システムのモデル化によく使用される数学的オブジェクトの例は、有限状態マシンラベル付き遷移システムペトリネットベクトル加算システム時限オートマトンハイブリッドオートマトンプロセス代数、操作的意味論表示的意味論などのプログラミング言語の形式的意味論です公理的意味論ホーア論理[2]

アプローチ

1つのアプローチと形成は、モデル検査です。これは、数学モデルの体系的な徹底的な調査で構成されます(これは、有限モデルでも可能ですが、抽象化を使用したり、を利用したりすることで、無限の状態セットを効果的に有限に表現できる一部の無限モデルでも可能です。対称)。通常、これは、スマートでドメイン固有の抽象化手法を使用して、単一の操作で状態のグループ全体を検討し、計算時間を短縮することにより、モデル内のすべての状態と遷移を探索することで構成されます。実装手法には、状態空間列挙、記号状態空間列挙、抽象解釈記号シミュレーション、抽象化の改良が含まれます。[必要な引用] 検証されるプロパティは、線形時相論理(LTL)、プロパティ仕様言語(PSL)、SystemVerilogアサーション(SVA)、[3]計算ツリーロジック(CTL)などの時相論理で記述されることがよくあります。モデル検査の大きな利点は、多くの場合完全に自動化されていることです。その主な欠点は、一般的に大規模なシステムに拡張できないことです。シンボリックモデルは通常、数百ビットの状態に制限されますが、明示的な状態列挙では、探索される状態空間を比較的小さくする必要があります。

別のアプローチは演繹的検証です。これは、システムとその仕様(および場合によっては他の注釈)から数学的証明義務のコレクションを生成し、その真実はシステムがその仕様に準拠していることを意味し、いずれかの証明アシスタント(対話型定理証明者)を使用してこれらの義務を履行することで構成されます(HOLACL2IsabelleCoqPVSなど)、または自動定理証明器(特に満足度モジュロ理論を含む)(SMT)ソルバー。このアプローチには、システムが正しく機能する理由をユーザーが詳細に理解し、証明される一連の定理の形式または仕様の形式でこの情報を検証システムに伝達する必要があるという欠点があります(システムコンポーネント(関数やプロシージャなど)およびおそらくサブコンポーネント(ループやデータ構造など)の不変条件、前提条件、事後条件)。

ソフトウェア

ソフトウェアプログラムのフォーマル検証には、プログラムがその動作のフォーマル仕様を満たしていることを証明することが含まれます。形式的検証のサブエリアには、演繹的検証(上記を参照)、抽象解釈自動定理証明型システム、および軽量形式手法が含まれます。有望な型ベースの検証アプローチは、依存型プログラミングであり、関数の型にはそれらの関数の仕様(少なくとも一部)が含まれ、コードの型チェックにより、それらの仕様に対する正確性が確立されます。フル機能の依存型言語は、特殊なケースとして演繹的検証をサポートします。

もう1つの補完的なアプローチは、プログラムの導出です。このプログラムでは、一連の正確性を維持する手順によって、機能仕様から効率的なコードが生成されます。このアプローチの例は、Bird-Meertens形式であり、このアプローチは、構築による別の形式の正当性と見なすことができます。

これらの手法は、検証されたプロパティがセマンティクスから論理的に推測できることを意味する健全な場合もあれば、そのような保証がないことを意味する不健全な場合もあります。サウンドテクニックは、可能性の空間全体をカバーした後にのみ結果を生み出します。不健全な手法の例は、可能性のサブセットのみ、たとえば特定の数までの整数のみをカバーし、「十分な」結果をもたらす手法です。手法は決定可能である場合もあります。つまり、アルゴリズムの実装は回答で終了することが保証されているか、決定不可能であり、決して終了しない可能性があります。それらは制限されているため、不健全な手法は、健全な手法よりも決定可能である可能性が高くなります。

検証と妥当性確認

検証は、製品の目的への適合性をテストする1つの側面です。検証は補完的な側面です。多くの場合、全体的なチェックプロセスをV&Vと呼びます。

  • 検証:「私たちは正しいものを作ろうとしていますか?」、つまり、製品はユーザーの実際のニーズに合わせて指定されていますか?
  • 検証:「作成しようとしていたものを作成しましたか?」、つまり、製品は仕様に準拠していますか?

検証プロセスは、静的/構造的および動的/動作の側面で構成されます。たとえば、ソフトウェア製品の場合、ソースコードを検査し(静的)、特定のテストケースに対して実行できます(動的)。検証は通常、動的にのみ実行できます。つまり、製品は、典型的な使用法と非典型的な使用法を使用してテストされます(「すべてのユースケースを十分に満たしていますか?」)。

自動プログラム修復

プログラムの修復は、生成された修正の検証に使用されるプログラムの目的の機能を含む、オラクルに関して実行されます。簡単な例はテストスイートです。入力/出力のペアがプログラムの機能を指定します。さまざまな手法が採用されており、特に、満足度モジュロ理論(SMT)ソルバー[4]遺伝的プログラミング[5]を使用して、進化的計算を使用して修正の候補を生成および評価します。前者の方法は決定論的ですが、後者はランダム化されます。

プログラム修復は、フォーマル検証とプログラム合成の手法を組み合わせたものです。フォーマル検証でのフォールトローカリゼーション手法を使用して、合成モジュールの対象となる可能性のあるバグの場所である可能性のあるプログラムポイントを計算します。修復システムは、検索スペースを減らすために、事前定義された小さなクラスのバグに焦点を合わせることがよくあります。既存の技術の計算コストのために、産業用途は制限されています。

業界での使用

設計の複雑さが増すにつれて、ハードウェア業界におけるフォーマル検証手法の重要性が増しています。[6] [7]現在、フォーマル検証はほとんどまたはすべての主要なハードウェア企業によって使用されていますが[8]ソフトウェア業界での使用は依然として低迷しています。[要出典]これは、エラーがより商業的に重要であるハードウェア業界でのより大きなニーズに起因する可能性があります。[要出典]コンポーネント間の潜在的な微妙な相互作用のために、シミュレーションによって現実的な可能性のセットを実行することはますます困難になっています。ハードウェア設計の重要な側面は、自動証明方法に対応しているため、フォーマル検証の導入が容易になり、生産性が向上します。[9]

2011年の時点で、いくつかのオペレーティングシステムが正式に検証されています。NICTAのSecure Embedded L4マイクロカーネル。OKLabsからseL4として商業的に販売されています。[10]華東師範大学によるOSEK / VDXベースのリアルタイムオペレーティングシステムORIENTAIS [要出典] Green HillsSoftwareのIntegrityオペレーティングシステム; [要出典]SYSGOPikeOS[11] [12]

2016年の時点で、イェール大学とコロンビア大学のZhongShao教授とRonghuiGu教授は、CertiKOSと呼ばれるブロックチェーンのフォーマル検証プロトコルを開発しました。[13]このプログラムは、ブロックチェーンの世界でのフォーマル検証の最初の例であり、セキュリティプログラムとして明示的に使用されているフォーマル検証の例です。[14]

2017年の時点で、フォーマル検証は、ネットワークの数学的モデル[16]を通じて、また新しいネットワークテクノロジカテゴリであるインテントベースのネットワーキングの一部として、大規模なコンピュータネットワークの設計に適用されています[15] 。[17]フォーマル検証ソリューションを提供するネットワークソフトウェアベンダーには、Cisco [18] Forward Networks [19] [20]およびVeriflowSystemsが含まれます。[21]

CompCert Cコンパイラは、ISOCの大部分を実装するフォーマル検証済みのCコンパイラです

も参照してください

参考文献

  1. ^ Sanghavi、Alok(2010年5月21日)。「フォーマル検証とは何ですか?」。EEタイムズアジア
  2. ^ フォーマル検証の概要、カリフォルニア大学バークレー校、2013年11月6日取得
  3. ^ コーエン、ベン; ベンカタラマナン、スリニバサン; クマリ、アジータ; パイパー、リサ(2015)。SystemVerilogアサーションハンドブック(第4版)。CreateSpace Independent PublishingPlatform。ISBN 978-1518681448
  4. ^ Favio DeMarco; Jifeng Xuan; ダニエル・ル・ベール; マーティンモンペラス(2014)。SMTを使用したバギーの場合の条件と欠落している前提条件の自動修復ソフトウェアのテスト、検証、および分析における制約に関する第6回国際ワークショップ(CSTVA 2014)の議事録pp。30–39。arXiv1404.3186土井10.1145 /2593735.2593740ISBN 9781450328470S2CID506586 _
  5. ^ Le Goues、クレア; グエン、タンフ; フォレスト、ステファニー; ワイマー、ウェストリー(2012年1月)。「GenProg:自動ソフトウェア修復のための一般的な方法」ソフトウェアエンジニアリングに関するIEEEトランザクション38(1):54–72。土井10.1109 /TSE.2011.104S2CID4111307_ 
  6. ^ ハリソン、J。(2003)。「Intelでのフォーマル検証」。2003年第18回コンピュータサイエンスにおける論理のIEEEシンポジウム。議事録pp。45–54。土井10.1109 /LICS.2003.1210044ISBN 978-0-7695-1884-8S2CID44585546 _
  7. ^ リアルタイムハードウェア設計のフォーマル検証Portal.acm.org(1983年6月27日)。2011年4月30日に取得。
  8. ^ 「正式な検証:Erik Seligman、Tom Schubert、およびMV AchuthaKirankumarによる最新のVLSI設計に不可欠なツール」2015年。
  9. ^ 「業界におけるフォーマル検証」(PDF)2012年9月20日取得
  10. ^ 「seL4 / ARMv6APIの抽象的な形式仕様」(PDF)2015年5月21日にオリジナル(PDF)からアーカイブされました2015年5月19日取得
  11. ^ Christoph Baumann、Bernhard Beckert、Holger Blasum、およびThorsten Bormerのオペレーティングシステムの正確性の成分?PikeOSのフォーマル検証で学んだ教訓
  12. ^ ジャック・ガンスルによる「GettingitRight
  13. ^ ハリス、ロビン。「ハッキングできないOS?CertiKOSは安全なシステムカーネルの作成を可能にします」ZDNet 2019年6月10日取得
  14. ^ 「CertiKOS:エールは世界初のハッカーに強いオペレーティングシステムを開発しました」International Business TimesUK2016年11月15日2019年6月10日取得
  15. ^ ヘラー、ブランドン。「ネットワーキングの真実を探る:テストから検証まで」フォワードネットワーク2018年2月12日取得
  16. ^ Scroxton、Alex。「シスコにとって、インテントベースのネットワーキングは将来の技術的要求を告げるものです」ComputerWeekly 2018年2月12日取得
  17. ^ ラーナー、アンドリュー。「インテントベースのネットワーキング」ガートナー2018年2月12日取得
  18. ^ ケラバラ、ゼウス。「シスコはインテントベースのネットワークをデータセンターにもたらします」NetworkWorld 2018年2月12日取得
  19. ^ 「フォワードネットワーク:ネットワーク操作の加速とリスク軽減」インサイトの成功2018年2月12日取得
  20. ^ 「意図=ベースのネットワーキングに着手する」(PDF)NetworkWorld 2018年2月12日取得
  21. ^ 「Veriflowシステム」ブルームバーグ2018年2月12日取得