メモリ安全性を高めるAdaCoreの革新技術「CHERI」、C/C++レガシーコードの救世主に

米国政府機関や関連企業は、メモリ安全性の懸念から2026年までにCおよびC++コードからの移行を迫られる可能性があります。しかし、数百万行にも及ぶレガシーコードを抱える組織にとって、完全な書き換えは現実的ではありません。そこで注目されているのが、AdaCoreの新しいアプローチです。AdaCoreのプロダクト＆イノベーション責任者であるTony Aiello氏と、組込みターゲット製品マネージャーのJose Ruiz氏は、レガシーシステムのメモリ安全性を確保する現実的な方法について語っています。AdaCoreは、高信頼性システム開発ツールを提供する企業で、業界全体の課題に独自の解決策を提示しています。

現在、DARPAなどもソフトウェアの正確性やメモリ安全性の問題に取り組んでいますが、新規開発には有効な手法が既存システムには適用しにくいという課題が残っています。こうした中、AdaCoreが注目するのがハードウェアを活用したソリューション、「CHERI（Capability Hardware Enhanced RISC Instructions）」です。CHERIはコードを書き直すことなく、再コンパイルだけでメモリ安全性を劇的に改善できる画期的な技術です。この技術では、特殊なハードウェア命令によって実行時にメモリ安全性をチェックし、問題があればプログラムを停止します。AdaCoreは現在、このCHERI技術を活用したツールチェーンの開発を進めています。ただし、CHERIのハードウェアはまだ実験段階のため、AdaCoreはエミュレーターを提供し、実際のハードウェアがなくてもレガシーコードの脆弱性を検出できるようにしています。この方法は、ファジングテストなど脆弱性の検出試験にも効果的です。

また、CHERIを使用すると、プログラムが問題のある動作を検知すると停止するため、可用性を多少犠牲にしつつも、機密性や完全性を確保できます。一方、システムの停止が許されないようなクリティカルなコードに関しては、メモリ安全な言語であるSpark（Adaの方言）やRustへの部分的な書き換えを推奨しています。例えばNVIDIAは、セキュリティが極めて重要なファームウェアの一部をSparkで書き換え、安全性を数学的に証明しています。

AdaCoreは、C/C++、Rust、Spark向けに相互に連携できるツールチェーンを提供し、組織が徐々にセキュリティを改善しつつ既存のコードベースを維持できるよう支援しています。特にSparkは、ソフトウェアの機能的な正しさを形式的に証明することができる言語であり、事前条件や事後条件を指定して、実装がこれらの条件を満たすことを数学的に証明します。これにより実行時エラーやメモリ安全性の問題が起こらないことを事前に保証できます。また、Rustもメモリ安全性、開発者の多さ、豊富なライブラリなどの理由から急速に支持を拡大しており、AdaCoreはこれも自社のソリューションに組み込んでいます。

今後の展望としてAiello氏は、生成AIとSparkなどの形式手法を組み合わせ、安全なソフトウェア開発を迅速化する可能性にも期待を寄せています。AIが生成したコードを形式検証によって安全性を保証する仕組みが理想的だと考えているからです。メモリ安全性という重要課題に対して、AdaCoreは次のような現実的かつ多層的な対応策を提唱しています。まず、CHERIを活用したレガシーコードの脆弱性検出と緩和。次に、重要なコードをSparkやRustに戦略的に書き換える。さらに、形式検証を利用してメモリ安全性問題を数学的に証明する。これにより、組織はレガシーコードの維持という現実と、安全性改善の両立が可能となります。

AdaCoreについて
AdaCoreは、高信頼性・高セキュリティのソフトウェア開発を支援するツールを提供する企業であり、AdaおよびSpark言語を中心とした先進的な開発環境を提供しています。航空宇宙、防衛、鉄道などの安全性が重視される分野で多数の導入実績があります。