Maxima で綴る数学の旅

紙と鉛筆の代わりに、数式処理システムMaxima / Macsyma を使って、数学を楽しみましょう

-セキュリティ- セキュリティの形式的証明の実世界での応用(3)

 

Formally verified software in the real world
Communications of the ACM, Volume 61, Issue 10, pp. 68-77, October, 2018

 

前回はセキュリティの形式的な証明を可能にするソフトウェアのフレームワークとしてSEL4マイクロカーネルとCAmkESという部品ソフトウェアのフレームワークの紹介をしました。特にCAmkESで記述した部品間の関係から、関係に相当するRPCのグルーコードとそのIsabelle/HOL形式の証明が生成され、アクセス制御ポリシーが強制されることが証明されます。

 

とはいえ、カメラ制御、地上からの制御通信、機体制御などヘリコプターを飛ばして任務を達成するためには大量のソフトウェアが必要です。これを全部証明するのはあまりに大変です。論文著者らはここで「セキュリティの耐震補強(seismic security retrofit)」と呼ばれる手法を提案し実装しています。

カメラ制御、地上からの制御通信、機体制御などのソフトを一から証明付きで書くのではなく、現在動いているそれらのソフトウェアをまず適切に分割した上で仮想化します。具体的にはミッションコンピュータとフライトコンピュータという二つの仮想環境を考えます。前者の中でカメラ制御や地上からの制御通信、WiFi通信などのコードを動かします。一方後者ではフライトセンサーの処理や回転翼のローター制御を行います。論文では前者の仮想環境について詳細を記述しています。ゲストOSとしてLinuxが動作し、その中でこれらの機能がレガシーコードとして実行されます。

この仮想環境とCAmkESのグルーコードをつなぐことで部品ソフトウェアを構成します。これであれば大量の証明付きコードを新しく実装する必要はありません。

またある部品ソフトウェアのネットワーク通信を制御するモジュールも部品ソフトウェアとして記述します。この場合、ミッションコンピュータとフライトコンピュータのそれぞれについてネットワーク機能が部品として、記述します。

全体のアーキテクチャは以下の図のようになります。

f:id:jurupapa:20190729215424p:plain

アーキテクチャ

(論文ではフライトコンピュータの構成は具体的には示されていないので、ここは推測です)。

 

このような構成をとることで、ミッションコンピュータで何が起ころうとも、たとえウィルスに完全に乗っ取られたとしても、それがSEL4カーネルに影響を及ぼすことはできないし、そこからフライトコンピュータに対してはアクセス制御ポリシーで許された範囲のことしかできない、ということが証明されます。フライトコンピュータが常時機体制御を行うのですから、この完全性(Integrity)には影響がないことが証明される、、、ということになります。

ちなみに論文著者らによる、証明付きのプログラム作成の利点が述べられています。プログラムの動作には外部環境や設定が必要です。従ってプログラムの動作のセキュリティに関する定理を証明するためには、外部環境の条件や設定が正しく行われることが前提となります。証明する際にこの部分の分析を詳細に行い、それを環境側、動作プログラム側に反映することで、プログラム動作がより厳密に記述されることになります。またそれができない場合にも通常のテストを含む別の検証手段を使うこともできます。

以上を正しく実行することで、ソフトウェア規模からすると、従来よりも格段に少ない努力で、AH-6のシステム全体の形式的証明を得ることができました。そして、「この一連の攻撃が航空機の安全な運行に影響を与えることはなかった」という結果が得られたのです。

ソフトウェアの仮想環境はその特性として、部品の単位として優れています。内部にリッチな機能を提供でき、外部との境界も明確です。AH-6ヘリコプターの中で仮想環境や証明済のカーネルが動いていると思うと、組み込みシステムの世界も驚くような変化を遂げていることがわかります。

 

ちなみに論文著者らによると、この方法によるシステムの形式的証明はCommon CriteriaのEAL7で要求される形式的検証よりも進んだものになっているそうです。

 

以上で本論文の紹介は終わりです。