Loading article…
SPARKは、 Adaプログラミング言語をベースにした正式に定義されたコンピュータプログラミング言語であり、予測可能で信頼性の高い動作が不可欠なシステムで使用される高信頼性ソフトウェアの開発を目的としています。安全性、セキュリティ、またはビジネスの完全性を要求するアプリケーションの開発を容易にします。特に、安全性やコンピュータセキュリティの問題が最優先されるリアルタイムコンピューティングや組み込みシステムで利用されています。[ 2 ]
当初、SPARKには3つのバージョン（SPARK83、SPARK95、SPARK2005）が存在し、それぞれAda 83、Ada 95、Ada 2005をベースとしていた。
Ada 2012をベースとした第4バージョンであるSPARK 2014は、2014年4月30日にリリースされました。SPARK 2014は言語の完全な再設計であり、ソフトウェア検証ツールをサポートしています。
SPARK言語は、Ada言語の明確に定義されたサブセットで構成されており、契約を使用してコンポーネントの仕様を静的検証と動的検証の両方に適した形式で記述します。[ 3 ]また、SPARKは、予測不可能な動作を引き起こす可能性のあるすべての言語構造を排除するように設計されています。[ 4 ]
SPARK83/95/2005では、契約はAdaコメントでエンコードされているため、標準のAdaコンパイラでは無視されますが、SPARK Examinerとその関連ツールによって処理されます。これらの以前のバージョンは、契約の静的検証に重点を置いています。[ 3 ]
一方、SPARK 2014は、Ada 2012に組み込まれているアスペクト構文を用いて契約を表現し、それを言語の中核に組み込んでいます。SPARK 2014の主要ツール（GNATprove）はGNAT/GCCインフラストラクチャに基づいており、GNAT Ada 2012のフロントエンドのほぼすべてを再利用しています。
SPARKは、Adaの強みを活かしつつ、潜在的な曖昧さや安全性の低い構造を排除しようと努めています。SPARKプログラムは、設計上、曖昧さのないものであり、その動作はAdaコンパイラの選択に影響されないことが求められます。これらの目標は、Adaのより問題のある機能（無制限の並列タスクなど）の一部を省略することと、プログラムの特定のコンポーネントに対するアプリケーション設計者の意図と要件をエンコードする契約を導入することによって達成されます。
これらのアプローチを組み合わせることで、SPARKは以下の設計目標を達成することができます。
Praxisのスタッフの一人は、「Sparkを使用した場合の欠陥率は、他の言語で作成されたものよりも少なくとも10倍、場合によっては100倍低い」と述べている。[ 4 ]
以下のAdaサブルーチン仕様を検討してください。
手続きIncrement (X : in out Counter_Type);
純粋なAdaでは、これは変数をX1または1000だけインクリメントするかもしれません。あるいは、グローバルカウンタをに設定してX、カウンタの元の値を返すかもしれませんX。あるいは、に対して何も行わないかもしれませんX。
SPARK 2014では、サブルーチンが実際に何を行うかについての詳細情報を提供するために、コードに契約が追加されました。たとえば、上記の仕様は次のように変更できます。
procedure Increment (X : in out Counter_Type) with Global => null , 状況による => (X => X);
これは、このIncrement手順がグローバル変数を一切使用せず（更新も読み取りも行わない）、新しい値の計算に使用されるデータ項目は のみであることをX指定しますX。
あるいは、仕様は次のように記述することもできます。
プロシージャIncrement (X : in out Counter_Type) with Global => (In_Out => Count) 依存 => (カウント => (カウント、X) X => null);
これは、 が同じパッケージ内のIncrementグローバル変数を使用すること、 のエクスポート値がとのインポートされた値に依存すること、そして のエクスポート値はどの変数にも依存せず、定数データのみから導出されることを指定しています。CountIncrementCountCountXX
GNATproveを仕様書とサブルーチンの本体に対して実行すると、サブルーチンの本体を分析して情報フローのモデルを構築します。このモデルは注釈で指定された内容と比較され、不一致があればユーザーに報告されます。
これらの仕様は、サブルーチンが呼び出されたときに満たされる必要があるプロパティ（事前条件）またはサブルーチンの実行が完了した後に満たされるプロパティ（事後条件）を表明することによって、さらに拡張できます。たとえば、次のように記述する場合：
プロシージャIncrement (X : in out Counter_Type) with Global => null, 場合による => (X => X) Pre => X < Counter_Type'Last、 投稿 => X = X'Old + 1;
これにより、それX自体からのみ派生するだけでなく、Incrementが呼び出される前にはX、その型の最後の可能な値よりも厳密に小さくなければならないこと（結果がオーバーフローしないことを保証するため）、そして呼び出し後は、X初期値にX1 を加えた値と等しくなることも指定されます。
GNATproveは、検証条件（VC）のセットを生成することもできます。これらは、特定のサブプログラムに対して特定の特性が成り立つかどうかを判断するために使用されます。最低限、GNATproveは、次のようなすべての実行時エラーがサブプログラム内で発生しないことを証明するVCを生成します。
サブルーチンに事後条件やその他のアサーションが追加された場合、GNATprove は、ユーザーがサブルーチン内のすべての可能なパスでこれらのプロパティが成り立つことを示すことを要求する VC も生成します。
GNATproveは内部的には、Why3中間言語とVCジェネレータ[ 3 ] 、およびCVC4、Z3、Alt-Ergo定理証明器を使用してVCを解放します。Why3ツールセットの他のコンポーネントを介して、他の証明器（対話型証明チェッカーを含む）を使用することも可能です。
この技術の起源は1987年に遡り、サウサンプトン大学で行われた研究に基づいている。[ 3 ] SPARKの最初のバージョン（Ada 83に基づく）は、英国国防省の支援を受けて、同大学でバーナード・カレとトレバー・ジェニングスによって作成された。SPARKという名前は、Pascalプログラミング言語のSPADEサブセットにちなんで、SPADE Ada Kernelから派生したものである。[ 5 ]
その後、この言語は、まず Program Validation Limited によって、次に Praxis Critical Systems Limited によって、段階的に拡張および改良されました。2004 年に、Praxis Critical Systems Limited は Praxis High Integrity Systems Limited に社名を変更し、SPARK の開発は継続されました。[ 4 ] 2010 年 1 月に、同社はAltran Praxisとなりました。
2009年初頭、PraxisはAdaCoreと提携し、GPLライセンスの下でSPARK Proをリリースした。これに続き、2009年6月には、フリーソフトウェアおよびオープンソースソフトウェア（FOSS）コミュニティと学術コミュニティを対象としたSPARK GPL Edition 2009がリリースされた。
2013年1月、Altran-Praxisは社名をAltranに変更し、2021年4月にはCapgemini Engineeringとなった（AltranとCapgeminiの合併による）。
SPARK 2014の最初のPro版は2014年4月30日に発表され、その後すぐにFLOSSコミュニティと学術コミュニティを対象としたSPARK 2014 GPL版がリリースされた。
SPARKは、実際の産業用途で数多く採用されています。設計プロセスのできるだけ早い段階で組み込むことが、一般的に最も好ましい結果をもたらすと考えられています。[ 6 ]
SPARKは、商用航空（船舶/ヘリコプター運用限界計装システム[ 6 ] 、ロールス・ロイス・トレントシリーズジェットエンジン、ARINC ACAMSシステム、ロッキード・マーティンC130J [ 6 ]）、軍用航空（ユーロファイター・タイフーン[3] 、ハリアーGR9、エアマッキM346）、航空交通管理（英国NATS iFACTSシステム[ 3 ] ）、鉄道（多数の信号アプリケーション）、医療（ライフフロー心室補助装置）、宇宙アプリケーション（バーモント工科大学CubeSatプロジェクト[ 7 ] ）など、いくつかの注目度の高い安全性が重要なシステムで使用されています。
このようなシステムに必要な承認プロセスに関して言えば、SPARKは英国国防規格（DEFSTAN）00-55 [ 3 ] 、 DO-178BレベルA、およびITSEC E6 [ 6 ]の認証に使用されています。
SPARKはセキュアシステムの開発にも使用されています。ユーザーには、Rockwell Collins（TurnstileおよびSecureOneクロスドメインソリューション）、オリジナルのMULTOS CAの開発[ 6 ] 、 NSA Tokeneerデモンストレーター[ 3 ]、secunetマルチレベルワークステーション、Muen分離カーネル、Genodeブロックデバイス暗号化装置などがあります。別の例として、Mondex Internationalが製造したプリペイドカード用のセキュア認証局が実装され、 SPARKでのコーディングの前段階としてZ表記が使用されました。[ 4 ]
2010年8月、Altran Praxisの主席エンジニアであるRod Chapmanは、SHA-3の候補の一つであるSkeinをSPARKで実装した。慎重な最適化の後、彼はSPARK版の実行速度をC言語版よりわずか5～10%遅い程度に抑えることに成功した。その後、GCCのAdaミドルエンド（AdaCoreのEric Botcazouが実装）の改良により、その差は縮まり、SPARKコードのパフォーマンスはC言語版と完全に一致するようになった。[ 2 ]
NVIDIA はセキュリティ上重要なファームウェアの実装にも SPARK を採用しています。[ 8 ] [ 9 ]この成功を受けて、同社はファームウェア関連の他のプロジェクトにも SPARK を追加し、SPARK テクノロジーの使用に関する社内トレーニングを開始しました。[ 3 ]
2020年、Rod ChapmanはSPARK 2014でTweetNaCl暗号ライブラリを再実装しました。 [ 10 ]このライブラリのSPARKバージョンは、型安全性、メモリ安全性、およびいくつかの正当性に関する完全な自動アクティブ証明を備えており、全体を通して定数時間アルゴリズムを維持しています。SPARKコードはTweetNaClよりも大幅に高速です。[ 3 ]
{{cite web}}: CS1 maint: url-status (リンク)