1. ホーム(Home) > 
  2. 製品情報 > 
  3. AdaCore 統合開発環境 > 
  4. 形式手法開発環境 AdaCore SPARK Pro

Products

 

形式手法開発環境 AdaCore SPARK Pro

SPARK Proは形式手法を用いて高信頼性ソフトウエアの検証ができる静的解析ツールが統合された開発環境で、SPARK 2014言語をサポートしGNAT Programming Studio (GPS) GUI下で動作します。 Eclipse環境をサポートするWind River WorkBench への統合も可能です。

概要

SPARK Proを使用することでソフトウエア・アーキテクチャ・プロパティを宣言、自動的に検証しランタイムエラーの修正、セキュリティポリシーの強化等ソフトウエア・インテグリティ・プロパティの広い範囲を保証します。この自動的検証はアプリケーションのソフトウエアエラー検出に特に有効です。SPARK Proは形式手法の使用で出荷コスト、開発期間を低減し開発工程の早い段階でディフェクトを数学的検証で検出、排除することができます。SPARK言語とツールはセーフティクリティカルならびに高セキュリティシステムで多くの採用実績があります。

SPARKの採用事例

http://www.adacore.com/sparkpro/projects/

プログラミングの最初から検証

SPARKテクノロジーはソフトウエアの不良を検証する設計手法を提供します。ソフトウエア・ライフ・サイクルの初期段階から検証を行いテスト、デバッグフェーズでの工数を削減、出荷後に発生する不良に対するリスク、コストを低減します。

検証しながらセキュアなソフトウェア開発

SPARK Proは IEC61508、DO178C等の高信頼性国際標準の基準に合致したセキュアソフトウエア開発に使用することができ、バッファオーバーフローや非初期化変数等のソフトウエアセキュリティの不良を検出する機能を備えています。
SPARK Proは米国国立標準技術研究所、U.S. National Institute for Standards and Technology (NIST)からのレポートに他の多くの言語よりセキュアであることが報告されています。

セイフティスタンダードへの準拠

SPARKProは高インテグリティ・ソフトウエア・セーフティ・スタンダード(DO-178B/C and the Formal Methods supplement DO-333)、CENELEC 50128 , IEC 61508, and DEFSTAN 00-56)の要求に対応しています。SPARK Proは各国際標準向けにコンストラクティブ保証ケース(constructive assurance case)ならびにデモンストレイト・コンフォーマンス(demonstrate conformance)をビルドするために使用するエビデンスを作成します。

既存Cコードのインテグリティ向上

高インテグリティ・アプリケーションを作成する際にSPARK Proは既存Cコードの品質改善に有効な手段です。SPARK言語は非初期化変数のようなエラー検出、コントラクト(contract)を用いて異なる検証手法を提供します。

2つの検証 Hybrid Verification ハイブリッド・ベリフィケーション

図:2つの検証 Hybrid Verification ハイブリッド・ベリフィケーション

最新のSPARK言語はAda2012をベースに開発され、フォーマル。プルーフ(Formal Proof)とユニット・テストを組合わせた2つの検証 (ハイブリッド・ベリフィケーション)が可能です。システムならびに国際標準の検証レベルに合致するようにベリフィケーションを選択して実行できます。
ContractはAdaのaspectとpragmaを使用してSPARKプログラムに適用されコンパイラによって作成されたダイナミック検証手法ならびにSPARKツールで実行されるFormal Proof (フォーマル・プルーフ)手法によってプログラムの仕様を検証します。
Contractは関数の振舞い、インファメーション・フロー、セーフィティプロパティ、セキュリティプロパティを検証します。

既存のコードを再構築

新しく高信頼性アプリケーションの開発に使用されることはもとより、SPARK Proは既存のソフトウェアの品質を向上させるために使用することができます。
例えば、C言語で書かれたシステムは低レベルのハードウェア・インタフェース・モジュールを変更することなく、アプリケーション・ロジックと制御アルゴリズムをSPARKに書き換え、そのコードの堅牢性は、SPARKの静的解析機能用いて改善することができ、そのコードにContractを使用してプロパティ、プログラムの振舞いを検証し正しく実装されていることを確認できます。

開発スタイルの新しい流れ

SPARKは新規システムの開発でcorrectness-by-construction approachを行う手法で高インテグリティコードを応用した製品開発時間ならびにコストを削減できるアプローチとなりテスト時間も削減します。また、組込機器やコンスーマ機器の出荷後のソフトウェア不良によるリコールを回避する上でも有用です。

SPARKの提供する機能

  • プログラムエラーの検出
  • コードコンパイル前のエラー検出
  • エビデンス作成

セキュアなシステム開発

SPARKはセキュリティを考慮した設計がなされ高信頼性システムソフトウエアの開発、検証に応用できます。

SPARK言語の特徴はセキュリティ上の欠陥を回避できるところにあります。SPARK Pro ToolsはCWE/ SANSのエキスパートがリスト(下記参照)した危険なプログラミングエラーを検出し軽減することができます。

improper input validation integer overflow or wraparound
buffer overflow errors improper initialization
improper validation of array index information leak

設計上のあいまいさやミスで生じた脆弱性はシステム・ライフ・サイクルの早い段階、コンパイル前でも評価前でもテスト、検証され削除されることが望まれます。

SPARKは、Dependency contractを使用してプログラムに必要な条件を指定することが可能でSPARKツールはcontractの要求条件に従って実装されているか確認し、セキュリティ違反となる箇所が検出されるとそのコードのパスを強調表示します。

最高レベルの保証においてSPARKは主なセキュリティプロパティをキャプチャすることができ、セキュリティプロパティにはソフトウエアcontract内にシステムのセキュリティ要件の置換えを保持する実装がなされています。

SPARKツールセットは、すべてのとり得る状態と入力用のセキュリティプロパティを保持していることを証明するために使用されます。システム検証をテストベースアプローチ (test-based approach)で行うのは困難な場合があります。

SPARKはアシュアランス・ケース(assurance case)をサポートするために必要なエビデンスを作成、コモン・クライテリア(Common Criteria)やITSECのような高レベルな標準に対するソフトウエアの信頼性をサポートするために使用可能です。

セーフティクリティカルなシステム開発

セーフティ関連、セーフティ・クリティカル・システムは通常、高度な基準にもとづいた環境において設計し、可能なかぎり高レベルのソフトウェア・インテグリティが要求されます。 DO-178B/ C、CENELEC50128、IEC 61508、およびDEFSTAN00-56のような主要な国際基準のソフトウェア関連の要件を満たす技術をSPARKは備えています。

DO-178B/ C CENELEC50128 IEC 61508 DEFSTAN00-56

SPARKは危険なプログラミング設計を回避する安全なシステム開発に適した高水準言語の要件を満たしており静的検証のための基盤を提供します。

SPARKツールセットは、プロセスベースの規格(process-based standards)で要求される静的解析機能を提供し、多くの一般的なプログラミングエラーを検出することができます。

SPARKツールセットは、クリティカルなシステムの認証のために要求されるセーフティ・ケース(safety case)のソフトウェア・インテグリティ・アスペクト(software-integrity aspects)に対応するエボデンスを生成します。

SPARKは、多種多様な産業分野ならびに知名度の高い重要なシステムのアプリケーションで多くの実績があります。

SPARK Proツールセット

SPARK ProツールセットはGPS IDE(AdaCore社GUI)に統合されており、ソースコード、エラーならびにウォーニングも同一GUI内に表示されます。また、認証取得用エビデンスで要求されるレポートの作成はコマンドから行えます。

GPS Contractとプログラムを表示
図:GPS Contractとプログラムを表示拡大表示

データフロー解析

データフロー解析は初期化されていない変数や効果のない割り当てを含む 不確定さ、誤動作の原因となる一般的なプログラミングエラーを検出します。また、contractで指定された条件にしたがってグローバル変数へのアクセスをチェックするために使用されます。結果として、ソフトウエアが設計仕様に適合しているか確認できます。

インフォメーション・フロー・アナリシス(Information Flow Analysis)

クリチカル・アプリケーションにおいては、dependency contractsを使用してプログラム内で許可された情報の流れ(Information Flow)を制限するために指定することができます。これらのcontract違反(潜在的にセーフティやセキュリティポリシーの違反を表す)はコードがコンパイル前に検出することができます。

実行時例外の検証

SPARK Proは、プログラムがゼロ除算、数値オーバーフロー、バッファオーバーフロー、配列の境界外インデックス参照など、実行時例外を検証することができます。SPARKproは数学的な証明システムで解析を行いシステムの堅牢性を検証し、プログラム未実行、評価前であっても検出が困難なエラーをソフトウエアから排除することができます。

SPARK関連リンク

AdaCore製品情報
AdaCore 統合開発環境
↑このページのトップ