Maxima で綴る数学の旅

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

-セキュリティ- Bell-La PadulaアクセスコントロールモデルとMulticsオペレーティングシステム

 

セキュリティとコンピュータと数学の歴史の話です。

ある種のセキュリティの勉強をしているとアクセスコントロールのポリシーの話が出てきます。中でもBell LaPadulaモデルというモデルが秘匿性のモデルとして登場します。

Bell-LaPadulaモデルでは情報の機密度の階層を考えます。例えば、トップシークレット、シークレット、コンフィデンシャルの3段階の階層を考え、この順に機密度が高いとします。

次に情報を扱う人にはどの機密度まで扱えるかのクリアランスを付与します。「私はシークレットレベルのクリアランスを持っている」。

一方、機密情報にも機密度を付与します。「このファイルはトップシークレットだ」。

このような設定のもとで、あるレベルのクリアランスを持っている人はその機密度以下の情報にしかアクセスできない、ということを強制できれば、機密漏えいが起きないことが数学的に証明できるのです。「私はシークレットのクリアランスを持っているが、このファイルはトップシークレットなので、閲覧できない」。映画の中のスパイが言いそうなセリフです。

 

さて、1970年代に上記のようなアクセスコントロールモデルを米国空軍の依頼を受けて研究したのがBellとLa Padulaという二人の研究者でした。

 

どんな数学的な手法を使ったのか興味があり、調べたところ、以下の論文を見つけることができました。

SECURE COMPUTER SYSTEM: UNIFIED EXPOSITION AND MULTICS INTERPRETATION, ESD-TR-75-306, Bell and La Padula, Mitre Corporation, 1976

数学的な扱いとしては、計算機の構造をステートマシンという代数構造で表し、その間の機密度の関係を定義して、機密漏えいがないことを証明する、というものです。

 

この論文のタイトルにMulticsという単語が見えます。それってあれっ、と気がつく人は多分OSの研究者か私と同年代のコンピュータ屋さん、そして数式処理屋さん(!?)でしょう。そうです。1960年代のMITで作られた当時の最先端のOSです(あまりに複雑になったMulticsの反省から後にUnixが誕生し、今日のLinuxに繋がります)。

 

実は上記の論文は、単にセキュリティの数学的な取り扱いを提案しているだけではありません。アクセスコントロールの数学モデルを定義してから、それをMulticsの設計と対応づけて、Multicsのファイルやプロセスのアクセスコントロールのセキュリティを数学的に証明している論文なのでした。この数学の中で、最初に述べたBell LaPadulaモデルが登場し、クリアランスの関係が重要な基礎として語られています。

このように計算機の動作のセキュリティを数学的に証明する、ということが後のオレンジブックやCommon Criteriaのformally verifiedという考えに繋がるのでしょう。

 

ところで、数式処理にとってMulticsといえば、、、Macsymaが初期の頃から動作したOSです。MIT AI labで開発されたMacLispやMacsymaはMIT LCSのMulticsにも移植されて、広く使われたことは有名です。そしてMacsymaが後のMaximaに繋がっています。