第2回 セキュリティ至上主義からセキュリティ市場主義へ

櫻庭　健年
日立製作所 システム開発研究所
Linuxテクノロジ研究部 主任研究員
2007/7/11

---

　セキュリティの証明に向けた取り組み

　米国では、OSのセキュリティの証明を実行しようとしてきました。そのために、1970年代から80年代にかけて、証明可能なOS（Provably Secure OS）、すなわち、証明できるようにOSのアーキテクチャと仕様を設計する、という研究が行われました。

　これを踏まえて、TCSEC（1983、1985）のA1レベルの認証では、ラベル制御や強制アクセス制御（MAC）といった機能の実装とともに、それらの設計に欠陥がないことを数学的に証明することを求めています。

　TCSECが世に出たころに政府主導でA1レベル汎用OSを目指して開発されたLOCK（Logical Coprocessing Kernel）では、アクセス制御の核心部をコプロセッサとしてOS本体から分離しました。また、現在、SELinuxに採用されているTE（Type Enforcement）モデルを開発することによって、コプロセッサによるセキュリティの証明を可能にしました。

　ちなみに、TEは特許になっていますが、それがハードウェアの発明として書かれていることは、このような背景を知れば納得できます。

【関連リンク】 LOCKの概要：LOCK：An Historical Perspective http://www.acsac.org/2002/papers/classic-lock.pdf

　LOCKのコプロセッサのようなアクセス制御の核心部のことを参照モニタ、あるいはセキュリティカーネル、TCB（Trusted Computing Base）などと呼びます。上に述べた「迂回不可」「tamper proof」「小規模」の3条件は参照モニタ（reference monitor）の必要条件としてよく知られています。

【関連リンク】 参照モニタ http://csrc.nist.gov/publications/history/ande72.pdf

　その後も米国政府は、セキュリティ保証を含む、OS開発プロジェクトを実施しています。大ざっぱにいって、1970年代はMultics、80年代はUNIX（LOCKもUNIXをエミュレートしています）、90年代はMach分散OSなど、そのときの旬のOSをベースとした開発を行い、2000年代のSELinuxにつなげています。90年代後半のDTOSプロジェクトでは、Mach OSに多大の貢献をしたユタ大のグループがFlaskアーキテクチャを提案しました。

　FlaskはSELinuxにも採用されていますが、いかにもMach風の分散セキュリティサーバです。LOCKではコプロセッサによって実現された「参照モニタをOS本体から分離する」という思想を、Flaskはソフトウェアによって実現したもの、と見ることができます。 　

【関連リンク】 DTOSプロジェクト http://www.cs.utah.edu/flux/fluke/html/dtos/HTML/dtos.html

　全体の流れを見ると、ハードウェアも含めてセキュリティとその保証を追求していたものが、だんだん軟化し、コモディティプラットフォームでの実現を目指すようになってきています。それでもまだ譲れないところがある、というのが第1回でも触れたラベルとパス名の論争のもとではないでしょうか。

　ラベルとパス名の議論もセキュリティ保証の観点から

　ラベルとパス名の問題も「保証」や「証明」の観点からの議論が必要です。ただしこれは、これまでに述べたセキュリティモデルや機能モデルよりも詳細な、実装レベルの問題ですので、証明は格段に困難となります。

　パス名方式の問題点はファイルの命名ルールが新たに必要となることです。これがないと次のようなことが起こります。

（1）同じファイルに複数の異なるセキュリティ属性が付く

　 別名の作成（link）やファイル名の変更（mv）によって、同時に、あるいは時間を置いて、同じファイルに異なるパス名を付けることができます。そのような状態を容認すると、それぞれのパス名について異なるセキュリティ属性が設定される可能性があります。このとき、例えば先のモデルでいうと、Hグループのパス名で機密を書き込み、Lグループのパス名で読み出せば、機密が容易にLグループに漏えいします。

　従って、同じファイルを指すパス名についてはすべて同じセキュリティ属性とするためのルールが必要です。たとえば、別名の作成や名前の変更では、新しいパス名の属性は元のパスの属性と同じでなければならず、あるパス名の属性を変更するときは、別名についても同様の属性変更を自動的に行う、といった制御が必要です。さらにこれらが破たんなく実現されることを証明しなければなりません。

（2）パス名とセキュリティ属性のデータだけでは、情報フローが分からない

　 別名をつけた場合、ファイルの実体とパス名が1対1に対応しませんから、パス名の分析だけでは、ファイルを経由した情報フローの分析に抜けが生じます。分析を正しく実行するには、実際のシステムにおいて、どれがどれの別名になっているか、という情報を追加しなければなりません。

（3）新たに作成するファイルのセキュリティ属性を記述できない

　新たに作成するファイルについては、その名前があらかじめ分かっているならば、適当な属性とともにそれを指定しておくことができます。名前が不明なときは、ワイルドカードを利用します。

　例えば/tmp/にはさまざまなプログラムがさまざまなファイルを作るので、/tmp/*と指定したいところです。しかし実際には、/tmp/に作られるファイルのセキュリティ属性は一通りではありません。従って新規ファイル名について、より精密な設定が必要になります。

　 新規ファイルのセキュリティ属性を定める別のアプローチは、作成時の条件に基づいて属性を定める、というルールを設けることです。

　たとえば先のモデルでは、新規作成ファイルの属性は、作成したユーザーの属性に合わせ、新規作成リンクの属性はリンク先のファイルの属性と同じにする、というルールが妥当です。この場合、個々のプログラムの詳細に立ち入らずに、ルールの正当性の確認が可能です。パス名での指定と生成時のルールが矛盾するときは、新たな作成は不可、などとしておけば、パス名方式の場合にも適用できるでしょう。

　いずれにせよ、パス名方式の導入は、新たなルールと機能の導入を伴い、システムの複雑さが少なからず増大することは間違いありません。

2/3

Index
セキュリティ至上主義からセキュリティ市場主義へ
	Page1 何を守るためのセキュリティなのか？ 「セキュリティの証明」問題をブレイクダウンする まずはセキュリティモデルを考える OSによるセキュリティルールの強制
	Page2 セキュリティの証明に向けた取り組み ラベルとパス名の議論もセキュリティ保証の観点から
	Page3 証明によるセキュリティ保証の課題 息抜きコラム：第2回「トラステッドOSとTCSEC」

Security&Trust記事一覧

＠ITメールマガジン　新着情報やスタッフのコラムがメールで届きます（無料）