AdaCore クエンティン・オケム（Quentin Ochem） – 2024年9月27日

AdaCoreでは、組込システム向けの高信頼性ソフトウェアを開発するためのツールを提供しています。現在、プログラミング言語では、C/C++、Ada/SPARK、Rustをサポートしています。言語を選択する際に、「どうすればよいでしょうか? 最適なものは何ですか?」と質問されます。最良の答えを出すのは難しいですが、検討すべき項目を、解説します。

C/C++のリスク

組込では、C/C++が、一般的に「デフォルト」選択肢で利用されています。ソフトウェアの大部分は、すでにC/C++で記述され、多くの開発者は言語を理解し、ツールやプロセスも整っています。変更する必要はあるのでしょうか？

C/C++では、セーフティでかつセキュアなソフトウェアを開発には不向きな場合があります。長期にわたって研究と投資が行われてきましたが、費用対効果が高く、柔軟で信頼性の高い「セーフティなC/C++」はまだ存在していません。そのため、ほかの言語を選択することもできます。

開発プロセスを改善するRustとAda の使用

新たにプログラミング言語を検討する場合、現在2つの選択肢があり、それは AdaとRustです。どちらの言語も、C/C++と比較してセーフティとセキュリティの水準が高く、それぞれ独自の強みがあります。エコシステムとコミュニティに関して、Rust には、短期間で膨大な量のリソースを開発してきた活気のあるコミュニティが存在します。ただし、商用エコシステムはまだ組織化の過程にあり、AdaCoreはそれに貢献できる技術を備えています。そのギャップを埋めるには時間がかかります。対照的に、Ada のコミュニティは小さく、長年にわたってゆっくり成長しています。ただし、Ada には、ツールチェーンの可用性と認定ドキュメントの両方の面で、成熟したエコシステムが存在します。

さらに、言語機能に関して、Rust はメモリの安全性を高め、現在、存在するプログラミング言語よりも柔軟なメモリモデルを利用できます。Adaは、ソフトウェアとハードウェアの制約を定義し、検証できる優れた仕様言語です。つぎに、Ada と Rustの比較を表に示しますので、最適な言語を選択に利用してください。

SPARK – ソフトウェアの安全性を向上させる形式手法

C/C++以外の言語を選択する際に、SPARKはAdaやRustよりもさらに踏み込んだ選択肢となります。AdaをベースとするSPARKは、採用事例も多い強力な形式手法で、ソフトウェアがセーフティでセキュアであることを数学的に証明できます。ソフトウェア開発手法におけるこのパラダイムシフトは、高信頼性ソフトウェアに大幅なコスト削減をもたらします。

SPARKを使用すると、プログラム全体が形式化され、検証可能なプロパティを静的に、つまりコンパイル時に特定できます。AdaとRustには、Adaではハードウェア制約の指定、Rustではボローチェックによるメモリセーフティなど、静的にチェックされる基本的なプロパティがあります。SPARKはこのアプローチを極限まで高め、Adaの仕様言語を使用してプロパティを形式化し、自動的に証明します。

SPARKは、最初に脆弱性を検証します。例えば、配列要素へのアクセスに使われるインデックスが範囲内であるかを検証します。多くのプログラミング言語では、範囲外のアクセスは実行時に例外を発生しますが、SPARKは、範囲外のインデックスが存在する可能性がないことを静的に証明します。

SPARKは、任意プロパティに対して、コードが仕様に準拠しているかを検証できます。それは、シンプルなものから（ミューテックスに対する呼び出し元はバランスが取れていますか？　ソート呼び出しの後、配列は本当にソートされていますか？）から、関数の入力と出力の間のより複雑な関係などまでさまざまです。

最終的に、SPARKを使用することで、さまざまなチェックツール（例えばMISRA-Cチェックツール）の使用は不要となります。数学的証明によってプロパティを100％確実に検証することで、単体テストを省略可能です。これにより、直接的なコスト削減が実現され、全体的に高いレベルの整合性が確保されます。

最良の選択肢とは？

Ada、Rust、SPARKの選択は簡単ではありません。重要なのは、開発チームの目標を特定し、新しい変化を受け入れることが許容範囲なのかに依存します。以下の表は、選択する際に参考となる要素となります。なお、この見解はAdaCoreおよびAdaCoreのお客様が物事をどのように見ているかの指標です。

コミュニティ

Rustプログラミング言語の大きな強みの1つは、大規模で活気のあるコミュニティで、言語に関するリソースや、言語に情熱を持つ人々を簡単に見つけることができます。ツールやライブラリは、継続的にコミュニティで開発され、プロジェクトを始める際に簡単に利用することができます。

AdaおよびSPARKのコミュニティは比較的小規模です。AdaおよびSPARKを学ぶための優れたリソースは存在しますが、コミュニティ提供のツールやライブラリは多くはありません。しかし、長年にわたって試練を乗り越えて、献身的な人々によって構成され、新しいメンバーも増えつつあります。
全体として、両コミュニティは（活動の幅に差はありますが）潜在的な力から恩恵を受けています。それは、セーフティとセキュリティを求めるテクノロジーへの需要の高まりと言えます。

組込ツールチェーンのエコシステム

AdaとSPARKは、組込分野において、非常に成熟したエコシステムを持っています。LinuxやWindows環境以外にも、多くのリアルタイムOSやハードウェア・アーキテクチャ用のコンパイラが存在し、ツールは静的解析から動的解析まで、あらゆる要求に対応しています。また、ツールには長期サポートが提供され、1つのバージョンを選択すれば、何年、何十年とサポートを受け続けることができます。

今日のRustは、ネイティブ／サーバー環境で定着しつつあります。組込RTOSとアーキテクチャのサポートの多くは、開発中です。多くの環境をサポートする必要があるため、入手性、特殊性から、開発には長い時間がかかります。特定の環境はすでに市販されており、その他は（AdaCoreを含め）開発中で、長期的なサポートも重要です。プロバイダによっては、ツールチェーンを頻繁に更新する傾向があり、長期にわたるプロジェクトのサポートが困難になる可能性があります。AdaCore製品では、この問題に対応できます。

ツールチェーンに関しては、時間の経過とともに洗練されていきます。どちらの言語を選択するかの基準は、今日すべての答えを得ることが重要なのか、もしくは使用する側が待つことができるのか、ということとなります。

安全認証

認証の状況は、ツールチェーンのサポートの状況と同様です。AdaとSPARKは、すでに多くの実績があり、特に組込の世界で最も一般的な規格である航空電子機器（DO-178）、自動車（ISO 26262）、鉄道（EN-50128）、宇宙（ECSS-E-ST-40C、ECSS-Q-ST-80C）など、幅広い規格の認定と認証のエビデンスを持っています。

Rustはかなり歴史の浅い技術であるため、認定を受けるまでにはまだ時間がかかります。自動車のISO-26262のエビデンスが出始めていますが、これは現在、一部の環境とRustツールチェーンの一部のサブセットに限られています。

ライブラリ

Rustプログラミング言語の特長のひとつは、カーゴ・パッケージ・マネージャから利用できる多くのライブラリがあることです。考えられるほとんどのものが、用意されています。しかし、このライブラリの多くは趣味で開発されており、最も人気のあるライブラリの多くはまだバージョン1.0です。

AdaとSPARKは、既製ライブラリの数は多くありません。2021年に開始されたAlireパッケージ・マネージャは、現在、数百のパッケージを提供しています。また、ネイティブ・ライブラリは多くはないですが、AdaとSPARKから既存のCまたはC++ライブラリへのバインディングによって対応しています。

しかし、どちらの言語についても、規制または認証要件から制約が生じる可能性があります。一般的に公開されているライブラリは、セーフティまたはセキュリティ認証を取得している組込開発には適していないからです。

プログラミング思想

プログラミング思想に関して、Ada、SPARK、Rust の間には根本的な違いはありません。いずれも命令型モジュール言語であり、オブジェクト指向の概念や類似した機能が用意されています (関数型言語などとは対照的です)。すべて静的にマシンコードに直接コンパイルされます (インタプリタ型言語などとは対照的です)。

プログラミング・エラーの回避

３つの言語はすべて、プログラミング・エラーを回避または軽減するためのメカニズムを備えています。たとえば、3つの言語は、境界を含み、動的なインデックスチェックを可能にする配列を第一級オブジェクトとして扱っています。また、初期化されていない変数、データ競合、ヌルポインタの逆参照などを回避するためのさまざまな方法も用意されています。

強い型付け

強い型付けにより、コンパイル時にオブジェクトの特定の型を決定し、その値の整合性をチェックできます。C は、弱い型付けで、変数は型付けされますが、暗黙的な変換により、暗黙のうちに異なる表現の数値を混在させることができます (たとえば、整数と浮動小数点数を追加する場合)。そのため、オーバーフロー、アンダーフロー、丸めエラーなどの問題が発生する可能性があります。配列をポインタのように扱うことは、弱い型付けから生じる問題のもう一つの例です。Rust の型付けはより強力で、明示的な変換なしで異なる型を混在できず、配列は第一級オブジェクトです。そのため、一般的なプログラミングミスを回避できます。

Ada と SPARK はさらに進化しています。型はソフトウェア設計の基本要素になります。型には名前が付けられ、プロパティに関連付けされ、静的および動的に一貫性がチェックされます。たとえば、ある浮動小数点をマイル単位の距離として宣言し、別の浮動小数点をパーセンテージとして宣言すると、明示的な変換を行わなくても、誤って混同するリスクがなくなります。同様に、緯度と経度の浮動小数点型を定義して、型システムによってサブプログラム呼び出しや演算でそれらが混同されることを防止できます。強力な型付けにより、コーディングエラーだけでなく設計の不一致も検出できます。

データ制約、ハードウェア/ソフトウェアデータの一貫性

Ada および SPARK 型では、データ範囲、表現制約条件、妥当性述語などのさまざまなプロパティを型に関連付けることができます。たとえば、パーセンテージ型は 0 ～ 100 、緯度は -90 ～ 90 度に制約できます、経度は -180 ～ 180 度に制約できます。この制約は、静的および動的検証可能です。データ構造は、特定のエンディアンを使用してメモリ内のビットレベルで指定できるため、ビット単位の演算に関連する間違いを回避できます。仕様表現の一貫性は静的にチェックされます (たとえば、構造のフィールド間に重複がないこと、型一致に指定されたビット数が取り得る値に対して十分であること、浮動小数点値の精度をハードウェアで実装できることなど)。

Rustはこの機能を備えていないため、必要に応じて、適切に定義された構造体などを使用して、従来の設計方法で対応することができます。

ランタイム・エラーがないことの保証

ランタイム・エラーとは、プログラムの実行中にチェックやアサーションによって検出できるエラーを指します。例えば、配列要素へのアクセスに使用されるインデックスが有効かどうかを検証します。AdaとRustは、データの有効性を検証するランタイム・チェックを提供しており、失敗した場合は例外を発生させるか、パニックを発生させます。これらの機能は、コード・サイズやパフォーマンスにおいて小さなフットプリントのため、バッファ・オーバーフローのような脆弱性からコードを保護することができます。SPARK は、コンパイル時に実行時エラーがないことを証明します。たとえば、SPARK は、値を範囲外に置く可能性のあるコードがないことを静的にチェックできます。そのため、パフォーマンスの低下を回避できるだけでなく、潜在的な例外/パニックに対してコードが適切に実行できる利点があります。ただし、追加の制約、アサーション、および契約（Contract）を表現する作業が増えます (後のセクションを参照してください)。

契約（Contract）言語（事前事後条件（pre- post- conditions）、不変条件（invariants）、述語（predicates）

AdaとSPARKは、ソフトウェア・エンティティ、特に型と関数に関する契約（Contract）を記述できるという点で 特徴的です。そのため、制約条件や 動的な動作の期待値を仕様の一部としてエンコードし、アプリケーション全体で妥当性をチェックすることができます。

Ada は、この契約（Contract）を、実行時に検証される動的チェックに変換します。これは、コードのサイズとパフォーマンスに影響がありますが、テスト、デバッグ、統合の段階で有用で、コンパイル時に取り除くことができます（すべて、または部分的に）。契約（Contract）のエラーは通常、例外に置き換えられます。

SPARKでは、契約（Contract）がアプリケーションが満足することを形式的、数学的に証明することができ、どのような値が操作されたかにかかわらず、指定された制約条件と機能要件が満足することが保証されます。この場合、契約（Contract）をコンパイルして動的なチェックを行う必要がないため、容量やパフォーマンスのペナルティが生じません。そのためSPARKはプログラミングの矛盾を解決する手段を提供するため検証を重視できます。

現在、Rustにはこの機能を実装できる仕様はありません。動的チェックを目的とした防御コードやアサーションによって、ある程度実現することは可能です。しかし、SPARKのように、プロパティを形式的に証明できる機能は、Rustには、今のところありません。

メモリの安全性

Rustの強力な機能の1つは、メモリの所有権モデルを通じてメモリエラーを回避できる点です。そのため、ソフトウェアにおける重大なセキュリティ脆弱性の原因を排除できます。Rustを採用し、所有権モデルに従い、ボローチェッカを満たすことで、メモリエラーを避けることができます。

最新のAda（2022年）は、ポインタ回避方法を提供し、メモリ破損のリスクを軽減します。しかし、特定のプログラミンムではポインタの使用が必要であり、明示的な所有権モデルやボローチェッカがない場合、メモリの問題が発生する可能性があります。

一方、SPARKは強力な所有権モデルとボローチェッカを追加し、Rustと同じレベルの保証を提供可能です。

導入コスト

AdaとRustの導入コストは同等です。どちらの場合も、新しい言語を習得して、ツールチェーンを導入する必要があります。影響は軽微とは言えませんが、全体的なプログラミングプロセスは殆どそのままで済みます。

SPARK採用に必要なコストは、多分それ以上かかると思われます。最初のAdaとツールチェーンと言語に関する検討事項はほぼ同じです。しかし、実際にSPARKを採用することは、異なるプログラミング方法を採用することを意味しています。効果的であるためには、形式検証を開発プロセスに統合し、ソフトウェアの設計方法を変更する必要があります。これは決して単純な決定ではなく、想定されるコスト削減効果に応じて、証明すべきプロパティを優先することもあれば、優先しないこともあります。ただし、その結果得られるメリットは極めて大きくなります。

メリット

メリットはプログラムに依存し、高信頼性開発の観点から言語を見ています。

大まかな視点では、AdaやRustを採用するメリットはよく似ています。どちらの言語もプログラミング・エラーの確率を大幅に軽減します。方法は異なりますが、どちらの言語もメモリセーフティに対応しています。Rustのメモリモデルを利用すると、現在のAdaのポインタ回避方法よりも進化していますが、Adaの強力な仕様と型付けによって、Rustには実現できない一貫性チェックが可能になります。 Adaに関する論文では、C言語と比較して、最大40%の開発コスト削減可能であることが説明されています。これには、製品に含まれる可能性が低いバグの削減は考慮されていません。

SPARKは強力な形式手法を提供し、AdaやRustの利点をはるかに凌ぐ可能性があります。開発の初期段階で多くの検証が行われるため、後段のテストやチェックは省略することが可能です。それは、SPARKで表現された制約条件や特性をチェックするような検証です。特定された動作に対する障害は、緩和されるのではなく、除外されます。不具合の代償が大きい耐用年数が長期にわたるアプリケーションの場合、言語を変更することによって大きな利益をもたらす可能性があります。

 

その他のブログ： #Ada    #Rust    #SPARK    

クエンティン・オケム（Quentin Ochem）はAdaCoreのチーフプロダクト＆レベニューオフィサーで、マーケティング、セールス、プロダクトマネジメントを統括しています。AdaCoreとの関わりは学生時代の2002年に始まり、2005年に正式に入社し、IDEとクロス言語バインディングに携わってきました。ソフトウェアエンジニアリング、中でも航空電子工学や防衛などの高信頼性領域でのバックグラウンドを有しています。その後、トレーニングやテクニカルセールスを担当するようになり、テクニカルセールス部門の立ち上げや米国でのグローバル製品管理にも携わるようになりました。2021年に現在の職務に就任し、AdaCoreの戦略的取り組みを主導しています。

2005年にマルセイユ工科大学でコンピューター工学の修士号を取得しています。

*本資料は、AdaCoreのブログを意訳したものです。正確な内容については、原文こちらをご参照下さい。