SPARK Pro
SPARK Pro
より安全なコードを記述するために
SPARK Proは、形式検証可能なAda 2012サブセットの言語で、ソフトウェア検証に数学ベースの信頼性をもたらすツールセットです。
SPARK Pro を使用して、ソフトウェア・アーキテクチャ要件を形式的に定義、自動検証します。実行時エラーを削減し、セーフティ・プロパティまたはセキュリティ・ポリシーの適用、機能の正確性 (形式的に定義された仕様への準拠) などの幅広いソフトウェア整合性に対するプロパティを保証する事ができます。
SPARK言語
SPARK言語は、形式検証と静的解析ツールセットで、最新バージョンはSPARK 2014でAda 2012に基づいたサブセットです。静的検証に適さない機能、ならびにソフトウェアの欠陥となる機能は除外されています。
SPARK言語の主要な機能は、契約（contract）を使用できることで、プロパティ記述の正しさを、検証ツールセットで確認できます。
SPARK 2014の契約（contract）はAda 2012と同じ構文を使用するため、仕様と実装の両方を同一言語で記述できます。契約（contract）は、Adaセマンティクス（semantics）を使用して実行時チェック、ならびにSPARKツールで静的検証が可能です。
SPARKプログラミング言語と形式検証ツールについては、AdaCore社学習サイトで、 Ada言語とSPARK言語の違い、ならびにSPARKに付属するさまざまな解析ツールの使用方法を使用しながら学ぶことができます。 learn.adacore.comの「Intro to SPARK」コースを参照してください。
レベル別でのSPARK使用
ツールスイートには、各種ツールとSPARKが同梱されています。 SPARK Proは、自動検証機能が3つ含まれたツールセットで、SPARK Discovery（GNAT Proに添付）には、SPARK Proと同じ解析が可能ですが、自動検証機能は1つに限定されます。
他のSPARK Proの特長は、静的解析ツールCodePeerとの統合、反例の生成（証明がフェイルした際の）、モジュラ演算、浮動小数点演算を使用したプログラムのサポート、より複雑な証明のために補助ライブラリ（lemma library）が含まれています。
🔸ストーン（Stone）
SPARK言語の制約事項により、安全なプログラムが記述できます。
SPARK DiscoveryおよびSPARK Proで利用可能
🔸ブロンズ（Bronze）
データフロー解析とインフォメーションフロー解析を使用して、非初期化変数の参照などの広範なエラーを排除できます。
SPARK DiscoveryおよびSPARK Proで利用可能
🔸シルバー（Silver）
実行時にソフトウェアエラーがないことの保証
SPARK DiscoveryおよびSPARK Proで利用可能
🔸ゴールド（Gold）
証明（Proof）を使用して、ソフトウェアの重要なプロパティを保証
SPARK Proで利用可能
🔸プラチナ （Platinum）
クリティカルなコードが機能仕様を満たしていることを証明
SPARK Proで利用可能
ソフトウェア設計と検証サイクル全体に対して統合されたアプローチを提供
SPARK Proは、ソフトウェア仕様、コーディング、テスト、ならびに証明（Proof）によるユニット検証を、統合化フレームワークで実行されます。手動レビューなどで達成すべき検証目標は、SPARKツールスイートで実現でき、認証要件を満たすレポートを作成できます。
SPARKプログラミング言語は、新規の開発で使用することも、他言語（CやC ++など）での既存プロジェクトに段階的に使用することも可能です。 ハイブリッド検証と呼ばれるアプローチでのテストと組み合わせることができます。
特長
🔹IDEへの統合
SPARK ProツールセットはGNAT StudioおよびGNATbench IDEに統合され、エラーとウォーニングをソースコードと同一ウインドウに表示し、よりスムーズな作業が実現できます。 または、ツールをコマンドラインモードで実行でき、例えば、証明の結果に必要なレポートを生成することもできます。
🔹データフロー解析
SPARK Proは、非初期化変数の参照など、不確実性や不正な動作の原因となる一般的なプログラミングエラーを検出します。 データフロー解析は、グローバル変数へのアクセスを解析し、ソフトウェアが設計仕様に準拠しているかを確認できます。
🔹インフォメーションフロー解析
クリティカルアプリケーションの場合、依存契約（dependency contracts）を指定して、プログラムで許可されるインフォメーションフロー（サブプログラムによるグローバル変数と形式パラメーターの使用方法）を制限できます。
この契約（contracts）の違反 （セーフティやセキュリティ・ポリシーの違反となる可能性）は、コードをコンパイルしなくても検出できます。
🔹実行時例外の除外
SPARK Proは、プログラムにゼロ除算、数値オーバーフロー、バッファオーバーフロー、配列の範囲外インデックスなどの実行時例外がないことを確認で、基礎となる数学的証明（proof）システムは、この解析が妥当であることを保証します。そのため、プログラムが実行またはテストされる前であっても、検出が困難な可能性のある多岐にわたるエラーをソフトウェアから除外できます。
🔹プロパティチェック
クリティカルアプリケーションにとって、セーフティやセキュリティプロパティは、Ada 2012で使用されているのと同一契約（contract）表記で記述できます。（たとえば、サブプログラムの事前条件と事後条件（pre- and postconditions））。
数学的に妥当な証明システムを使用して、SPARK Proツールセットは、プログラムが取りうるすべての入力と実行パスについて、プロパティを満足するかを自動的に検証できます。
プログラムは徹底的にテストされますが、コードをコンパイルまたは実行する必要はありません。
🔹機能の正確さ
拡張された契約（contract）言語により、SPARKはプログラムに要求される挙動の形式仕様（要件の仕様）の記述を許可します。
SPARK Proツールは、プログラムがその機能仕様を満たしていることを証明します。これにより、クリティカルシステムの正しい動作に対して高いレベルで保証します。
CWE互換ツール
SPARK Proは、MITREのCommon Weakness Enumeration（CWE）互換性および有効性プログラムによりCWE互換として指定されており、CWEの上位25に含まれる危険なソフトウェアエラーなど、さまざまなコードの弱点を検出できます。
SPARK Proは、証明技術を使用して、Ada言語のサブセットで記述されたプログラムのプロパティを検証します
このツールは、データ/インフォメーションフローの有効性、実行時エラーの除外、システム整合性制約（安全な状態遷移など）の解析、さらに、クリティカルソフトウェアのために、形式記述された要件を用いて、機能の正確さなどのプロパティを証明できます。 SPARK Proは静的解析ツールで、プロパティの違反を検出可能、かつ誤検知率は低くなっています。
SPARK Proは、CWE weaknessを防止、検出可能
| CWE weakness | Description |
| CWE 120, 123, 124, 125, 126, 127, 129, 130, 131 | Buffer overflow/underflow |
| CWE 136, 137 | Variant record field violation, Use of incorrect type in inheritance hierarchy |
| CWE 188 | Reliance on data layout |
| CWE 190, 191 | Numeric overflow/underflow |
| CWE 193 | Off-by-one error |
| CWE 194 | Unexpected sign extension |
| CWE 197 | Numeric truncation error |
| CWE 252, 253 | Unchecked or incorrectly checked return value |
| CWE 366 | Race Condition |
| CWE 369 | Division by zero |
| CWE 456, 457 | Use of uninitialized variable |
| CWE 466, 468, 469 | Pointer errors |
| CWE 476 | Null pointer dereference |
| CWE 562 | Return of stack variable address |
| CWE 563 | Unused or redundant assignment |
| CWE 682 | Range constraint violation |
| CWE 786, 787, 788, 805 | Buffer access errors |
| CWE 820 | Missing synchronization |
| CWE 821 | Incorrect synchronization |
| CWE 822, 823, 824, 825 | Pointer errors |
| CWE 835 | Infinite loop |
製品カタログ（日本語）
リンク
Intro to SPARK コース
https://learn.adacore.com/courses/intro-to-spark/index.html
