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

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

歴史的な経緯からセキュアOSは複雑な出自をもっています。第1回で紹介した「至上主義派」と「カジュアル派」という二つの流派、今回はセキュリティ至上主義派の考え方と歴史を基に、その来し方行く末を考えてみたいと思います（編集部）

---

　セキュリティ至上主義派の思想の根本は、セキュリティの保証の追求にあると考えられます。今回はセキュリティ至上主義の歴史をひもとくことで、セキュアOSの成り立ち、そしてなぜ思想がぶつかり合うのかを紹介していきたいと思います。

　何を守るためのセキュリティなのか？

　セキュリティは、守るものの価値によって、かける手間やお金、適用する手段が違ってきます。セキュリティで守るべき最も価値のあるものとは何でしょうか。

　歴史的に見て、それは「国家」だったようです。つまり、政府や軍事的防衛組織のセキュリティが最も責任が重い。具体的には、政策や防衛に関する計画や情報を秘匿して、外敵から国民の安全を守ることがその目的です。

　特に、米国では、コンピュータの始まりのときから、政府の手によって、大変熱心に情報セキュリティに対する研究と投資が行われてきています。米国国防総省（DoD：United States Department of Defense）、アメリカ中央情報局（CIA）、連邦捜査局（FBI）などを含む、インテリジェンスコミュニティがセキュリティの研究と実践の中心です。OSのセキュリティについても、国家安全保障局（NSA：National Security Agency）や国立標準技術研究所（NIST：National Institute of Standards and Technology）が研究をリードしてきました。

　国家を守るというレベルのセキュリティは、失敗するとダメージが大きすぎますから、「絶対」が求められます。しかし、人間のやることに「絶対」はありません。そこで、どうするかというと、セキュリティを論理的に「保証」しようとします。保証の方法はいろいろあり得ますが、最も説得力のあるのが、セキュリティを数学的に証明することです。論理的にあり得ないことは起こらない、というわけです。

　「セキュリティの証明」問題をブレイクダウンする

　では、どうすればセキュリティの証明ができるのでしょうか。

　まず、組織や情報を抽象化し、そこで守られるルールを決めます。これがセキュリティモデルです。そして、セキュリティモデルの中では、（起こり得ることは）何が起ころうとも、ルールが守られている限り、情報の漏えいや破壊は起こらない、ということを証明します。

　かくして問題は、

• セキュリティモデルを作り、セキュリティを証明すること
• そのモデルが実際の組織に当てはまること
• そのモデルが前提としたルールを、組織が確実に守ること（を証明すること）

に帰着されました。

　まずはセキュリティモデルを考える

　まず、セキュリティモデルの例を紹介しましょう。モデルは実際のシステムにうまくマッピングでき、セキュリティの証明が実行可能であるように構成する必要があります。

【関連リンク】 アクセス制御に関するセキュリティポリシーモデルの調査 http://www.ipa.go.jp/security/fy16/reports/access_control/policy_model.html

　秘密情報を守るためのセキュリティモデルとして、ドロシー・デニングによって整理された、「情報フローに関する束（lattice）モデル」が有名です。BLP（Bell-LaPadula）モデルはこれの特殊化、詳細化と考えられます。情報フローモデルの基本原理を以下に説明します。

図1　簡単なセキュリティモデル

　いま、秘密情報が1つ存在したとします。これを情報Sとしましょう。組織のメンバーは、情報Sを参照してよい人たちのグループHと、参照してはいけない（参照させてはいけない）人たちのグループLに明確に分けられます。さらにファイルについても情報S（およびSから作成された2次情報）を格納してよいものと、そうでないものに分けます。

　初めに情報Sが参照してよい人たちの側にあり、その後の操作で、参照してよい人たちから参照してはいけない人たちへの情報の伝播を、情報の内容にかかわらず、すべて禁止する、というルールを設けます。このとき、参照してはいけない人たちが情報Sを参照することはあり得ないことは明らかでしょう。これを情報Sの秘匿性を守るためのセキュリティモデルと考えることができます。

　次に、これを実際の組織に当てはめます。まず、組織のメンバーを明示的にグループHとグループLに分けなければなりません。これの実現方法には、ユーザーやファイルそのものに「L」あるいは「H」のラベルを貼り付けて区別するラベル方式と、ユーザーやファイルに名前を付けておき、名前とグループの対応表を別途用意する名簿方式の2つがあります。これは第1回の記事のラベルベースアクセス制御とパスベースアクセス制御に相当します。

　さらに、この組織にルールを厳密に適用することを考えます。Hから、Lへの情報の伝播が絶対に起きないようにしなければなりません。

　ユーザーのモラルに任せる、というやり方ではルールが守られるという保証がありません。ルールを確実に守るためには、「絶対に信用できる」何かによって「強制」する必要があります。

　OSによるセキュリティルールの強制

　ここでOSが登場します。コンピュータシステムでは、情報転送はユーザーやユーザーのプログラムが単独で遂行できるものではなく、必ずOSが介在します。そこで、ルール違反の場合には、OSがその情報転送を実行しないことによって、「強制」を実現することができます。

　これが実際に強制的であるためには、それ以外に情報転送の手段が存在しないこと（迂回（うかい）不可）が必要です。またOSが「絶対に信用（trust）できる」ためには、OSがルール違反を起こさないように作られていること、しかもそれが壊されることがないこと（tamper proof）が必要です。

　OSが「ルール違反を決して起こさないように作られている」ことを保証するための最も厳密なアプローチは、それを形式手法（formal method）によって証明することです。

【関連記事】 いまさら聞けない形式手法入門 http://www.atmarkit.co.jp/fembedded/special/fm/fm01.html

　形式手法には、定理証明システムや、モデル検査のアプローチがありますが、いずれにしても、対象が複雑になり規模が大きくなると実行が困難になります。そこで、対象をできる限り小規模にする、あるいは適切に抽象化して、対象を単純化、小規模化する必要があります。

　先ほど、モデルレベルでのセキュリティは「明らか」と書きましたが、OSにはさまざまな機能があり、これらは先ほどのモデルには組み込まれていません。従って、ここではもっと細かいレベルでのモデル化と証明が求められています。

　OSの機能全体をそのまま証明することは不可能です。上述の通り、何らかの方法で対象を小さくしなければなりません。

1/3

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

Security&Trust記事一覧

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