Maxima で綴る数学の旅

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

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

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

の論文紹介の続きです。今回は形式的証明を可能にするソフトウェアのフレームワークを紹介します。次回ではこのフレームワークを利用した実機のソフトウェアアーキテクチャの紹介となります。

 

まずは機体全体を制御するOSが必要です。OSと言っても実際にはハイパーバイザと考えてください。ここには論文著者らが以前に開発した証明済のマイクロカーネルSEL4を使います。またその上で動作する部品ソフトウェアのフレームワークとして、こちらも論文著者らが以前に開発したCAmkESを用います。

SEL4は機能として、その上で動作する部品ソフトウェアの分離性および部品ソフトウェア間の通信チャンネルが提供されています。このため部品ソフトウェアがどのように動作しても、(1) SEL4の提供されている通信チャネル以外ではお互いに影響を及ぼすことができない仕組みです。また(2) 通信チャンネルにはアクセス制御ポリシーが強制されるため、部品ソフトウェア間でポリシーで許される以上の書き込みアクセスは発生しません。SEL4では(1)の性質を「権限の制限」、(2)の性質を「完全性(integrity)」と呼んでおり、これらの2つの性質が、数学的に証明されています。またこの完全性の双対として秘匿性(ある部品ソフトウェアが別の部品ソフトウェアの情報を通信チャンネル以外の手段で知ることは出来ない)も証明されています。

この完全性と秘匿性の双対はBell-LaPudula秘匿性モデルとBiba完全性モデルの双対性の類似と考えられそうです。

 

部品ソフトウェアはCAmkESプラットフォームを利用して、その間の関係を記述します。この関係は実際には部品ソフトウェア間の可能な通信プロトコルであり、実装的にはRPCです。CAmkESは関係の記述からRPCのグルーコードを生成し、システム実装者はこのグルーコードを埋めます。CAmkESはグルーコードと同時に形式証明システムIsabelle/HOLの形式で証明も出力します。従って、グルーコードが関係を満たしていることは証明されていることになります。

またCAmkESを使って部品の初期生成も記述します。ここでも実装コードが生成されます。この初期生成の記述がそのままシステムの動作中に強制されるアクセス制御ポリシーになります。

これらの関係を表した図が下記となります。

 

f:id:jurupapa:20190729000948p:plain

ソフトウェア フレームワーク

次回はAH-6の場合に部品ソフトウェアをどう作り、全体の動作をどう保証するか、というアーキテクチャの話になります。