情報処理学会論文誌

コンピューティングシステム

Vol.5 No.2 51–62 (Mar. 2012)

情報セキュリティ向上に向けた OS 研究の動向
橋本 正樹1,a)

安藤 類央1,2

前田 俊行3

田中 英彦1

受付日 2011年7月19日, 採録日 2011年12月9日

概要：近年，情報システムが社会基盤化しているため，そのセキュリティ耐性向上が急務であるが，一方で，セキュリティ・インシデントの発生数は年々増加している現実がある．本稿では，情報セキュリティを担保する最も基礎的なソフトウェアとして OS を位置付け，参照モニタの設計要件と対応付けながら，
特に，仮想化技術，OS プログラムの検証技術，アクセス制御技術に焦点をあてて近年の研究動向を紹介する．また，各技術について，今後の展望と課題を整理する．
キーワード：オペレーティングシステム，仕様記述・仕様検証，ディペンダブルコンピューティング

A Survey of Security Research for Operating Systems
Masaki Hashimoto1,a)Ruo Ando1,2

Toshiyuki Maeda3

Hidehiko Tanaka1

Received: July 19, 2011, Accepted: December 9, 2011

Abstract: In recent years, information systems have become the social infrastructure, so that their security
must be improved urgently. In this paper, we introduce the results of the survey of virtualization, operating
system veriﬁcation and access control technologies in association with the design requirements of the referencemonitor. Additionally, we show the prospects and challenges for each technology.
Keywords: operating system, speciﬁcation/veriﬁcation of speciﬁcation, dependable computing

1. はじめにンシデントの発生数が年々増加する一因となっている．
情報セキュリティを強化するためには，技術・管理・法

近年，情報システムが社会基盤化しているため，そのセ制・倫理の抜本的な裏づけが不可欠であり，そのためのキュリティ強化は重要な課題となっている．今や我々の社

様々な研究・開発や検討が行われている．このうち，特に会生活は，情報システムによる様々な支援により成立して技術に着目すると，暗号技術・侵入検知技術・認証技術・いるため，セキュリティ・インシデント発生時の被害は以

証拠保全技術等，幅広い研究が行われているが，それらは前にも増して深刻化している．同時に，情報システムへのいずれもそれらの機能が働く基盤の健全性を仮定したもの

要請が，その利用用途の拡大に合わせて多様化しているたがほとんどである．基盤はいわゆる OS であるが，OS がめ，その構成は複雑化しており，インターネットに接続す脆弱であると，その上で動作する様々なセキュリティ強化

るノード数の爆発的な増加と合わせて，セキュリティ・イ

機能は砂上の楼閣であるし，OS が健全であった場合にも，

OS からどのようなセキュリティ支援機能を上位層に提供
1

2

3

a)

情報セキュリティ大学院大学情報セキュリティ研究科
Graduate School of Information Security, Institute of Information Security, Yokohama, Kanagawa 221–0835, Japan
情報通信研究機構
National Institute of Information and Communications
Technology, Koganei, Tokyo 184–8795, Japan東京大学大学院情報理工学系研究科
Graduate School of Information Science and Technology,
The University of Tokyo, Bunkyo, Tokyo 113–8656, Japanhashimoto@iisec.ac.jp

c 2012 Information Processing Society of Japan

するべきかは検討が必要な課題である．
そのため，OS そのもののセキュリティ強化と，健全なOS から提供すべきセキュリティ支援機能については，古くから検討が行われ，米国国防総省の Trusted OS をはじめ，近年では，SELinux や Trusted Solaris 等，多くの研究・実装例が存在する．しかしながら，これらは様々な脅
威を抜本的に減らす重要な要素ではあるが，いまだ十分な51

情報処理学会論文誌

コンピューティングシステム

Vol.5 No.2 51–62 (Mar. 2012)

解決策とはいえないため，現在でも各所で活発な研究が行

暗号化，認証技術，デジタルフォレンジック等も OS と情われている．

報セキュリティに関係する技術であるが，本稿では対象外

本稿では，情報セキュリティを担保する最も基礎的なソ
フトウェアとして OS を位置付け，特に，OS の仮想化技とする．

( 1 ) 仮想化技術

術，OS プログラムの検証技術，アクセス制御技術に焦点を仮想化技術は，ハードウェア資源を有効利用するためあてて近年の研究動向を紹介する．はじめに，2 章で，OSに古くから研究されてきた技術であり，近年では，ク

におけるセキュリティ研究について，本稿での分類方針を

ラウド・コンピューティングの基盤技術として広く普参照モニタの設計要件との関連から説明し，この中で，上及している．OS の仮想化技術を特に TCB との関連

記 3 技術の関係を述べる．その後，3 章と 4 章，5 章では，から見たとき，仮想化技術は参照モニタの要件 (i)〜各々について研究動向を紹介し，今後の課題を述べる．最(iii) のすべてに関連する．

後に，6 章で本稿をまとめる．

2. OS におけるセキュリティ研究( 2 ) OS 検証技術
OS 検証技術は，従来からあるプログラム検証技術を
OS に適用することで，OS の完全性を確認するためのTrusted Computing Base（TCB）は ，米 国 国 防 総 省技術である．前述したように，TCB の完全性を保証

が TCSEC（Trusted Computer System Evaluation Cri-

できることは高信頼システムを実現するための要件とteria）[1] の中で定義した概念で，高信頼システムを実現すされており，仮想化技術と OS 検証技術が参照モニタるための基本コンポーネントである．TCB は，参照モニの要件 (iii) に関連する．

タ*1 や形式的に検証可能なセキュリティポリシを含み，特( 3 ) アクセス制御技術に参照モニタについては，(i) 耐タンパ性があること，(ii)

アクセス制御技術は，参照モニタを用いて情報システ

制御対象が迂回不能であること，(iii) 完全性保証のために

ム全体の安全性を担保するための技術で，参照モニタ

十分小さいこと，をその設計要件にあげている．

の要件 (ii) に関連する．アクセス制御技術は，参照モ

OS は，情報システムを構成するソフトウェア・スタッ
クの最下層にあることから，上位層の動作を捕捉可能である点で参照モニタの設計要件 (ii) を自然に満たしている．
そのため，従来より，OS は TCB を構成する主たるソフニタが完全であることを前提としており，他プログラ
ムをどう制御するかが主な課題となる．

3. OS の仮想化技術

トウェアとしての役割を担い，また，OS を参照モニタと

近年，ハードウェア性能の著しい向上により，OS の仮してより強固に構成することで，情報セキュリティを担保想化技術に対する研究・開発が活発になっている．OS のする研究が現在でも行われている．同時に，OS は，応用

仮想化技術は，クラウド・コンピューティングの基盤技術プログラムに実行環境を提供する基本ソフトウェアとしてとしても広く利活用されており，そのセキュリティ強化がの役割もあるため，ハードウェアの進化と情報システムに重要な検討課題となっている．本章では，仮想化技術に関対する新しい要請に応えるべく，参照モニタとしての側面

する近年の研究を，「ハイパーバイザによる仮想マシンの以外からの研究も進められてきた．特に，近年では，組み観測」「主記憶装置の仮想化」「入出力機構の仮想化」「仮込みシステムや携帯端末，クラウドに代表される分散コン

想マシンの完全性検証」の 4 つの側面から整理して紹介すピューティングの普及により，これらからの要請に応えるる．また，今後の課題についても述べる．

新しい OS 技術の研究が各所で行われている．

なお，4 つの分類の論拠であるが，はじめに，情報セキュ

したがって，OS 研究は様々な側面からとらえることがリティ対策を適切に施すためには，情報システム内で起こできるが，本稿では，特に情報セキュリティとの関連から，るある事象について，防御側からは観測可能で，攻撃側か

近年の OS 研究を以下の 3 つに分類して整理する．すなわら観測されないことが重要で，そのための研究が活発に行

ち，本稿では，情報システムに対する脅威の中から OS にわれていることに鑑み，ハイパーバイザによる仮想マシン

関係の深いものとして，OS そのものに対する攻撃と OS 上の観測を第 1 項目とした．次に，ハイパーバイザによる観で動作するプログラムに対する攻撃に焦点をあてる．本分

測対象は，現状では主に主記憶装置と入出力であるため，類では，主に前者への対抗策として OS 検証技術を，主にこれらについても各々整理した．最終項目は，攻撃側が観後者への対抗策としてアクセス制御技術を，両者への対抗測を行うために混入するソフトウェアを締め出すために策として仮想化技術を整理する．データや入出力に対するは，ブートプロセスも含めた実行シーケンスの完全性検証が必要で，このために，ハードウェアによるサポートを前*1

参照モニタは，アクセス主体とアクセス対象間に正当なアクセス
関係を強制する仕組みで，1972 年に発表されたアンダーソンレ
ポート [2] により，セキュアなコンピューティングに必須の要素として提示された．

c 2012 Information Processing Society of Japan提とした研究が各所で行われているため，これらを別途整理したものである．

52

情報処理学会論文誌

コンピューティングシステム

Vol.5 No.2 51–62 (Mar. 2012)

3.1 ハイパーバイザによる仮想マシンの観測技術

ング機構の扱いが重要な課題となる．仮想マシンが利用しハイパーバイザは，仮想マシンとハードウェアの中間にている物理アドレスは，ハイパーバイザによって仮想化さ位置し，リソース管理やスケジューリングを仮想マシンにれた擬似的な物理アドレスであり，真の物理アドレスへの対して行う．ハイパーバイザにより享受できる利点は，第アクセスを調停するためには，通常の場合と比べ，二重の

1 に，運用面で，複数の仮想マシンを一元管理できること，

アドレス変換が必要となる．仮想化技術特有のこの 2 段階

すなわち，稼動状況にあわせて割り当てるリソースを動的以上のページングは，ソフトウェアで行われる場合とハーに伸縮できることがあげられる．第 2 は，仮想マシンのセドウェアで行われる場合がある．

キュリティ強化で，ハイパーバイザを用いることで，複雑

ソフトウェアによる主記憶装置の仮想化には，代表的化し脆弱性を内包するようになった汎用 OS 上のアクセスなものに Xen の Shadow Paging がある．Shadow Paging

制御を強化したり，マルウェアから検出不可能な観測・解

は，主記憶装置のページフォールトを捕捉し，仮想マシン

析器を構築したりできることである．ハイパーバイザの代による主記憶装置へのアクセスを仮想化するもので，仮想表的な実装例としては，Xen [3]，KVM [4]，VMware [5] がマシンが認識している物理アドレスを，実マシンの物理アある．

ドレスに変換するための機構を Shadow Page Table といハイパーバイザを用いて仮想マシンを監視し，観測，防う．これに関連し，Shadow Page Table を修正することで，御，隔離等の処理を行う概念は，VMI（Virtual Machine

rootkit 等の悪意のあるカーネル拡張を検出する研究がさ

Introspection）[6] として提示された．この中で，VMI は，

かんに行われている．

仮想マシンからハイパーバイザ側のコードを修正できない

たとえば，Panorama [13] では，Google Desktop [14] をこと，ハイパーバイザ側から仮想マシンのすべての状態をケーススタディとした汚染検出の手法が提案されている観測できること，仮想マシンから発行されるコードを捕捉し，Ether [15] では，ハードウェアによる仮想化支援機能をできることの 3 点により，不正アクセス検知と防御に有効用いてマルウェアを検出する手法が提案されている．同様

であると指摘されており，本研究を参照した仮想マシンのに，nEther [16] では，RDTSC からのデータ採取により，観測についての論文が多数発表されている．

ゲスト OS から外部で動いているマルウェアを検出する方

VMI による観測方法には，能動的な方法と受動的な方法が提案されている．

法がある．能動的な方法は，仮想マシンの状態を外部から

その一方で，攻撃者の視点から，2006 年には，ハイパー

一定時間ごとに取得し，情報を抽出するもので，代表的なバイザが提供する強力な隔離方式を利用することで，ゲ研究例として，メモリのスナップショットを取得解析する

スト OS からは不可視の rootkit を構築可能な SubVirt [17]Volatality [7] がある．受動的な方法は，仮想マシン内部でや Blue Pill [18] が提案されている．同様に，Ristenpart らリソースアクセス等のイベントが起きた場合に関連する情は，Amazon EC2 を対象として，同じ物理マシン上で動作報を引き出す方法で，代表的な研究例として，Lares [8]，する仮想マシン間のサイドチャネル攻撃が可能であること

Xenprobes [9]，VMScope [10] がある．

を示した [19]．そのほか，Chen らは，防御側のハイパーバ

受動的な方法と能動的な方法の具体的な実装方法としては，内部観測（in-the-box）方式と外部観測（out-of-the-box）

イザによる解析をマルウェアが検出する方法を包括的に調査し，その分類を行っている [20]．

方式の 2 通りあり，これらは観測機構の攻撃者側からの検ハードウェアによる主記憶装置の仮想化には，代表的なも出可能性とセマンティックギャップ [11] の解消可能性*2 ，のに Intel VT-d や AMD-V がある．Intel VT-d や AMD-V

実装に係るコストのトレードオフ [12] との関連性から論じでは，仮想化技術にハードウェアによるメモリ管理機構がられることが多く，現状では，観測対象の仮想マシン内部利用可能で，これにより，ハイパーバイザによるアドレス

から観測機構が検出困難であるという理由から，外部観測

変換の負荷や実装の負荷を低減することができる．これに方式が採用されることが多い．一方で，外部観測方式には，

関連し，Intel VT-d の EPT（Extended Page Table）を利

内部観測方式と比べて，観測可能な情報量が低下するとい用することで，不正なカーネル拡張を検出する研究として，う課題がある．

HUKO [21] がある．HUKO は，Shadow Paging において共有されていたテーブルを物理的に隔離し，ゲスト OS ご

3.2 主記憶装置の仮想化
仮想化技術を実装する際には，主記憶装置，特にページ*2とに所有することで，ゲスト OS のページングによるオー
バヘッドを削減すると同時に，アクセス制御を強化したものである．仮想化技術を用いたアドレス空間の分離に

セマンティックギャップとは，仮想マシン内部のリソースアクセ
スに関連するセマンティック情報を，ハイパーバイザ側で得られる情報から再構築できないことをいう．すなわち，セマンティッ
クギャップの解消とは，ハイパーバイザが仮想マシン上で起こる
リソースアクセスのセマンティックを再構築可能することである．

c 2012 Information Processing Society of Japan

よる保護については，SIM [12] もあるが，SIM が Shadow

Paging を用いているのに対し，HUKO はハードウェア支援によるページングを用いて VMM 遷移や TLB にかかる負荷を低減させている．

53

情報処理学会論文誌

コンピューティングシステム

Vol.5 No.2 51–62 (Mar. 2012)

3.3 入出力機構の仮想化

3.4 仮想マシンの完全性検証

ハイパーバイザから仮想マシンに対してアクセス制御や仮想マシンへの攻撃が増加するにつれ，仮想化マシンの完全性検証等，セキュリティ強化を行う際には，前節で紹構成要素に対して完全性検証を行う研究がさかんに行われ介した主記憶装置の仮想化に加えて，入出力を仮想化する

るようになっている．物理マシンに対する完全性検証を可必要がある．入出力の仮想化は，主記憶装置の仮想化同様能とするデバイスに TPM（Trusted Platform Module）がに，ソフトウェアによるものとハードウェアによるものがあるが，この TPM を仮想化し，物理マシン上の複数の仮ある．

想マシンの構成証明を行う vTPM [26] が提案されている．

ソフトウェアによる入出力機構の仮想化では，デバイス

vTPM では，仮想マシンから TPM への入出力要求を捕ドライバによる入出力要求の捕捉と中継が行われる．Xen

捉するために，先に紹介した Split Device Driver を仮想マの Split Kernel Driver は，その代表例で，仮想マシンとハシンと仮想マシンモニタの双方で実装している．TPM を

イパーバイザの間で共有メモリを設置し，イベントチャン

用いた Trusted Boot には，SRTM（Static Root of Trust

ネルを用いて入出力を仮想化する．また，この応用として，

Measurement）と DRTM（DynamicRoot of Trust Man-

XenAccess [22] では，Split Kernel Driver である blktap ド

agement）の 2 種類がある．STRM は，Sailer らの研究 [27]

ライバを用いて仮想マシンのイベントの修正し，システム

や Bitlocker [28] 等で利用されている．2004 年の Sailer ら

全体の負荷を軽減することができる．また，sHype [23] は，の研究では，ブートローダからカーネル，実行されるアプリ

仮想マシンのスナップショット生成・破棄時や仮想割込み

ケーションにわたって信用の連鎖（Chain of Trust）を確保

発生時に，セキュリティポリシに従った動作を強制するこする手法が提案されている．これにより，OS にロードされとができる．

るコードやデータは，動的に TPM によって完全性が検証

別の実装例としては，BitVisor [24] がある．BitVisor は，されるようになる．Kauer は，2007 年時点での SRTM への準パススルーと呼ばれるアーキテクチャを採用したハイ攻撃手法と AMD の SKINIT を用いた OpenSecure Loader

パーバイザである．BitVisor は，他のハイパーバイザと比（OSLO）の構築方法を提案している [29]．

較して，仮想マシンが生成する I/O 要求のうち，アクセス

また，より進んだ完全性検証を行うものとして，TOCT-

制御や暗号化に関連するもののみを捕捉し，中間処理を行

TOU（time of check to time of use）の一貫性を検証する

うことでセキュリティを強化する．同アーキテクチャを採ことが可能な HIMA [30] が提案されている．HIMA では，用することにより，ハイパーバイザ側は，制御 I/O およ

設計目標として強力な隔離と TOCTTOU 攻撃に対する防びデータ I/O のみを処理すればよく，仮想マシン間の保御にプライオリティを置き，そのための手法として，ゲス

護やスケジューリングが不要になる．BitVisor のコード数

ト OS に対する能動的な観測とゲスト OS のメモリ保護機

は，コア部分で約 20 KLOC，準パススルードライバは通能を提案している．

常のドライバの約 10 分の 1 程度とすることに成功していHyperSentry [31] は，別の研究例で，ハイパーバイザ自体る．また，情報セキュリティの CIA の観点から見ると，他の完全性検証を目的としている．HyperSentry では，out-のハイパーバイザが機密性（Conﬁdentiality）の確保に傾

of-channel と呼ばれる検証対象からは検出不能な専用の観倒しているのに対し，BitVisor は機密性に加えて，完全性測機構と通信路を用いて，ハイパーバイザそのものの完全（Integrity）の確保にも効果的な機能を持っていることが性を検証する．具体的には，ハイパーバイザ内に測定機構特徴である．

を設置し，SMI（System Management Interrupt）handler

ハードウェアによる入出力機構の仮想化では，仮想マシと IPMI（Intelligent Platform Management Interface）をンによるハードウェアへの直接的なアクセスを支援する

経由して，リモートにある検証器と通信する．これによ

IOMMU が提案されている．IOMMU は，DMA（Direct

り，ハイパーバイザからも十分な隔離性を確保しつつ，ハMemory Access）時のアドレス・リマッピング機能をハー

イパーバイザを含むシステム全体の完全性検証を実現してドウェアで実現することで，物理デバイスのアドレスをいる．

仮想マシンが直接扱うことを可能にする．これと関連し，Intel VT-d では，さらに TXT（Trusted Execution Tech-

3.5 今後の課題

nology）[25] によって，DMA を利用した不正なコード転OS の仮想化技術に関連する今後の課題は，前節までに送を防止する機能も実現されている．TXT は，DMA の際紹介した各研究成果を応用することで，仮想化技術に関連に発生するアドレス・リマッピング機能に介入し，保護さする各種セキュリティ機能をよりいっそう強化することでれた領域への DMA を禁止する．また，Intel Vt-i と Intelある．これは，汎用 OS がますます大規模化・複雑化し，脆Vt-d によりゲスト OS のメモリアクセスを含む I/O 空間

弱性を内包する可能性が高まる一方で，今後は組み込みをの完全な分離が可能になることで，機密性を確保することはじめとした各分野で汎用 OS を採用する傾向が高まるこができる．

とが予想されるので，セキュリティ機能を実現する領域のc 2012 Information Processing Society of Japan


54

情報処理学会論文誌

コンピューティングシステム

Vol.5 No.2 51–62 (Mar. 2012)

表 1 OS 検証手法の比較

Table 1 Comparison of OS verification approaches.
検証手法

検証可能な性質

検証のコスト

定理証明支援系（4.1 節）優可ソースコードモデル検査（4.2 節）良良

安全なプログラミング言語（4.3 節）

可優

構築と隔離を，よりハードウェアに近い層であるハイパー
バイザで行う仕組みが必要となることが想定されるためである．

のコストが非常に大きくなるのが欠点である．

Kit [35] は，そのプログラムが直接検証された最初の OSカーネルである．Kit は，約 300 行の機械語（von Neumann

たとえば，アクセス制御に関連するセキュリティ機能の型の仮想的な計算機の機械語）からなる非常に小さなカーネ強化としては，不正なカーネル拡張を検出防止する HUKO

ルであり，カーネル内のタスクの独立性等が Boyer-Mooreのようなシステムが，現在各所で活発に研究が進められて

定理証明器 [36] を用いて検証されている．具体的には，カー

いるし，マルウェア検出に関連するものとしては，マルウェ

ネルが満たすべき抽象仕様および機械語の実装を Boyer-

ア検出・解析用のハイパーバイザに関する検討が進められ

Moore 論理を用いて定義し，抽象仕様がカーネル内の各タており，現在は，その実装方法が課題となっている．また，スクの独立性を保証していることと，実装が抽象仕様を正セマンティックギャップを解消することで，仮想マシン内

しく実現していることを，Boyer-Moore 定理証明器を用いの悪意のある操作をハイパーバイザで検出する研究 [32] もて証明している．

進められている．

4. OS の検証技術
OS は計算機システムの基盤となるソフトウェアであり，より大規模な OS の例としては，seL4 [37] があげられる．

seL4 は約 8700 行の C 言語プログラムと約 600 行のアセン
ブリコードによって実装されたカーネルであり，フォーマ
ルに与えられた仕様をこの実装が正しく実現していること

その信頼性・安全性は，計算機システム全体のセキュリ

が，Isabelle/HOL [33] を用いて保証・検証されている（たティにも大きく影響する．このため，OS プログラムを直だし，seL4 はマイクロカーネルであるため，メモリ管理等

接的に検証しようとする研究が長年行われてきた．本章での複雑な部分はカーネル外にあり，検証の対象とはなっては，このうち 3 つの手法「定理証明支援系を用いた検証手いない）．実際の検証作業は以下のように行われた．まず，法」「ソースコードモデル検査を用いた検証手法」「安全なカーネルが満たすべき性質・振舞いを抽象仕様として定義

プログラミング言語を用いた検証手法」についてそれぞれする（たとえばシステムコールのインタフェースや振舞い紹介する．なお表 1 は 3 つの検証手法を簡単に比較した等）．次に，抽象仕様の抽象的実装として，実行可能仕様

ものである．本章ではまた，OS 検証の今後の課題についを定義する．具体的には，プログラミング言語 Haskell [38]てもふれる．

のサブセットを用いて抽象仕様を実装するプログラムを記述し，そのソースコードから実行可能仕様を自動生成する．

4.1 定理証明支援系を用いた検証手法

そして，こうして得られた実行可能仕様が，抽象仕様と正定理証明支援系とは，何らかの定理とその証明を入力としく対応していることを証明する．次に，実行可能仕様をして受け取り，その証明の正しさを判定するプログラムで

C 言語のサブセットを用いて実装する．この C 言語のサブある [33], [34]．まず OS プログラムの安全性・信頼性を定セットの意味論は，Isabelle/HOL 上でフォーマルに定義

理として表現し，次にその証明を作成して，定理証明支援

されているため，C 言語による実装を Isabelle/HOL でほ系を用いてその証明の正しさを検証することで，OS の安ぼ直接扱うことができる．最後に，この C 言語による実装

全性・信頼性を保証・検証する．具体的には，たとえば，が，実行可能仕様と正しく対応していることを証明する．

OS プログラムの振舞いを抽象状態機械上の状態遷移とし

なお，これらの検証作業には，全体として約 22 人年を要て表現し，その抽象状態機械が何らかの性質を満たしていしたとのことである．

ること（たとえば状態機械が不正なメモリ操作を行わない
ことや状態機械が予期せず停止したり，無限ループに陥ったりしないこと）を証明することで，OS の性質を保証・検証することができる．

4.2 ソースコードモデル検査を用いた検証手法
ソースコードモデル検査 [39], [40] とは，モデル検査技
術 [41] を直接プログラムのソースコードに適用する手法で定理証明支援系を用いた検証手法の利点は，その支援系ある．より具体的には，入力として与えられたソースコー

で扱うことができる任意の性質の検証が可能な点である．

ドからモデルを抽出し，プログラムがとりうる状態を網羅

一方，定理の証明を人手で作成する必要があるため，検証的に検査することで，プログラムの性質を保証・検証する．

c 2012 Information Processing Society of Japan

55

情報処理学会論文誌

コンピューティングシステム

Vol.5 No.2 51–62 (Mar. 2012)

ソースコードモデル検査を用いて OS を検証することので分類し，プログラムが実行時にその分類（型）に従って

利点は，定理証明支援系を用いた手法とは異なり，人手を振る舞うかどうかを検査する．このため，厳密な型検査に基本的に必要としない点である．一方，欠点としては，一通ったプログラムは，型エラーを生じるような不正なメモ

般にモデル検査には多くの計算資源（CPU 時間・メモリ

リ操作やコード実行を行わないことが保証される．

等）が必要となることが多い点があげられる．

安全なプログラミング言語を用いて OS プログラムを記

SDV（Static Driver Veriﬁer）[42] は，Windows のデバ

述することの利点は，OS プログラムの検証が，プログラ

イスドライバを検証するためのフレームワークである．

ミング言語の型検査等により自動的に行われる点である．

より具体的には，デバイスドライバが，SLIC という仕様

また，ソースコードモデル検査と比べて，検証に要する計記述言語で記述された仕様（主にカーネル API の利用方

算資源（CPU 時間・メモリ等）が少ないという利点もあ法）を守っているかどうかを，ソースコードモデル検査器

る．一方，検証できる性質が基礎的なものに限られるとい

SLAM [43] を用いて検証する．OS カーネル本体の検証はう欠点がある．また一般の OS 開発者にとって，安全なプ

対象ではない．なお，SDV は Microsoft のデバイスドライ

ログラミング言語を用いて OS を記述することは敷居が高バ開発キット（Windows Driver Kit）に含まれており，すいという問題もある．

でに実用に供せるレベルにある．

SPIN [47] は，安全に機能を拡張することができる，マイ

また，直接ソースコードモデル検査が適用されている

クロカーネル方式の OS カーネルである．伝統的なマイク

わけではないが，類似した方法で OS カーネルを検証する

ロカーネルでは，カーネル拡張をカーネル本体と異なる特試みとして，Verve における Nucleus と呼ばれる部分の検権レベルで実行することでカーネルの安全性を保証しよう

証 [44] があげられる．Verve は型安全性が保証・検証されとするが，カーネル拡張とカーネル間の通信，またカーネ

た OS であり，その一部である Nucleus は，主にメモリ管

ル拡張間の通信にオーバヘッドが生じるという問題があっ

理（ガーベジコレクション）やスレッド管理（スタック管た．これに対し，SPIN のカーネル拡張は，型安全なプロ理），ハードウェア管理（割込み処理・デバイスドライバ

グラミング言語 Modula-3 [48] を用いて記述できるため，等）を担っている．この Nucleus の検証は次のようにしてカーネル本体と同じ特権レベルで実行しても安全性が保証行われた．まず Nucleus のアセンブリコード実装，およびされ，また通信によるオーバヘッドを低減できる．具体的

Nucleus が満たすべき仕様を，Boogie [45] というプログラには，仮想メモリ領域管理やネットワーク通信処理等，低ム検証器上で表現し，Boogie へ入力として渡す．すると

レイテンシが求められる処理が，Modula-3 を用いたカー

Boogie は，Nucleus が仕様どおりに振る舞うかどうかを表ネル拡張として実装されている．なお SPIN では，カーネ

す検証条件（veriﬁcation condition）を生成し，この条件がル本体は検証の対象ではない．また Modula-3 のコンパイ満たされるかどうかを，Z3 [46] と呼ばれる SMT solver をラにバグがあると，カーネルの安全性が破れる可能性があ

用いて検証する．このように，Nucleus の検証は基本的にる．つまり，Modula-3 のコンパイラをシステムの Trusted

自動である．なお Nucleus は，約 4,500 行の Boogie コード

Computing Base（TCB）に含める必要がある．

からなる（これはアセンブリコードの行数では約 1,400 行

Singularity [49] は，型安全なプログラミング言語 C# [50]，に対応する）が，このうち約 7%は，完全に自動で検証を行

C# を拡張したプログラミング言語 Sing#，およびアセン

うためのヒントとして人手で与えられた注釈とのことであ

ブリ言語で記述された OS である．厳密にいえば，Sing#る．また，アセンブリコード実装および仕様の Boogie 上は，C# を拡張したプログラミング言語 Spec# をさらにでの記述には，約 9 人月を要し，Boogie による Nucleus 自

拡張したものである．Spec# は，オブジェクトのメソッド

動検証には，CPU が Intel Core2 2.4 GHz・メモリが 4 GBの事前条件・事後条件等を明示的に記述できるように C#のマシン上で，272 秒を要したとのことである．

を拡張したものである．Sing# は，Spec# をさらに拡張
し，プロセス間の通信手段としてチャネルを導入したもの

4.3 安全なプログラミング言語を用いた検証手法である．Singularity では，OS の各コンポーネントはそれ

本稿では，「安全なプログラミング言語」とは，厳密な型

ぞれプロセスとして実装されており，コンポーネント間検査等により，実行時にプログラムが不正なメモリ操作・の通信は上述のチャネルを介して行われる．具体的には，コード実行等を行わないことを保証・検証できるようなプ

Singularity は約 280,000 行の C# プログラムと約 90,000

ログラミング言語のことを指す．このような安全なプログ

行の Sing#（およびアーキテクチャ依存のアセンブリプロ

ラミング言語を用いて OS プログラムを記述することによグラム）からなり，C# および Sing# で記述された部分

り，OS が不正なメモリ操作を行わないこと等を，型検査等の型安全性・コンポーネント間の独立性等が保証される．

により保証・検証することができる．厳密な型検査は，プ

ただし，メモリ管理やスレッド管理等の部分は直接の検証

ログラムを解析することで，プログラム中の変数や式を型の対象外である．なお，C#・Sing# のプログラムは型安（整数やメモリ参照等，データやコードの種類を表す分類）

全なアセンブリプログラム（型付きアセンブリ言語 [51]）c 2012 Information Processing Society of Japan

56

情報処理学会論文誌

コンピューティングシステム

Vol.5 No.2 51–62 (Mar. 2012)の一種に変換され，アセンブリプログラムのレベルで型が標準化されている．以降の節では，OS によるアクセス

安全性を検査することができるため，（SPIN とは異なり）制御機能の主要な構成要素として，セキュリティポリシモ

C#・Sing# のコンパイラをシステムの TCB に含める必

デル，セキュリティポリシ記述言語，セキュリティポリシ

要はない．

検証技術，アクセス制御メカニズムについて，それぞれ近TOS [52] は，OS カーネルの記述向けに拡張された型付

年の研究動向を紹介し，今後の課題について述べる．

きアセンブリ言語 TALK [53], [54] を用いて記述された OSカーネルである．TALK は，メモリを表すための可変長

5.1 セキュリティポリシモデル

配列やアドレス計算を扱うための整数制約，メモリの安全

情報システムは，その用途に応じて様々な水準の機密な strong update（メモリ領域の型を変更するようなメモ性・完全性・可用性を必要とするため，この特性を反映しリ操作）等を型システムで扱えるようにすることで，従来た様々なセキュリティポリシモデルが従来から研究されの型付きアセンブリ言語では難しかった OS カーネルの記てきた．主要な類型は，機密性保護型，完全性保護型に加述とその型検査を可能としている．TOS は約 3,000 行のえ，これらの混成型で，各類型の代表的なセキュリティ

TALK プログラムからなる，機能が限定された OS カーネ

ポリシモデルは，機密性保護型として Bell-LaPadula モデルであるが，他の安全なプログラミング言語を用いた OS

ル [59]，完全性保護型として Biba Integrity モデル [60] と検証の研究では直接の対象にされてこなかった，メモリ管

Clark-Wilson モデル [61]，混成型として Chinese Wall モ

理やスレッド管理等の部分も含めて TALK で記述されてデル [62] と RBAC モデル [63], [64] 等がある．以下に，近おり，そのメモリ安全性が TALK の型検査によって保証・年の代表的なセキュリティポリシモデルの研究例を示す．

検証可能である点が特徴である．

RBAC モデル [63], [64] は，Role（役割）を中核としたセキュリティポリシモデルで，情報システム内のアクセス

4.4 今後の課題

制御を実世界の組織構成と各人の責務に合わせて実現しや前節までに紹介したとおり，OS プログラムの直接検証

すいため，直感的に理解しやすく，正しく運用すれば最小は研究レベルではすでに実証されつつあり，今後の課題は，特権の原則に沿ったアクセス制御を実現可能であるため，

より大規模かつ実際的な OS へ検証技術を適用することにSELinux や Solaris をはじめとした様々な OS で採用が進んある．これを実現するためには，前節で紹介したいくつかでいる．RBAC モデルの近年の研究成果としては，RBACの検証技術を組み合わせて利用することが現実的であるとモデルの形式的な定義と基礎モデルの拡張 [65] や，RBAC考えられる．実際，前述の Verve [44] では，Nucleus 以外

モデルの標準化・ANSI 標準への採用 [66] がある．そのほの部分については，別途 C#（すなわち，安全なプログラ

かにも，RBAC モデルには，誰がどのように RBAC シス

ミング言語）で記述されており，全体として OS カーネル

テム内の様々な関係を設定するべきか，という管理上の課の型安全性が保証されるようになっている．

題があるが，これに対しては，ARBAC の諸研究 [67], [68]また，より学術的・技術的な課題としては，近年広く普や，管理上の課題に焦点をあてた RBAC モデルの分析が及しているマルチコア CPU 等，複数のプログラムが同時ある [69]．また，実際の OS に実装された RBAC モデルにに実行される環境における OS プログラムの安全性をどのついて，そのセキュリティ特性を形式的に検証する方法もように検証するか [54] 等があげられる．従来の OS 検証

提案されている [70]．

の研究は，基本的に単一 CPU の計算機環境を仮定しておTBAC（Task-Based Authorization Controls）モデル [71]り，特に，複数のプログラムが共有のメモリを同時に操は，Authorization Step（AS）として複数の認可を認可手作する場合に生じる競合状態やメモリ一貫性モデルの問順としてグループ化し，アクセス主体・アクセス対象・操

題 [55], [56], [57] への対処が必要となる．

作内容に加えて，AS 名と AS 内の工程名を指定して認可

5. アクセス制御技術

判定を決定するセキュリティポリシモデルである．TBAC
では，AS ごとにサブジェクトに付与するアクセス権限を，アクセス制御技術は，情報セキュリティを支える最も基その前後関係を考慮しながら逐次有効化・無効化するため，礎的な要素技術の 1 つであり，機密性・完全性・可用性のい

たとえば，トランザクションの処理状況に応じて細かなア

ずれの保護にも関係する．このため，2 章で述べたとおり，

クセス権限を指定できる．これにより，TBAC は，特定のアクセス制御機能を TCB としての OS から上位層に提供認可手順を抽象的に構造化し，サブルーチンのように繰りし，情報セキュリティを担保するための研究が半世紀近く返し利用可能とすることで，ポリシ全体の見通しを向上さ

前から継続的に行われており，初期の研究成果は，TCSECせることができる．

（Trusted Computer System Evaluation Criteria）[1] に見ることができる．また，近年では，ISO/IEC10181-3 [58] として，高度に抽象化されたアクセス制御システムのモデル

c 2012 Information Processing Society of Japan

5.2 セキュリティポリシ記述言語
セキュリティポリシ記述言語は，セキュリティポリシを57

情報処理学会論文誌

コンピューティングシステム

Vol.5 No.2 51–62 (Mar. 2012)

表現するためのもので，アクセス制御の仕様を記述する言報システムの区画化，最弱点等を検証することができる．

語として見ることができる．近年，セキュリティポリシ記

RBAC-PAT は，複数の管理者によってアクセス権限の変

述言語の研究では，述語論理をはじめとする数理論理学の更が随時行われるような ARBAC モデルでは，ポリシの分知見を応用した研究が行われており，主要な課題は，アク析が困難となるという課題に対処している．具体的には，

セス権限の委譲・制限・否定等に対する表現力，人間にとっあるユーザに対する特定 Role の到達性・可用性や，Roleての文法的な明快さ・読みやすさ，簡潔で明快な意味論，間の内包性・最小セット等の関係，不要 Role の発見，オブ

効率的な認可判定手順，拡張性等がある．以下に，近年のジェクト間の情報流を検証することができる．

代表的なセキュリティポリシ記述言語の研究例を示す．

PALMS [76] は，MLS ポリシの形式的な仕様を定義する

SecPAL [72] は，比較的大規模なシステムで，セキュリ

ことで，分析対象の MLS ポリシに存在する全情報流を検ティポリシを管理領域ごとにモジュール化して構成するこ証することができる．また，2 つの MLS ポリシ間の整合とを前提とし，分散管理された領域間でアクセス権限の委性を自動的に検証することができる．PALMS は，Prolog

譲を柔軟に記述するためのセキュリティポリシ記述言語でベースのツールとして実装されており，与えられた MLS

ある．SecPAL は，制約論理言語による高レベルなセキュ

ポリシが，∗ プロパティやシンプルセキュリティコンディ

リティポリシ記述言語で，認可判定要求は節の集合に対すション等を満たすこと，アプリケーションの MLS ポリシ

る問合せが成功したときに承認される．SecPAL の文法はが，そのホスト OS の MLS ポリシと整合がとれていること

自然言語に近く，意味づけは 3 つの推論ルールから構成さ等を検証することができる．PALMS は，MLS ポリシのみれており，否定的なクエリや再帰的な述語，回数を指定可を対象としているが，現実の情報システムでは，複数のセ能な権限委譲やその他様々な制限をサポートすることで，キュリティポリシモデルが連携する場合が多いため，MLS

多くのセキュリティポリシモデルを汎用的に表現可能であポリシと他のセキュリティポリシモデルが連携する際にもる．SecPAL は，クラウド OS である Windows Azure のセ検証可能とするように研究が進められている．

キュリティポリシ記述言語として実装するために，現在も研究が進められている．

5.4 アクセス制御メカニズム

Lithium [73] は，論理的な否定を形式的に正しく推論でき

アクセス制御メカニズムは，セキュリティポリシ記述言るセキュリティポリシ記述言語である．Lithium は，一階

語によって記述された個々のアクセス制御規則を情報シ

述語論理を基礎にした高レベル言語で，再帰的な表現を制

ステムに強制するための仕組みである．具体的な実装手

限することで否定を含んだ推論を実現している．Lithium

法としては，ACL 方式と Capability 方式が従来から存在は，たとえば，複数のポリシをマージしてそのアクセス制

し [77]，長年 ACL 方式が広く採用されてきたが，最小特権

御仕様を分析する場合に，あるアクセスが未認可であるこの原則によるアクセス制御を実現しやすいという利点があとを形式的に確認できる点で有用であるが，一方で，多くるため，Capability 方式の研究も継続されている．また，のセキュリティポリシモデルで必要となる，アクセス権限

セキュリティポリシとの連携に重点を置いた強制アクセスの委譲を簡潔に表現できないという課題がある．Lithium

制御機構を既存の OS に追加するための研究も行われていには，その文法や一階述語論理の知識がなくても利用可能

る．以下に，近年の代表的なアクセス制御メカニズムの研とするために，通常の英文法によってポリシ記述ができる

究例を示す．

ようなフロントエンドも開発されている [74]．

seL4 [37] は，L4 マイクロカーネルをベースにセキュリ
ティ拡張を行った研究用 OS で，take-grant モデル [78] を

5.3 セキュリティポリシ検証

Capability 方式と組み合わせて実装し，各種カーネルオブ

セキュリティポリシ検証は，セキュリティポリシが特定ジェクトに対するアクセス制御を実現している．ここで，のアクセス制御に関する仕様を満たすことを検証するため

L4 のカーネルオブジェクトとは，スレッド，アドレス空の技術である．近年の情報システムは大規模・複雑化して間，プロセス間通信，未使用の物理メモリを示す untyped-いるため，前節で紹介したような言語によるセキュリティ

memory で，これらに対するアクセス権限は Capability を

ポリシの記述量が特に増大する傾向にあり，実現されるア

通して授受する仕組みになっている．別の Capability 方式

クセス制御仕様を人間が明快に把握できないことが多い．

による研究例としては，Capsicum [79] がある．Capsicum

この課題に対処するために，記述されたセキュリティポリ

は，UNIX の標準 API を拡張する研究用 OS で，Capability

シを容易に解析するための検証手法が求められており，活を用いることでプロセスやアプリケーションのサンドボッ発な研究が進められている．以下に近年の代表的なセキュクス化を容易かつ細粒度に実現している．Capsicum は，

リティポリシ検証の研究例を示す．

OS からアプリケーション層の区画化を一元的に制御するRBAC-PAT [75] は，ARBAC モデルを対象として，あのではなく，個々のアプリケーションが自身の区画化を容る Role を始点にしたときの情報流の到達性や可用性，情易に実現できるよう OS として支援するという設計思想で

c 2012 Information Processing Society of Japan


58

情報処理学会論文誌

コンピューティングシステム

Vol.5 No.2 51–62 (Mar. 2012)

研究が進められている．

した．

Flask セキュリティアーキテクチャ（FLSA）[80] は，セ

今後の情報社会の健全な発達には，強固な OS によるセキュリティポリシによる決定を強制的に執行するオブジェ

キュリティ支援が必要不可欠であるが，本稿で紹介したよクトマネージャと，与えられたセキュリティポリシに従っうに，これを実現するための各要素技術はいまだ課題を多てアクセス可否の決定を下すセキュリティサーバから構

くかかえている．これはひとえに，OS に対する要請が長成される．各々は，あらかじめ定められたプロトコルに年にわたって大きく変化しなかったこともあり，特に実利従ってデータ通信を行い，FLSA 全体として参照モニタの用される OS では，その基本原理が半世紀近くほとんど変役割を果たす．FLSA は，様々なセキュリティポリシモデ

わってこなかったことに由来すると考えられる．しかしな

ルを柔軟に実現できることが大きな特徴である．SELinux

がら，今後を見ると，新しいコンピューティング環境の急は FLSA の Linux に対する実装で，そのほか，SEBSD も速な普及に合わせて，OS に対する要請もこれまでになくFLSA の実装例である．同様の強制アクセス制御機構とし大きく変化することが想定され，特に情報セキュリティのては，TrustedBSD MAC Framework [81] が提案されてお重要性と，OS が自然に備える TCB や参照モニタへの適合

り，FreeBSD や Darwin に実装されている．

性に鑑みたときに，本稿で取り上げた諸技術の残存課題が解決され，実社会であたりまえのように利用されるよう普5.5 今後の課題
アクセス制御技術は，比較的古くから研究が進められてきたもので，最も基礎的な理論はすでに確立されている．
同時に，情報セキュリティへの要請の変遷に合わせて，継続的にその拡張や応用が求められており，近年では，情報及することが期待される．本稿が近い将来この仕事にあたる方々の足がかりとなり，わが国の情報セキュリティ研究の発展を支える一助となれば幸いである．
謝辞

貴重なご助言をいただいた編集委員と匿名査読者の方々に感謝いたします．

システムの社会基盤化に合わせて，前節までに紹介したような諸研究が進行中である．
今後の課題は，仮想化技術を基礎としたクラウド環境

参考文献
[1]

や，スマートフォンをはじめとした組み込み環境等，要請されるアクセス制御仕様や，これを実現するための前提が異なる環境にこれらの成果を応用することである．具体的[2]には，分散システム向けのセキュリティポリシモデルやその記述言語，それを強制する分散アクセス制御メカニズム[3]が求められており，これに向けた研究は，すでに各所で検討が進められている．たとえば，FLSA の適用範囲を，ス
タンドアローン・システムの OS 層で捕捉可能な対象から，アプリケーション層や他システムの対象に拡張するための[4]

アクセス制御メカニズム等が研究されている [82], [83]．

6. まとめ
本稿では，OS に関する近年の様々な研究を情報セキュ

[5]

[6]

リティとの関連から整理し，各技術分野の課題を示した．
諸研究の整理にあたっては，参照モニタの設計要件との対応から，特に仮想化技術・OS 検証技術・アクセス制御技術に着目して分類し，各技術分野をさらに細分化したうえ[7]で，項目ごとに概要と研究例，課題を述べた．具体的には，仮想化技術については，ハイパーバイザによる仮想マシンの観測・主記憶装置の仮想化・入出力機構の仮想化・仮想[8]マシンの完全性検証に，OS 検証技術については，定理証明支援系を用いた検証手法・ソースコードモデル検査を用いた検証手法・安全なプログラミング言語を用いた検証手法に，アクセス制御技術については，セキュリティポリシ
モデル・セキュリティポリシ記述言語・セキュリティポリ
シ検証・アクセス制御メカニズムに，各々細分化して説明c 2012 Information Processing Society of Japan[9]

US Department of Defense: Trusted Computer Systems
Evaluation Criteria, Technical Report CSC-STD-00183, DoD Computer Security Center, Fort Meade, MD(1983).
Anderson, J.P.: Computer Security Technology Planning
Study, Technical Report Vols. I and II, USAF Electronic
Systems Div., Bedford, Mass (1972).
Barham, P., Dragovic, B., Fraser, K., Hand, S., Harris,T., Ho, A., Neugebauer, R., Pratt, I. and Warﬁeld,
A.: Xen and the art of virtualization, Proc. 19th ACM
Symposium on Operating Systems Principles, SOSP’03,
pp.164–177, New York, NY, USA, ACM (2003).
Kivity, A., Kamay, Y., Laor, D., Lublin, U. and Liguori,
A.: kvm: The Linux virtual machine monitor, Proc.
Linux Symposium, Vol.1, pp.225–230 (2007).
Waldspurger, C.A.: Memory resource management in
VMware ESX server, SIGOPS Oper. Syst. Rev., Vol.36,
pp.181–194 (2002).
Garﬁnkel, T. and Rosenblum, M.: A virtual machine
introspection based architecture for intrusion detection,
Proc. 10th Annual Network and Distributed System Security Symposium (NDSS ), Vol.1, ISOC, pp.253–285(2003).
Volatile Systems: The Volatility Framework: Volatilememory artifact extraction utility framework, (2006),
available from https://www.volatilesystems.com/
default/volatility.
Payne, B.D., Carbone, M., Sharif, M. and Lee, W.:
Lares: An Architecture for Secure Active Monitoring Using Virtualization, IEEE Symposium on Security andPrivacy, Vol.0, pp.233–247 (2008).
Quynh, N.A. and Suzaki, K.: Xenprobes, a lightweightuser-space probing framework for Xen virtual machine,2007 USENIX Annual Technical Conference on Proc.
USENIX Annual Technical Conference, pp.2:1–2:14,
Berkeley, CA, USA, USENIX Association (2007).

59

情報処理学会論文誌

[10]

[11]

[12]

[13]

[14]
[15]

[16]

[17]

[18]
[19]

[20]

[21]

[22]

[23]

[24]

コンピューティングシステム

Vol.5 No.2 51–62 (Mar. 2012)

Breslau, L., Chase, C., Duﬃeld, N., Fenner, B., Mao, Y.
and Sen, S.: VMScope: A virtual multicast VPN performance monitor, Proc. 2006 SIGCOMM Workshop on
Internet Network Management, INM’06, pp.59–64, New
York, NY, USA, ACM (2006).
Chen, P.M. and Noble, B.D.: When Virtual Is Better
Than Real, Proc. 8th Workshop on Hot Topics in Operating Systems, pp.133–138, Washington, DC, USA,IEEE Computer Society (2001).
Sharif, M.I., Lee, W., Cui, W. and Lanzi, A.: Secure
in-VM monitoring using hardware virtualization, Proc.
16th ACM Conference on Computer and Communications Security, CCS’09, pp.477–487, New York, NY,
USA, ACM (2009).
Yin, H., Song, D., Egele, M., Kruegel, C. and Kirda,
E.: Panorama: Capturing system-wide information ﬂow
for malware detection and analysis, Proc. 14th ACM
Conference on Computer and Communications Security, CCS’07, pp.116–127, New York, NY, USA, ACM(2007).
inc., G.: Inside Google Desktop, available fromhttp://googledesktop.blogspot.com.
Dinaburg, A., Royal, P., Sharif, M. and Lee, W.: Ether:
Malware analysis via hardware virtualization extensions,
Proc. 15th ACM Conference on Computer and Communications Security, CCS’08, pp.51–62, New York, NY,
USA, ACM (2008).
Pék, G., Bencsáth, B. and Buttyán, L.: nEther: Inguest detection of out-of-the-guest malware analyzers,
Proc. 4th European Workshop on System Security, EUROSEC’11, pp.3:1–3:6, New York, NY, USA, ACM(2011).
King, S.T., Chen, P.M., Wang, Y.-M., Verbowski, C.,
Wang, H.J. and Lorch, J.R.: SubVirt: Implementing
malware with virtual machines, IEEE Symposium on
Security and Privacy, Vol.0, pp.314–327 (2006).
Rutkowska, J.: Subverting VistaTM Kernel For Fun And
Proﬁt, Black Hat Briefings (2006).
Ristenpart, T., Tromer, E., Shacham, H. and Savage,
S.: Hey, you, get oﬀ of my cloud: Exploring information
leakage in third-party compute clouds, Proc. 16th ACM
Conference on Computer and Communications Security, CCS’09, pp.199–212, New York, NY, USA, ACM(2009).
Chen, X., Andersen, J., Mao, Z., Bailey, M. and Nazario,
J.: Towards an understanding of anti-virtualization andanti-debugging behavior in modern malware, IEEE International Conference on Dependable Systems andNetworks With FTCS and DCC, 2008, DSN 2008,
pp.177–186, IEEE (2008).
Xiong, X., Tian, D. and Liu, P.: Practical protection ofkernel integrity for commodity OS from untrusted extensions, Proc. 18th Annual Network and Distributed
System Security Symposium (NDSS ), ISOC (2011).
Payne, B., Carbone, M. and Lee, W.: Secure and ﬂexible
monitoring of virtual machines, Annual Computer Security Applications Conference 2007, ACSAC’07, pp.385–
397, IEEE Computer Society (2007).
Sailer, R., Valdez, E., Jaeger, T., Perez, R., Van Doorn,
L., Griﬃn, J., Berger, S., Doorn, L., Linwood, J.
and Berger, G.: sHype: Secure Hypervisor Approachto Trusted Virtualized Systems, IBM Research Report
RC23511, IBM Research Division (2005).
Shinagawa, T., Eiraku, H., Tanimoto, K., Omote, K.,
Hasegawa, S., Horie, T., Hirano, M., Kourai, K., Oyama,c 2012 Information Processing Society of Japan


[25]

[26]

[27]

[28]

[29]

[30]

[31]

[32]

[33]

[34]

[35]

[36]

[37]

[38]

[39]

[40]

Y., Kawai, E., Kono, K., Chiba, S., Shinjo, Y. and Kato,K.: BitVisor: A thin hypervisor for enforcing i/o device
security, Proc. 2009 ACM SIGPLAN/SIGOPS International Conference on Virtual Execution Environments,
VEE’09, pp.121–130, New York, NY, USA, ACM (2009).
Corporation, I.: Trusted Execution Technology (Intel
TXT), available from http://download.intel.com/
technology/security/downloads/315168.pdf.
Berger, S., Cáceres, R., Goldman, K.A., Perez, R., Sailer,
R. and van Doorn, L.: vTPM: Virtualizing the trusted
platform module, Proc. 15th Conference on USENIX
Security Symposium - Volume 15, SSYM’06, pp.305–
320, Berkeley, CA, USA, USENIX Association (2006).
Sailer, R., Zhang, X., Jaeger, T. and van Doorn, L.:
Design and implementation of a TCG-based integrity
measurement architecture, Proc. 13th Conference on
USENIX Security Symposium - Volume 13, SSYM’04,
p.16, Berkeley, CA, USA, USENIX Association (2004).
Corporation, M.: BitLocker Drive Encryption, available
from http://windows.microsoft.com/en-US/windows7/
products/features/bitlocker.
Kauer, B.: OSLO: Improving the security of trusted
computing, Proc. 16th USENIX Security Symposium Volume 16, SSYM’07, pp.16:1–16:9, Berkeley, CA, USA,USENIX Association (2007).
Azab, A., Ning, P., Sezer, E. and Zhang, X.: HIMA: A
hypervisor-based integrity measurement agent, Annual
Computer Security Applications Conference 2009, ACSAC’09, pp.461–470, IEEE (2009).
Azab, A.M., Ning, P., Wang, Z., Jiang, X., Zhang, X.
and Skalsky, N.C.: HyperSentry: Enabling stealthy incontext measurement of hypervisor integrity, Proc. 17th
ACM Conference on Computer and Communications
Security, CCS’10, pp.38–49, New York, NY, USA, ACM(2010).
Litty, L., Lagar-Cavilla, H.A. and Lie, D.: Hypervisor support for identifying covertly executing binaries,
Proc. 17th Conference on USENIX Security Symposium - Volume 17, SSYM’08, pp.243–258, Berkeley, CA,
USA, USENIX Association (2008).
Nipkow, T., Paulson, L.C. and Wenzel, M.: Isabelle/
HOL – A Proof Assistant for Higher-Order Logic,
LNCS, Vol.2283, Springer (2002).
Bertot, Y. and Castéran, P.: Interactive Theorem Proving and Program Development, Coq’Art: the Calculusof Inductive Constructions, Springer-Verlag (2004).
Bevier, W.R.: Kit: A Study in Operating System
Veriﬁcation, IEEE Trans. Softw. Eng., Vol.15, No.11,
pp.1382–1396 (1989).
Boyer, R.S. and Moore, J.S.: A computational logic
handbook, Academic Press Professional, Inc., San Diego,
CA, USA (1988).
Klein, G., Elphinstone, K., Heiser, G., Andronick, J.,
Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K.,
Kolanski, R., Norrish, M., Sewell, T., Tuch, H. and
Winwood, S.: seL4: Formal veriﬁcation of an OS kernel, Proc. SOSP’09, pp.207–220 (2009).
Jones, S.P. (Ed.): Haskell 98 Language and Libraries –The Revised Report, Cambridge University Press, Cambridge, England (2003).
Ball, T., Majumdar, R., Millstein, T. and Rajamani,
S.K.: Automatic predicate abstraction of C programs,
Proc. PLDI’01, pp.203–213 (2001).
Henzinger, T.A., Jhala, R., Majumdar, R. and Sutre, G.:
Lazy abstraction, Proc. POPL’02, pp.58–70 (2002).

60

情報処理学会論文誌

[41]
[42]

[43]

[44]

[45]

[46]
[47]

[48]
[49]

[50]

[51]

[52]

[53]

[54]

[55]

[56]

[57]

[58]

[59]

[60]

コンピューティングシステム

Vol.5 No.2 51–62 (Mar. 2012)

Clarke, Jr., E.M., Grumberg, O. and Peled, D.A.: Modelchecking, MIT Press, Cambridge, MA, USA (1999).
Ball, T., Bounimova, E., Kumar, R. and Levin, V.:
SLAM2: Static driver veriﬁcation with under 4% false
alarms, Proc. FMCAD’10, pp.35–42 (2010).
Ball, T., Cook, B., Levin, V. and Rajamani, S.K.: SLAM
and Static Driver Veriﬁer: Technology Transfer of Formal Methods inside Microsoft, Proc. IFM’04, pp.1–20(2004).
Yang, J. and Hawblitzel, C.: Safe to the Last Instruction: Automated Veriﬁcation of a Type-Safe Operating
System, Proc. PLDI’10 (2010).
Barnett, M., Chang, B.-Y.E., DeLine, R., 0002, B.J. andLeino, K.R.M.: Boogie: A Modular Reusable Veriﬁer
for Object-Oriented Programs, Proc. FMCO’05, pp.364–
387 (2005).
De Moura, L. and Bjørner, N.: Z3: An eﬃcient SMT
solver, Proc. TACAS’08, pp.337–340 (2008).
Bershad, B.N., Savage, S., Pardyak, P., Sirer, E.G.,
Fiuczynski, M., Becker, D., Eggers, S. and Chambers,
C.: Extensibility, Safety and Performance in the SPIN
Operating System, Proc. SOSP’95, pp.267–284 (1995).
Nelson, G. (Ed.): System Programming in Modula-3,
Prentice Hall (1991).
Hunt, G.C., Larus, J.R., Abadi, M., Aiken, M., Barham,
P., Fähndrich, M., Hawblitzel, C., Hodson, O., Levi,
S., Murphy, N., Steensgaard, B., Tarditi, D. and Zill,
T.W.B.: An Overview of the Singularity Project, Technical Report MSR-TR-2005-135, Microsoft Corporation(2005).
Hejlsberg, A., Torgersen, M., Wiltamuth, S. and Golde,P.: The C# Programming Language, 3rd edition,
Addison-Wesley Professional (2008).
Morrisett, G., Walker, D., Crary, K. and Glew, N.: From
System F to Typed Assembly Language, ACM Trans.
Prog. Lang. Syst., Vol.21, No.3, pp.528–569 (1999).
Maeda, T. and Yonezawa, A.: Writing an OS Kernel
in a Strictly and Statically Typed Language, Formal toPractical Security, LNCS 5458, pp.181–197 (2009).
Maeda, T. and Yonezawa, A.: Writing practical memory
management code with a strictly typed assembly language, Proc. SPACE’06 (2006).
Maeda, T. and Yonezawa, A.: Typed assembly language
for implementing OS kernels in SMP/multi-core environments with interrupts, Proc. SSV’10 (2010).
Adve, S.V. and Gharachorloo, K.: Shared Memory
Consistency Models: A Tutorial, IEEE Comp., Vol.29,
No.12, pp.66–76 (1996).
Boudol, G. and Petri, G.: Relaxed memory models:an operational approach, Proc. POPL’09, pp.392–403(2009).
Atig, M.F., Bouajjani, A., Burckhardt, S. andMusuvathi, M.: On the veriﬁcation problem for weakmemory models, Proc. POPL’10, pp.7–18, New York,NY, USA, ACM (2010).
International Organization for Standardization (ISO):
Information Technology – Open Systems Interconnection– Security Frameworks in Open Systems – Part 3: AccessControl, Technical report, ISO/IEC 10181-3 (1996).
Bell, D. and LaPadula, L.: Secure computer systems:
Mathematical foundations and model, Technical Report M74-244, The MITRE Corporation, Bedford, MA(1973).
Biba, K.J.: Integrity Considerations for Secure Computer Systems, Technical Report MTR-3153, The

c 2012 Information Processing Society of Japan


[61]

[62]

[63]

[64]

[65]

[66]

[67]

[68]

[69]

[70]

[71]

[72]

[73]

[74]

[75]

MITRE Corporation, Bedford, MA (1977).
Clark, D. and Wilson, D.: A comparison of commercial and military computer security models, Proc. IEEE
Computer Society Symposium on Security and Privacy,
pp.184–194, IEEE Computer Society (1987).
Brewer, D. and Nash, M.: THE CHINESE WALL SECURITY POLICY, Proc. IEEE Computer Society Symposium on Security and Privacy, p.206, IEEE Computer
Society (1989).
Ferraiolo, D., Cugini, J. and Kuhn, D.: Role-based access control (RBAC): Features and motivations, Proc.
11th Annual Computer Security Application Conference, pp.241–248 (1995).
Ferraiolo, D. and Kuhn, R.: Role-Based Access Control,
15th NIST-NCSC National Computer Security Conference (1992).
Sandhu, R., Coyne, E., Feinstein, H. and Youman, C.:
Role-based access control models, Computer, Vol.29,
No.2, pp.38–47 (1996).
Ferraiolo, D., Sandhu, R., Gavrila, S., Kuhn, D. andChandramouli, R.: Proposed NIST standard for rolebased access control, ACM Trans. Information and System Security (TISSEC ), Vol.4, No.3, pp.224–274 (2001).
Sandhu, R. and Bhamidipati, V.: Role-based administration of user-role assignment: The URA97 model andits Oracle implementation, Journal of Computer Security, Vol.7, No.4, pp.317–342 (1999).
Sandhu, R., Bhamidipati, V. and Munawer, Q.: The
ARBAC97 model for role-based administration of roles,
ACM Trans. Information and System Security (TISSEC ), Vol.2, No.1, pp.105–135 (1999).
Crampton, J. and Loizou, G.: Administrative scope: A
foundation for role-based administrative models, ACM
Trans. Information and System Security (TISSEC ),Vol.6, No.2, pp.201–231 (2003).
Jha, S., Li, N., Tripunitara, M., Wang, Q. andWinsborough, W.: Towards formal veriﬁcation of rolebased access control policies, IEEE Trans. Dependable
and Secure Computing, pp.242–255 (2007).
Thomas, R.K. and Sandhu, R.S.: Task-Based Authorization Controls (TBAC): A Family of Models for Active and Enterprise-Oriented Autorization Management,
Proc. IFIP TC11 WG11.3 Eleventh International Conference on Database Securty XI: Status and Prospects,
pp.166–181, London, UK, Chapman & Hall, Ltd. (1998).
Becker, M., Fournet, C. and Gordon, A.: Design and
Semantics of a Decentralized Authorization Language,
CSF ’07: Proc. 20th IEEE Computer Security Foundations Symposium, pp.3–15, Washington, DC, USA,IEEE Computer Society (2007).
Halpern, J. and Weissman, V.: Using ﬁrst-order logic
to reason about policies, ACM Trans. Informationand System Security (TISSEC ), Vol.11, No.4, pp.1–41(2008).
Weissman, V. and Lagoze, C.: Towards a Policy Language for Humans and Computers, Research and Advanced Technology for Digital Libraries, Heery, R.
and Lyon, L. (Eds.), Lecture Notes in Computer Science, Vol.3232, pp.513–525, Springer Berlin, Heidelberg(2004).
Gofman, M., Luo, R., Solomon, A., Zhang, Y., Yang, P.
and Stoller, S.: RBAC-PAT: A Policy Analysis Tool forRole Based Access Control, Tools and Algorithms for
the Construction and Analysis of Systems, Kowalewski,
S. and Philippou, A. (Eds.), Lecture Notes in Computer

61

情報処理学会論文誌

[76]

[77]

[78]

[79]

[80]

[81]

[82]
[83]

コンピューティングシステム

Vol.5 No.2 51–62 (Mar. 2012)

Science, Vol.5505, pp.46–49, Springer Berlin, Heidelberg(2009).
Guttman, J., Herzog, A., Ramsdell, J. and Skorupka,
C.: Verifying information ﬂow goals in security-enhanced
Linux, Journal of Computer Security, Vol.13, No.1,
pp.115–134 (2005).
Saltzer, J. and Schroeder, M.: The protection of information in computer systems, Proc. IEEE, Issue 9, Vol.63,
pp.1278–1308 (1975).
Lipton, R.J. and Snyder, L.: A Linear Time Algorithm
for Deciding Subject Security, J. ACM, Vol.24, pp.455–
464 (1977).
Watson, R.N.M., Anderson, J., Laurie, B. and
Kennaway, K.: Capsicum: Practical capabilities for
UNIX, Proc. 19th USENIX Conference on Security,
USENIX Security’10, p.3, Berkeley, CA, USA, USENIX
Association (2010).
Spencer, R., Corporation, S.C., Smalley, S., Loscocco, P.,
Agency, N.S. and Andersen, M.H.D.: The Flask Security
Architecture: System Support for Diverse Security Policies, Proc. 8th Conference on USENIX Security Symposium - Volume 8, SSYM’99, pp.123–139, USENIX Association (1999).
Watson, R.N.M.: TrustedBSD: Adding Trusted Operating System Features to FreeBSD, Proc. FREENIX
Track: 2001 USENIX Annual Technical Conference,
pp.15–28, Berkeley, CA, USA, USENIX Association(2001).
KaiGai, K.: Security Enhanced PostgreSQL (2006),
available from http://code.google.com/p/sepgsql/.
Macmillan, K., Brindle, J., Mayer, F., Caplan, D., Tang,
J. and Technology, T.: Design and implementation of
the SELinux policy management server, Proc. Security
Enhanced Linux Symposium, pp.1–6 (2006).

前田 俊行 （正会員）
1977 年 12 月生．2006 年東京大学大学
院情報理工学系研究科博士課程修了．
博士（情報理工学）．現在，東京大学
大学院情報理工学研究科コンピュータ
科学専攻助教．

田中 英彦 （名誉会員，フェロー）
1970 年東京大学大学院工学系研究科
電気工学専門課程修了，工学博士．東京大学にて計算機アーキテクチャ，並列処理，人工知能，自然言語処理，分散処理，メディア処理等の教育・研究に従事．東京大学工学部教授，同大学
院情報理工学系研究科長を経て，2004 年情報セキュリティ
大学院大学情報セキュリティ研究科長・教授．情報処理学会名誉会員，人工知能学会論文賞，ACM SIGGRAPH’99

Impact Paper Award，人工知能学会功績賞，東京都科学技術功労者表彰，経済産業大臣表彰等受賞．情報・システ
ム研究機構教育研究評議会評議員，IEEE Fellow，東京大学名誉教授．

橋本 正樹 （正会員）2010 年 3 月情報セキュリティ大学院
大学情報セキュリティ研究科修了，博士（情報学）．同年 4 月より情報セキュ
リティ大学院大学情報セキュリティ研
究科助教．電子情報通信学会，日本ソフトウェア科学会，IEEE 各会員．電子情報通信学会 ISS・情報通信システムセキュリティ研究会専門委員．

安藤 類央 （正会員）
2006 年慶應義塾大学大学院政策・メディア研究科後期博士課程修了（政策・メディア）．同年情報通信研究機
構所属．ネットワークセキュリティ，仮想化システムセキュリティの研究に従事．

c 2012 Information Processing Society of Japan

62