形式検証

ハードウェアおよびソフトウェアシステムの文脈では、形式検証とは、数学の形式手法を使用して、特定の形式仕様またはプロパティに関するシステムの正しさを証明または反証する行為です。^{[1]形式検証は、システムの}形式仕様の主要な動機であり、形式手法の中核をなしています。これは、電子設計自動化における分析と検証の重要な側面を表し、ソフトウェア検証への1つのアプローチです。形式検証を使用すると、コンピューターセキュリティ認証の共通基準のフレームワークで最高の評価保証レベル( EAL7 ) が可能になります。

形式検証は、暗号化プロトコル、組み合わせ回路、内部メモリを備えたデジタル回路、プログラミング言語でソースコードとして表現されたソフトウェアなどのシステムの正しさを証明するのに役立ちます。検証済みのソフトウェアシステムの代表的な例としては、CompCert検証済みC コンパイラやseL4高保証オペレーティングシステムカーネルなどがあります。

これらのシステムの検証は、システムの数学モデルの形式的な証明の存在を保証することによって行われます。 ^[2]システムをモデル化するために使用される数学的オブジェクトの例としては、有限状態機械、ラベル付き遷移システム、ホーン節、ペトリネット、ベクトル加算システム、時間付きオートマトン、ハイブリッドオートマトン、プロセス代数、操作的意味論、表示的意味論、公理的意味論、ホーア論理などのプログラミング言語の形式意味論などがあります。^[3]

アプローチ

モデル検査

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

演繹的検証

もう一つのアプローチは演繹検証である。^[5]^[6]これは、システムとその仕様（および場合によっては他の注釈）から数学的な証明義務のコレクションを生成し、その真実性がシステムの仕様への適合を意味し、証明支援システム（対話型定理証明器）（HOL、ACL2、Isabelle、Coq、PVSなど）または自動定理証明器（特に充足可能性法理論（SMT）ソルバーを含む）を使用してこれらの義務を果たすことから成ります。このアプローチの欠点は、ユーザーがシステムが正しく動作する理由を詳細に理解し、証明する定理のシーケンスの形、またはシステムコンポーネント（関数や手順など）と場合によってはサブコンポーネント（ループやデータ構造など）の仕様（不変条件、前提条件、事後条件）の形でこの情報を検証システムに伝える必要がある場合があることです。

ソフトウェアへの応用

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

もう一つの補完的なアプローチはプログラム導出であり、一連の正確性を保つ手順によって機能仕様から効率的なコードが生成されます。このアプローチの例はバード・メルテンス形式主義であり、このアプローチはプログラム合成の別の形式と見なすことができます。

これらの手法は、検証されたプロパティがセマンティクスから論理的に推論できることを意味する健全な手法と、そのような保証がないことを意味する不健全な手法の 2 種類があります。健全な手法は、可能性の空間全体をカバーして初めて結果を生成します。不健全な手法の例としては、可能性のサブセットのみ (たとえば、特定の数までの整数のみ) をカバーし、「十分な」結果を生成する手法があります。また、手法は、アルゴリズムの実装が必ず答えで終了することを意味する決定可能な手法と、決して終了しない可能性があることを意味する決定不可能な手法に分けられます。可能性の範囲を限定することで、決定可能な健全な手法が利用できない場合に、決定可能な不健全な手法を構築できる可能性があります。

検証と検証

検証は、製品の目的への適合性をテストする 1 つの側面です。妥当性確認は、補完的な側面です。全体的なチェックプロセスを V & V と呼ぶことがよくあります。

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

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

自動プログラム修復

プログラムの修復は、生成された修正の検証に使用されるプログラムの望ましい機能を網羅するオラクルに対して実行されます。簡単な例としては、入力/出力のペアがプログラムの機能を指定するテストスイートがあります。さまざまな手法が採用されていますが、最も有名なのは、満足可能性モジュロ理論(SMT) ソルバーと、進化的コンピューティングを使用して修正の候補を生成および評価する遺伝的プログラミング[ ^7]の使用です。前者の方法は決定論的であり、後者はランダム化されています。

プログラム修復は、形式検証とプログラム合成の技術を組み合わせたものです。形式検証の障害特定技術は、合成モジュールのターゲットとなり得るバグの可能性のある場所を計算するために使用されます。修復システムは、検索空間を減らすために、事前に定義された小さなクラスのバグに焦点を当てることがよくあります。既存の技術の計算コストのため、産業での使用は限られています。

産業用途

設計の複雑性が増すにつれ、ハードウェア業界では形式検証技術の重要性が高まっています。^[8]^[9]現在、形式検証はほとんどまたはすべての大手ハードウェア企業で使用されていますが、^[10]ソフトウェア業界での使用はまだ停滞しています。^[要出典]これは、エラーがより大きな商業的意味を持つハードウェア業界でのニーズが大きいためと考えられます。^[^要出典^]^{コンポーネント}間の微妙な相互作用の可能性があるため、シミュレーションによって現実的な可能性のセットを実行することはますます困難になっています。ハードウェア設計の重要な側面は自動証明方法に適応できるため、形式検証の導入が容易になり、生産性が向上します。^[11]

2011年現在^{[アップデート]}、いくつかのオペレーティングシステムが正式に検証されている。OK LabsがseL4として市販しているNICTAのSecure Embedded L4マイクロカーネル^{[12] 、}華東師範大学のOSEK/VDXベースのリアルタイムオペレーティングシステムORIENTAIS 、^[^{引用が必要}^]、 Green Hills SoftwareのIntegrityオペレーティングシステム、^[^{引用が必要}^]、SYSGOのPikeOS ^[13]^[14]。 2016年には、イェール大学のZhong Shao氏が率いるチームが、CertiKOSと呼ばれる正式に検証されたオペレーティングシステムカーネルを開発した。^[15]^[16]

2017年現在、形式検証はネットワークの数学的モデルを通じて大規模コンピュータネットワークの設計に適用されており、^[17]新しいネットワーク技術カテゴリであるインテントベースネットワーキングの一部として適用されています。^[18]形式検証ソリューションを提供するネットワークソフトウェアベンダーには、Cisco ^[19] Forward Networks ^[20]^[21]やVeriflow Systemsなどがあります。^[22]

SPARKプログラミング言語は、形式検証によるソフトウェア開発を可能にするツールセットを提供し、いくつかの高信頼性システムで使用されています。^[要出典]

CompCert Cコンパイラは、 ISO Cの大部分を実装した正式に検証されたCコンパイラです。^[23]^[24]

参照

参考文献

^ Sanghavi, Alok (2010 年 5 月 21 日)。「形式検証とは何か?」EE Times Asia。
^ Sanjit A. Seshia、Natasha Sharygina、Stavros Tripakis (2018)。「第3章：検証のためのモデリング」。Clarke、Edmund M.、Henzinger、Thomas A.、Veith、Helmut、Bloem、Roderick（編）。モデル検査ハンドブック。Springer。pp. 75–105。doi ：10.1007 /978-3-319-10575-8。ISBN 978-3-319-10574-1。
^ 形式検証入門、カリフォルニア大学バークレー校、2013年11月6日閲覧
^ Cohen, Ben; Venkataramanan, Srinivasan; Kumari, Ajeetha; Piper, Lisa (2015). SystemVerilog アサーションハンドブック(第 4 版). CreateSpace Independent Publishing Platform. ISBN 978-1518681448。
^ Ahrendt, Wolgang; Beckert, Bernhard; Bubel, Richard; Hähnle, Reiner; Schmitt, Peter H. 編 (2016).演繹的ソフトウェア検証 - KeY ブック: 理論から実践へ(第 1 版 2016). Cham: Springer International Publishing : Imprint: Springer. ISBN 978-3-319-49812-6。
^ Pretschner, Alexander; Müller, Peter; Stöckle, Patrick, 編 (2019)。「演繹的プログラム検証器の構築 - 講義ノート」。安全で信頼性の高いソフトウェアシステムのエンジニアリング。アムステルダム、オランダ: IOS Press。ISBN 978-1-61499-976-8。
^ Le Goues, Claire; Nguyen, ThanhVu; Forrest, Stephanie; Weimer , Westley (2012 年 1 月)。「 GenProg : 自動ソフトウェア修復のための汎用メソッド」。IEEE Transactions on Software Engineering。38 ( 1): 54–72。doi : 10.1109 /TSE.2011.104。S2CID 4111307。
^ Harrison, J. (2003). 「Intel での形式検証」。第 18 回 IEEE コンピュータサイエンスにおける論理シンポジウム、2003 年。議事録。pp . 45–54。doi :10.1109 / LICS.2003.1210044。ISBN 978-0-7695-1884-8. S2CID 44585546。
^ リアルタイムハードウェア設計の形式検証。Portal.acm.org (1983 年 6 月 27 日)。2011 年 4 月 30 日に取得。
^ 「形式検証: 現代の VLSI 設計に不可欠なツール」、Erik Seligman、Tom Schubert、MV Achutha Kirankumar 著、2015 年。
^ 「業界における形式検証」(PDF) 。2012 年9 月 20 日閲覧。
^ 「seL4/ARMv6 API の抽象形式仕様」(PDF)。2015 年 5 月 21 日時点のオリジナル(PDF)からアーカイブ。2015 年5 月 19 日閲覧。
^ Christoph Baumann、Bernhard Beckert、Holger Blasum、Thorsten Bormer オペレーティングシステムの正しさの要素? PikeOS の形式検証で学んだ教訓 2011 年 7 月 19 日アーカイブ、Wayback Machineで
^ 「正しく理解する」ジャック・ガンスル著
^ ハリス、ロビン。「ハッキング不可能なOS？CertiKOSで安全なシステムカーネルの作成が可能に」ZDNet 。 2019年6月10日閲覧。
^ 「CertiKOS: イェール大学が世界初のハッカー耐性オペレーティングシステムを開発」International Business Times UK 2016年11月15日。 2019年6月10日閲覧。
^ Scroxton, Alex. 「シスコにとって、インテントベースネットワーキングは将来の技術需要の先駆け」。Computer Weekly。2018年2 月 12 日閲覧。
^ Lerner, Andrew. 「インテントベースネットワーキング」。ガートナー。 2018年2月12日閲覧。
^ Kerravala, Zeus. 「シスコ、データセンターにインテントベースネットワークを導入」。NetworkWorld。2023年12月11日時点のオリジナルよりアーカイブ。2018年2月12日閲覧。
^ 「Forward Networks: ネットワーク運用の高速化とリスク軽減」。Insights Success。2018 年 1 月 16 日。2018年2 月 12 日閲覧。
^ 「インテントベースネットワーキングの基礎」(PDF)。NetworkWorld。2018年2 月 12 日閲覧。
^ 「Veriflow Systems」。ブルームバーグ。 2018年2月12日閲覧。
^ 「CompCert - CompCert C コンパイラ」. compcert.org . 2023年2月22日閲覧。
^ Barrière, Aurèle; Blazy, Sandrine ; Pichardie, David (2023 年 1 月 9 日)。「効果的な JIT での形式検証済みネイティブコード生成: CompCert バックエンドを形式検証済み JIT コンパイラーに変える」。ACMプログラミング言語に関する議事録。7 ( POPL): 249–277。arXiv : 2212.03129。doi : 10.1145/ 3571202。ISSN 2475-1421。S2CID 253736486 。

[1] Sanghavi, Alok (2010 年 5 月 21 日)。「形式検証とは何か?」EE Times Asia。

[2] Sanjit A. Seshia、Natasha Sharygina、Stavros Tripakis (2018)。「第3章：検証のためのモデリング」。Clarke、Edmund M.、Henzinger、Thomas A.、Veith、Helmut、Bloem、Roderick（編）。モデル検査ハンドブック。Springer。pp. 75–105。doi ：10.1007 /978-3-319-10575-8。ISBN 978-3-319-10574-1。

[3] 形式検証入門、カリフォルニア大学バークレー校、2013年11月6日閲覧

[4] Cohen, Ben; Venkataramanan, Srinivasan; Kumari, Ajeetha; Piper, Lisa (2015). SystemVerilog アサーションハンドブック(第 4 版). CreateSpace Independent Publishing Platform. ISBN 978-1518681448。

[5] Ahrendt, Wolgang; Beckert, Bernhard; Bubel, Richard; Hähnle, Reiner; Schmitt, Peter H. 編 (2016).演繹的ソフトウェア検証 - KeY ブック: 理論から実践へ(第 1 版 2016). Cham: Springer International Publishing : Imprint: Springer. ISBN 978-3-319-49812-6。

[6] Pretschner, Alexander; Müller, Peter; Stöckle, Patrick, 編 (2019)。「演繹的プログラム検証器の構築 - 講義ノート」。安全で信頼性の高いソフトウェアシステムのエンジニアリング。アムステルダム、オランダ: IOS Press。ISBN 978-1-61499-976-8。

[7] ^ Le Goues, Claire; Nguyen, ThanhVu; Forrest, Stephanie; Weimer , Westley (2012 年 1 月)。「 GenProg : 自動ソフトウェア修復のための汎用メソッド」。IEEE Transactions on Software Engineering。38 ( 1): 54–72。doi : 10.1109 /TSE.2011.104。S2CID 4111307。

[8] Harrison, J. (2003). 「Intel での形式検証」。第 18 回 IEEE コンピュータサイエンスにおける論理シンポジウム、2003 年。議事録。pp . 45–54。doi :10.1109 / LICS.2003.1210044。ISBN 978-0-7695-1884-8. S2CID 44585546。

[9] リアルタイムハードウェア設計の形式検証。Portal.acm.org (1983 年 6 月 27 日)。2011 年 4 月 30 日に取得。

[10] 「形式検証: 現代の VLSI 設計に不可欠なツール」、Erik Seligman、Tom Schubert、MV Achutha Kirankumar 著、2015 年。

[11] 「業界における形式検証」(PDF) 。2012 年9 月 20 日閲覧。

[12] 「seL4/ARMv6 API の抽象形式仕様」(PDF)。2015 年 5 月 21 日時点のオリジナル(PDF)からアーカイブ。2015 年5 月 19 日閲覧。

[13] Christoph Baumann、Bernhard Beckert、Holger Blasum、Thorsten Bormer オペレーティングシステムの正しさの要素? PikeOS の形式検証で学んだ教訓 2011 年 7 月 19 日アーカイブ、Wayback Machineで

[14] 「正しく理解する」ジャック・ガンスル著

[15] ハリス、ロビン。「ハッキング不可能なOS？CertiKOSで安全なシステムカーネルの作成が可能に」ZDNet 。 2019年6月10日閲覧。

[16] 「CertiKOS: イェール大学が世界初のハッカー耐性オペレーティングシステムを開発」International Business Times UK 2016年11月15日。 2019年6月10日閲覧。

[17] Scroxton, Alex. 「シスコにとって、インテントベースネットワーキングは将来の技術需要の先駆け」。Computer Weekly。2018年2 月 12 日閲覧。

[18] Lerner, Andrew. 「インテントベースネットワーキング」。ガートナー。 2018年2月12日閲覧。

[19] Kerravala, Zeus. 「シスコ、データセンターにインテントベースネットワークを導入」。NetworkWorld。2023年12月11日時点のオリジナルよりアーカイブ。2018年2月12日閲覧。

[20] 「Forward Networks: ネットワーク運用の高速化とリスク軽減」。Insights Success。2018 年 1 月 16 日。2018年2 月 12 日閲覧。

[21] 「インテントベースネットワーキングの基礎」(PDF)。NetworkWorld。2018年2 月 12 日閲覧。

[22] 「Veriflow Systems」。ブルームバーグ。 2018年2月12日閲覧。

[23] 「CompCert - CompCert C コンパイラ」. compcert.org . 2023年2月22日閲覧。

[24] Barrière, Aurèle; Blazy, Sandrine ; Pichardie, David (2023 年 1 月 9 日)。「効果的な JIT での形式検証済みネイティブコード生成: CompCert バックエンドを形式検証済み JIT コンパイラーに変える」。ACMプログラミング言語に関する議事録。7 ( POPL): 249–277。arXiv : 2212.03129。doi : 10.1145/ 3571202。ISSN 2475-1421。S2CID 253736486 。