News
ブログのお知らせ一覧です
メモリ・セーフティに関わるバグは、ソフトウェアのセキュリティや信頼性に深刻な影響を与える原因となります。実際、Google や Microsoft などの大手テクノロジー企業は、報告されているセキュリティ脆弱性の70％以上が、こうした問題に関連しているとしています。これらのリスクを効果的に減らすためには、プログラミング言語の設計段階でメモリ・セーフティを確保することが非常に重要です。
本ホワイトペーパーでは、境界外書き込みやユーズ・アフター・フリー、ヌル・ポインタ参照といった、よく見られるメモリ・セーフティのバグについて説明します。あわせて、Ada、SPARK、Rust といったプログラミング言語が、これらの問題にどのように対応しているのかを解説します。
DO-178C/ED-12Cの正式名称は「Software Considerations in Airborne Systems and Equipment Certification」で、民間航空機に搭載されるソフトウェアの妥当性を規定する認証規格です。section1.1には次のように記載されています：
「この文書の目的は、耐空性要求に準拠し、確実な安全性で、その機能を達成する航空機システムおよび搭載機器用のソフトウェアを開発するためのガイダンスを提供します。」
このガイダンスは、次の内容で構成されています：ソフトウェアライフサイクルプロセス（software life cycle processes）に関連するobjective
ソフトウェア・レベルは、どのガイダンスが、どの程度厳密に適用されるかを定めています。また、ソフトウェア異常が耐空性／パイロットの業務負荷に与える影響に基づいており、安全性評価（system life cycle process）の中で決定されます。DO-178C/ED-12C規格でのソフトウェア・レベルは、D (軽微な障害状態につながる可能性) から A (壊滅的な障害につながる可能性） までの範囲です。その主な目的は検証プロセスで、検証はソフトウェアライフサイクルプロセス（software life cycle process）の成果物を技術的に評価することです。レビュー、解析、テストを通じてソフトウェア開発中に発生したエラーを検出し、報告します。
section6.3には以下のように記載されています：
レビューは認証で必要なエビデンスの必須項目です。具体的に、レビューはDO-178C/ED-12Cの以下のsectionに準拠しています
以下のDO-178C/ED-12C sectionは、追加の「レビュー」アクティビティを定義していますが、ソフトウェア検証プロセスとは異なるため本稿の対象外です。
本稿は、DO-178C/ED-12Cの観点から効果的なレビューを行うためのフレームワークを定義し、活用する方法を紹介するブログの第1回目です。ツールのレビュー・フレームワークを実現する前に必要なステップは以下の通りです。
本稿では、DO-178C/ED-12Cのレビューobjectiveを効率良く達成するための制約（独立したエビデンスの記録、レビューする構成項目など）を特定します。続いて、2つの項目について説明します。
レビューの主な目的は、DO-178C/ED-12Cでは必須で、開発プロセスの初期段階で潜在的なソフトウェアの欠陥、エラー、不整合を特定し、修正することです。特に、アクティビティが自動化（認定された）ツールで実行されない場合に重要です。
DO-178C/ED-12Cのソフトウェアレビューアクティビティには、重要な要素が含まれています。
DO-178C/ED-12Cのレビューの最初のタスクは、ソフトウェアライフサイクルデータ（software life cycle data）の8つのカテゴリーに分類されたレビューと解析のobjectivesに注目することです。
下図は、ソフトウェア検証プロセスにおいてレビューのために提出されるソフトウェアライフサイクルデータ（software life cycle data）の概要を示しています：
DO-178C/ED-12Cのsection6.3「Software Reviews and Analyses」とsection6.4.5「Reviews and Analyses of Test Cases, Procedures, and Results」には、31のレビューと解析objectivesが明示されています。そのため、レビューの目的は、Objectivesが達成されたことを明確にすることです。そして、適切な検証方法を選択し、検証対象に焦点を当てる必要があります。
先に示した方法論を適用するために、レビューまたは解析を通じて、すべてのsoftware life cycle data（上位要求(high level requirements)、下位要求(low level requirements)、ソフトウェア・アーキテクチャ、ソースコード、実行可能オブジェクトコード、テストケース、テスト手順、およびテスト結果など）が、Objectivesを達成していることを確認する必要があります。
解析は再現可能なエビデンスとして妥当性を示し、レビューは定性的に妥当性を評価します（DO-178C/ED-12C 6.3項）。レビューの工数を削減する一つの解決策は、DO-333/ED-216 「Formal Methods Supplement to DO-178C/ED-12C and DO-278A 」を用いて、レビューを形式手法で解析することで 補完または置き換えることができます。「形式手法はライフサイクルの初期段階でエラーを特定できるため、プロジェクト全体の工数を削減することができます。(DO-333/ED-216 Section FM.B.1.4.4 Reduce Effort)
例えば、「上位要求(high level requirements)が正確で、曖昧さがなく、詳細な」objectiveであれば、要求が形式記述されていれば、形式解析で処理することができます。また、「上位要求(high level requirements)が形式記述されていれば、正確で曖昧さはなくなります。さらに、上位要求(high level requirements)の形式モデルは、一貫性（矛盾のなさ）を確認することが可能で、形式解析を用いて正確性を検証することができます。」(DO-333/ED-216section6.3.1 b)。
実際に、従来のソフトウェア開発では、次のようになります：
31個のDO-178objectiveのうち、29個以上のobjectiveがレビューによって検証されます。
形式記述では、次のようになります：
準形式記述を用いると、検証するレビューobjectivesを減らしたり、工数を軽減したりすることが可能になります。さらに、規定や規則に従うことで、その柔軟性や解釈の幅が拡がります。この記述法は、必ずしも絶対的な正確さが要求されない場合や、形式記述と可読性を両立させる必要がある場合に用いられます。以下は、EARS構文を使用した例です（EARSはEasy Approach to Requirements Syntaxの略で、テキスト形式の要求を適切に制約するメカニズムです）。EARS 形式の構文は、体系化されたガイダンスを提供するため、品質の高いテキスト要求を記述できるようになります：
When the input A is below 20 [amperes] for more than 10 [milliseconds], the function B shall set the output C to ACTIVE
（入力Aが20 [アンペア]を下回る時間が10 [ミリ秒]を超える場合、関数Bは出力CをACTIVEに設定します。）
要約すると、評価を自動化（レビューを解析に切り替える）、または、形式あるいは準形式記述を用いることで、レビュープロセスを簡素化できます。
DO-178C/ED-12Cでは、準拠すべき特定のレビュー方法を定めていません。ただ、「レビューは、チェックリストまたは類似した方法で示されたプロセスの成果物で検証を行います。」(6.3 Software Reviews and Analyses)。
代わりに、正確性、精度、完全性、検証可能性など、達成すべきobjectivesと基準（criteria）を規定しています。その結果、文書に定められた基準（criteria）を満たす限り、レビュー方法を選択することが可能になります。
一般的には、ウォークスルー（walk-through）とインスペクション（inspection ）という2つのレビュー方法を用います。２番目の方法は、問題点をより明確にしますが形式化が求められます。
ウォークスルー方式は一種の査読であり、成果物を複数の担当で確認します。ロジック、構造、機能を理解することに重点が置かれ、形式にとらわれず内容を理解することを目的としています。
インスペクション（inspection method）は、1970年代にマイケル・フェイガン氏（Michael Fagan）によって提唱された検査法で、より形式的なプロセスで、管理者（moderator）が複数のレビューアーとともに成果物をレビューします。あらかじめ定義された基準（criteria）または規格（standard）に従って、成果物を検証します。
以下の点に注意することで、効率の低下や工数の増加を防止できます。最初の3つの制約は、構成の明確化、独立性、可用性です。
最後の3つは、工数を削減し、管理を容易するための手段となります。
DO-178C/ED-12Cでは、レビューした構成項目を明確化することが重要です。
DO-178C/ED-12Cは、レベルAまたはBのソフトウェアのレビュー・アクティビティにおいて、独立性を重要視しています。独立性とは、ソフトウェア開発と検証アクティビティの客観性、正確性、徹底的な精査を明確にすることが基本原則です。さらに、レビュー対象となるソフトウェアライフサイクルデータ（software life cycle data）の開発者以外の担当者がレビューすることが独立性となります。ツールを使用することで、人による検証アクティビティと同等のレベルを達成することが可能です（DO-178C section6.2-e）。ソフトウェア・レベルAでは31項目中16項目（レベルBでは31項目中7項目、レベルC、Dでは該当なし）レビューobjectivesは、独立性を満たす必要があります。
レビューの独立性は、レビューのobjectivesを達成するために不可欠ですが、同時に、必要とされる工数に影響を及ぼす可能性があります：
– 人員の追加
– 必要な人員や専門知識を有する人員のスケジュール調整
– 文書化及びトレーサビリティの記録などの管理により全体的な経費の増加
レビュー・レコードはコンプライアンスのエビデンスで、認証機関から要求されることがあります。したがって、データとデータベースが監査に使用できる場合、データベースからレビュー・レコードをエクスポートして成果物文書を作成する義務はありません。
文書の書式は、DO-178C/ED-12Cに準拠したレビューおよび解析の効率に影響を及ぼすことがあります。構造化された文書では、レビューは効率化され、レビューアーが要求事項への準拠を適正に審査できます。「文書が念入りに作成されていれば、長期間にわたって有用なものとなります。 反対に、広範にわたって活用されるのであれば、きちんと作成される価値があります。」A Rational Design Process: How and Why to Fake It、Parnas、Clements、1986
DO-178C/ED-12Cは、レイアウトや見栄えではなく、内容に重きが置かれています。そのため、文書は自由な書式や構成（例えば、データベース）をとることが可能です。レビューの工数を削減するために、「少ないほど良い（less-is-more）」ルールを適用し、詳細を必要なものだけに限定し、レビューアーが、全体像を把握できるようにして、適切に詳細を管理することが重要です。
最後に、ソフトウェア要求のレビューを自動化するために、自然言語処理（NLP）ツールで処理できる形式で表現可能な要求の記述ルールを定義する必要があります。
ソフトウェア・アーキテクチャとそのソースコードへの実装に関するDO-178C/ED-12Cレビューおよび解析のobjectivesは次の通りです：
工数は、コンポーネントの定義、データフロー、コントロールフローの定義ならびに検証にツールを利用するかで大幅に異なります。DO-178C/ED-12Cでは、構成要素の規模や複雑さは、独立したソフトウェア・ モジュールまたは関数に始まり、サブシステム またはアプリ全体といった大規模なソフトウェア・ ユニットに至るまで、多岐にわたります。ここでは、DO-178C/ED-12CとDO-248C/ED-94Cに準拠したプロパティを紹介します：
したがって、ソフトウェア開発戦略に最も適したソフトウェア・コンポーネントの範囲を選択することが求められます。
プロジェクト管理に関する考慮事項はDO-178C/ED-12Cの範囲外ですが、時間や人員などのリソースが限られているため、レビューの範囲と深さが制限される可能性があります。重要なレビュー・アクティビティに優先順位を付け、品質を損なうことなくレビューがタイムリーに行われるよう、リソースを効果的に割り当てる必要があります。
この制約は、査読コメントが 「Status」、「Category 」または 「Severity 」のプロパティを含みます。
査読コメントを分類することが重要であるもう一つの理由は、EASAとFAAと連携して開発されたアドバイザリーサーキュラーadvisory circular（AC）であるAC 20-189 “Open Problem Reports (OPRs)” による未解決の問題報告書を管理することです。
本稿では、DO-178C/ED-12Cのレビューおよび解析objectiveから得られる制約事項に焦点をあて、DO-178C/ED-12Cに準拠するために最低限のレビュー・フレームワークを記述する仕様書を書くための基礎を解説しました。次回は、DO-178C に準拠し、可能な限り効率的で最小限の実行可能なレビュー・フレームワークを定義する方法を解説します。
著者
———————————————————————————————————————————————————————————————————————–
オリヴィエは認証エンジニアで、2022年にAdaCoreに入社しました。航空機ソフトウェアの認証分野で20年以上の経験を持ち、DO-178ソフトウェア安全認証規格に精通しています。AdaCoreでは、認証可能なアプリケーションに適したGNATランタイム・ライブラリを担当しています。
————————————————————————————————————————————————————————————————————————-
ジョスエは2022年よりAdaCoreの認証チームに所属しています。航空業界におけるソフトウェア、ハードウェア、飛行管理・誘導機能の認証に携わった経験を持っています。AdaCoreでは現在、ツール認定に従事し、ランタイム認証活動（ activities.）をサポートしています。
*本資料は、AdaCoreのブログを意訳したものです。正確な内容については、原文こちらをご参照下さい。
AdaCore クエンティン・オケム（Quentin Ochem） – 2024年9月27日
AdaCoreでは、組込システム向けの高信頼性ソフトウェアを開発するためのツールを提供しています。現在、プログラミング言語では、C/C++、Ada/SPARK、Rustをサポートしています。言語を選択する際に、「どうすればよいでしょうか? 最適なものは何ですか?」と質問されます。最良の答えを出すのは難しいですが、検討すべき項目を、解説します。
組込では、C/C++が、一般的に「デフォルト」選択肢で利用されています。ソフトウェアの大部分は、すでにC/C++で記述され、多くの開発者は言語を理解し、ツールやプロセスも整っています。変更する必要はあるのでしょうか？
C/C++では、セーフティでかつセキュアなソフトウェアを開発には不向きな場合があります。長期にわたって研究と投資が行われてきましたが、費用対効果が高く、柔軟で信頼性の高い「セーフティなC/C++」はまだ存在していません。そのため、ほかの言語を選択することもできます。
新たにプログラミング言語を検討する場合、現在2つの選択肢があり、それは AdaとRustです。どちらの言語も、C/C++と比較してセーフティとセキュリティの水準が高く、それぞれ独自の強みがあります。エコシステムとコミュニティに関して、Rust には、短期間で膨大な量のリソースを開発してきた活気のあるコミュニティが存在します。ただし、商用エコシステムはまだ組織化の過程にあり、AdaCoreはそれに貢献できる技術を備えています。そのギャップを埋めるには時間がかかります。対照的に、Ada のコミュニティは小さく、長年にわたってゆっくり成長しています。ただし、Ada には、ツールチェーンの可用性と認定ドキュメントの両方の面で、成熟したエコシステムが存在します。
さらに、言語機能に関して、Rust はメモリの安全性を高め、現在、存在するプログラミング言語よりも柔軟なメモリモデルを利用できます。Adaは、ソフトウェアとハードウェアの制約を定義し、検証できる優れた仕様言語です。つぎに、Ada と Rustの比較を表に示しますので、最適な言語を選択に利用してください。
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）を表現する作業が増えます (後のセクションを参照してください)。
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で表現された制約条件や特性をチェックするような検証です。特定された動作に対する障害は、緩和されるのではなく、除外されます。不具合の代償が大きい耐用年数が長期にわたるアプリケーションの場合、言語を変更することによって大きな利益をもたらす可能性があります。
クエンティン・オケム（Quentin Ochem）はAdaCoreのチーフプロダクト＆レベニューオフィサーで、マーケティング、セールス、プロダクトマネジメントを統括しています。AdaCoreとの関わりは学生時代の2002年に始まり、2005年に正式に入社し、IDEとクロス言語バインディングに携わってきました。ソフトウェアエンジニアリング、中でも航空電子工学や防衛などの高信頼性領域でのバックグラウンドを有しています。その後、トレーニングやテクニカルセールスを担当するようになり、テクニカルセールス部門の立ち上げや米国でのグローバル製品管理にも携わるようになりました。2021年に現在の職務に就任し、AdaCoreの戦略的取り組みを主導しています。
2005年にマルセイユ工科大学でコンピューター工学の修士号を取得しています。
*本資料は、AdaCoreのブログを意訳したものです。正確な内容については、原文こちらをご参照下さい。
Ferrocene言語仕様（ドラフト）の公開を発表
AdaCoreは、2月にFerrous Systemsとのパートナーシップを発表後、自動車、航空、宇宙、鉄道などの高信頼性市場におけるRustユーザ向けに、Ferrocene Rustツールチェインを各業界のソフトウェア安全規格で認定されることを目標に、開発を進めています。
現段階では、ツール資格認定作業は主に文書化に重点を置いています。また、Ferrocene Language Specification (FLS) の最初のドラフトの公開を発表できることを嬉しく思っています。これは、Ferrocene に関連する Rust 言語を詳細に説明する認定取得用のドキュメントです。
FLS の取り組みは、既存の Rust 言語ドキュメント、Ferrous Systems の Rust の技術的専門知識、およびプログラミング言語の標準化とソフトウェアの安全規格認定取得における AdaCore の経験が役立っています。私たちは、Ada言語標準とその定義であるAdaリファレンスマニュアルの進化に長年積極的に関与してきましたが、FLSを記述するにあたって、その構成と詳細度からアイデアを得ています。
FLS の初期開発は主に Ferrous Systems と AdaCore の共同作業ですが、ドキュメントは現在 GitHub で公開されており、Rust の標準的なオープンソースライセンスの下で公開されています。FLSは年内に完成させる予定で、オープンな立場で FLS を改善し続けます。 Rust の意思決定プロセスを置き換えることはなく、 ドキュメントは進行中の Rust プロジェクトの変更、決定、および Request for Comments (RFC) に対応し、コミュニティからのコントリビューションを考慮するよう最善を尽くしていきます。 詳細については、コントリビューションガイドラインを確認してください。
Ferrous Systems、AdaCore、Ferroceneにご興味がある場合は以下へご連絡をお願いします。
*本資料は、AdaCoreのブログを意訳したものです。正確な内容については、原文をご参照下さい。
2022/03/10
AdaCoreとFerrous SystemsがRust言語サポートで提携
AdaCore は、25年以上にわたり、セーフティ/ミッションクリティカルが重要な業界のニーズをサポートすることに取り組んできました。当初、プログラミング言語Ada/ツールチェーンに重点を置き、長年にわたって、多種多様な技術に拡張されてきました。最新の製品では、Ada言語、形式検証可能なSPARK言語、C言語、C++言語ならびにSimulink®/Stateflow®モデルに対応するツールがサポートされています。DO-178B/C, EN 50128, ECSS-E-ST-40C / ECSS-Q-ST-80C, IEC 61508, ISO 26262などの安全規格へも対応しています。
約10年前、信頼性を向上するために、業界全体のプログラミング手法の改善を目指して、新しいプログラミング言語「Rust」が登場しました。その技術は進化を遂げ自動車などの高い信頼性が要求される組込市場にも訴求しています。このような背景からFerroceneテクノロジーをベースにセーフティクリティカルで、かつ認定済のツールチェーンを提供することを目的に、RustコミュニティメンバーによってFerrous Systemsがドイツに設立されました。
AdaCoreとFerrous Systemsは異なる手法で、Rust言語をサポートすることを考えていましたが、技術面でもビジネス面でも、基本的な思想とアプローチが同一であることに気づきました。両社は、優れた言語使用の促進、オープンソースソフトウェアに対するコミットメント、ソフトウェア認証に対する方向性、技術面での共通性がありました。結論として、両社が提携することで、安全認証を取得したRustツールチェーンをより迅速に信頼性が重要視される業界に投入できると判断しました。
Ferrous SystemsとAdaCoreは、自動車、航空電子、宇宙、鉄道などのソフトウェア認証に対応するために安全認証を取得したRustツールチェーン「Ferrocene」を共同開発することを2022年2月2日に発表しました。
AdaCore プレスリリース：
https://www.adacore.com/press/adacore-joins-forces-ferrous-systems-support-rust
Ferrous Systemsは、Rustツールチェーン「Ferrocene」を、技術的専門知識とRustコミュニティとの関係を活用して、ミッション/セーフティクリティカルな組込ソフトウェア開発向けに、ツールを整備していきます。AdaCoreにとって、長年のAda言語への取組みを補完し、安全認証で認定されたAdaツールチェーンで培った専門知識をRustコミュニティに提供する機会となります。
セーフ/セキュリティクリティカルな分野では、Ada言語とRust言語の両方が必要とされています。
具体的には、Ferrocene（Rustコンパイラ）が各種安全規格の認定を取得し、動的・静的解析ツールの開発ならびに認定も取得する予定です。また、安全認証を取得した言語サポート（libcore）やユーザライブラリ開発、ならびに各分野で使用されるアーキテクチャやオペレーティングシステム向けの製品開発を目指しています。このビジョンの実現には時間がかかりますが、Ferrous SystemsとAdaCoreは特定の分野から開発を進めていきます。最終的には、高信頼性アプリケーションの開発で使用される他プログラミング言語と同様に、Rust言語を包括的にサポートすることを目標としています。
当初はRustアプリケーションに焦点を当てますが、Rust言語とAda言語への長期的な取り組みは、両方の言語を併用することを考慮して、双方向のバインディングジェネレータの開発など、両言語の相互運用性を検討しています。また、Ada言語とRust言語の両方のユーザが使用できるように、SPARK言語で形式検証され認定されたライブラリを開発して、相互運用することも考えています。
このように、Rust言語とAda言語の両コミュニティの協力関係によって、新たな時代の幕開けとなることを期待しています。今後、更なるニュースをお届けしていきます。
*本資料は、AdaCoreのブログを意訳したものです。正確な内容については、原文をご参照下さい。 https://blog.adacore.com/
| ソフトウェアの安全性、信頼性を確保するための形式検証手法とは |
本日は、6月30日弊社開催のWebinarにて形式手法の活用の事例をご紹介頂いた株式会社ジェイテクト ステアリングシステム統括部上席主担当 米木真哉様に自社の製品開発へ形式検証を使用するに至る経緯や、これまでの自社の取組でのSPARK適用の効果や課題などのお話を伺いました。
| 出典：JTEKT 米木様 Webinar資料より |
先日はWebinarでのご講演ありがとうございます。本日は御社の開発において、形式検証を適用することになった経緯や、AdaCore社のSPARKにこれまで取り組んできて良かった点や課題となる点について、お話を伺えればと思います。よろしくお願いいたします。
●はじめに、御社の事業紹介をお願いします。
「弊社の柱となる事業として、電動パワーステアリング（EPS）があります。1988年に量産、生産開始から現在まで世界トップシェアを維持しており、より安全で快適な、自動運転に対応する技術研究開発をすすめています。」
| 形式検証の可能性とAdaCore社SPARKの適用範囲 |
●形式検証を使用するに至る経緯は何ですか？
「自動運転やステアバイワイヤ等の技術開発の過程で、ソフトウェアの安全性の論証が課題となったことが直接の背景になります。自動運転やステアバイワイヤでは、ソフトウェアの不具合が安全上重大な影響を引き起こす可能性があることから、従来のソフトウェア開発に加えて、形式検証を用いることで本質的にソフトウェアの不具合を開発の早い段階で確実に排除できる可能性があると考えました。」
●SPARKに決定した理由を教えてください。
「SPARKは自動車業界以外では既に実績を積み上げていること、開発環境が比較的しっかりと整備されていること、の2点が大きな理由になります。」
●SPARKをどのようなプログラムに応用していますか？」
「現時点では、どのプログラムから適用すべきかについて、実際の製品ソフトを例題に検討を進めているところですが、先ずは小・中規模のソフトウェアコンポーネントから徐々に適用範囲を拡げていくことを検討しています。」
●SPARKのプログラムの適用範囲、方法を教えてください。●
「上記3.のとおり、現時点では明確に適用範囲を決定した訳ではありません。C言語との共存させることも可能であることから、SPARKの持つ機能とC言語に対する既存の検証の枠組みとを有機的に融合させ、より高いレベルで安全性の論証が提供できるようにするという利用方法を検討中です。」
●Contractの適用は、容易に行えましたか？
「論証したい内容にもよりますが、特に定理証明を行う際のcontractについては、ある程度以上のノウハウが必要と感じています。」
| SPARKの利点とは？ |
●御社からみたSPARKの長所、短所を教えてください。
「現状分かっている長所としては、コーディングの時点で検証をほぼ平行して行えること、結果として単体テスト項目ができる可能性があることがあります。将来的には演算処理結果が安全上許容可能な範囲を逸脱しないことの検証といった、テストだけでは完全に論証することが難しい領域への応用についても、潜在的な長所と捉えています。また、これらの様々な観点からのソフトウェアの静的な検証を全て一つのツールで行うことができることも利点であると考えます。
一方、短所ですが、プログラムをAda/SPARKで作成する必要があることが挙げられます。現在、組込みソフトウェアエンジニアの大半がC言語に慣れていることもあり、新たにAda/SPARKに取り組まなくてはなりません。また同じ理由から、C言語で記述された過去のソフトウェア資産が利用できなくなることも短所のひとつと考えます。」
●SPARKの拡張性（モデルベースへ）は考えていますか？
「モデル開発への適用について、現時点では具体的な計画はありません。しかし、モデルで記述した制御仕様の検証にSPARKが応用できるのであれば、取り組んでみたい題材であると考えます。」
| 今後の取組について 今後の展開を教えてください。 |
「まずは、弊社のソフトウェア開発の中で、複雑なcontractを記載せずに、比較的容易にSPARKの特徴が生かせるユースケースを洗い出すことが当面の目標になります。その上で、実際の製品開発の中で、段階的にそれらのユースケースに対してSPARKの導入を進めて行くことまでが最初のステップになります。
次の段階として、contractを積極的に活用しソフトウェアの演算結果に対する安全性の論証に駒を進めて行きたいと考えています。」
 ジェイテクト 米木様 |
米木様、どうもありがとうございました。Webinarおよび本対談で御社が形式手法に取り組んでいる経緯やこれから直面されるであろう課題など、いろいろとお話を頂戴できまして大変参考になりました。また今回挙げられた課題を越えた際には、またお話をお聞かせください。
公開日：2021年11月15 日
RISC-V ISAの脆弱性
NVIDIA社は、SPARKを使用して、安全性やセキュリティが重要なファームウェア（develop safety- and security-critical firmware applications.）を開発しています。DEF CON 29会議では、ハッカーZabrocki氏とMatrosov氏（Zabrocki and Matrosov）が、SPARKで記述されたファームウェアに対する攻撃方法（attacking NVIDIA firmware written in SPARK）を発表しました。結論として、ファームウェアではなくRISC-V ISAを攻撃することになりました。
Zabrocki氏は、まずNVIDIAでのレッドチーム活動（the context for their red teaming exercise at NVIDIA）について解説し、続いてSPARKの概説とセキュリティ攻撃の観点から言語の評価（their evaluation of the language from a security attack perspective）を行っています。Zabrocki氏は、Ghidraの拡張機能を使ってGNATが生成したバイナリコードを逆コンパイルする方法（extension of Ghidra to decompile the binary code generated by GNAT）を紹介し、その逆コンパイルによってRISC-V ISAに発見された脆弱性（how they glitched the NVIDIA chip to exploit this vulnerability）について述べています。さらにMatrosov氏は、この脆弱性を利用してNVIDIAチップにどのような細工を施したか（how they glitched the NVIDIA chip to exploit this vulnerability）を説明しています。最後に、Zabrocki氏は、RISC-Vプラットフォームを強化するためのプロジェクト（projects used to harden RISC-V platforms）について語っています。
この発表で驚かされることは、NVIDIAチームがSPARKを使用して、ソフトウェアにランタイムエラーが無いことを証明しています。 結果、ファームウェアは保護されています。そのため、ハッカーたちはソフトウェアの脆弱性を検出できず、RISC-V ISA自体の問題点の発見に至りました。
Zabrocki氏は、メモリの枯渇はSPARK/GNATprove検証ツール（memory exhaustion issues are not detected by the SPARK tool, GNATprove.）では検出できないことを指摘しています。代わりに、GNATstackを使用して問題点を検出する必要があります。これは、SPARKで検出できない機能要件と言えます。また、リアルタイムソフトウェアのタイミング制約や、衛星ソフトウェアの宇宙線に対する堅牢性などは検出できません。最後に、SPARK Pro 2020で追加された機能としてのポインタをサポート（an enhancement added in SPARK Pro 2020）、ならびに、ツールで検出される問題のクラスがツール内で明確に定義（the classes of problems detected by the tool are clearly defined in the tool）されています。
本資料は、AdaCore のブログを意訳したものです。正確な内容については、原文をご参照下さい。
原稿タイトル When the RISC-V ISA is the Weakest Link
https://blog.adacore.com/
まずはお気軽に
お問い合わせください！
