組織内データセキュリティの定理証明による検証に関する研究

(1)

JAIST Repository

https://dspace.jaist.ac.jp/

Title 組織内データセキュリティの定理証明による検証に関

する研究

Author(s) 徳田, 拓

Citation

Issue Date 2006‑03

Type Thesis or Dissertation Text version author

URL http://hdl.handle.net/10119/1988 Rights

Description Supervisor:片山卓也, 情報科学研究科, 修士

(2)

修士論文

組織内データセキュリティの定理証明による検証に関する研究

北陸先端科学技術大学院大学情報科学研究科情報システム学専攻

徳田拓

2006

年

3

月

(3)

修士論文

組織内データセキュリティの定理証明による検証に関する研究

指導教官

片山卓也教授

審査委員主査

片山卓也教授

審査委員

二木厚吉教授

審査委員

小川瑞史特任教授

北陸先端科学技術大学院大学情報科学研究科情報システム学専攻

410086 徳田拓

提出年月: 2006年

2

月

Copyright c°2006 by Taku Tokuda

(4)

第 1 _{章序論}

1.1 情報セキュリティ

情報化社会といわれる現在，柔軟かつ透明であり，安全・安心で高い信頼性を有する

「高信頼性社会」の実現が，経済や社会の基盤として必要不可欠である．

情報セキュリティの目的は，システム内部の操作ミスや敵対的活動などの脅威から，情報及びシステムを守ることである．情報が水や電気と同じように，経済活動・社会生活の基盤を支えるインフラストラクチャになった今，企業や生活者が安心して情報を使えるようにし，情報の安全を確保することが重要な課題になっている．情報は国家や企業，国民一人ひとりの財産であるという観点から，その財産を守るために情報を安全に取り扱うための考え方やルールを設定する必要がある．このような経緯から，情報社会の中で活動を営むためのルールとして生まれた概念が，情報セキュリティである．それゆえ，情報セキュリティという言葉に含まれる意味は幅広く，個人情報を中心として企業の機密情報，個人の著作権など，さまざまな情報に対して生じる取扱責任を指す．具体的には，秘匿性，完全性および可用性を維持するこという．

秘匿性秘匿性

(confidentiality)

とは，特定の情報を特定の人間以外に知られないようにすることである．システム内に格納されたり，通信メッセージに含まれたりした秘匿すべき情報を，その情報を知ることを許されていない人間による不正な読み出しや，知ることを許された人間による不正な開示からも守らなければならない．

完全性完全性

(integrity)

とは，システムの状態が正しいことを保障することである．情報やサービスが事前の期待通りの状態であること，誤った更新，不正な更新を受けていないこと，正しさの保証がない情報を含んでいないことを含む．適用されるシステムやコンテキストによって，これらはシステム内の情報が互いにつじつまがあっている，システム内の情報が外界の状況を正しく表現している，システム内の情報やプログラムが不正な改竄を受けていない，システムが権限のないユーザの捜査を受けていない，システムが誤った入力を受けていない，といった用件に対応する．

可用性可用性とは，使用の権利を持つユーザが，CPU，メモリ，ファイル，装置，情報などのシステムのリソースやサービスを使用したいときに，実際に使用可能であることをいう．リソースの喪失，リソースの独占などにより，半永久的，あるいは一時的にそのリソースが仕様不可能になり，必要に応じた仕様が妨害されないようにしなければならない．

(9)

1.2 セキュリティポリシー

セキュリティポリシーとは，組織の情報セキュリティ関する基本方針である．セキュリティ対策を効率よく，効果的に行うための指針であり，恒久的にセキュリティを維持するための仕組みを指す．

•

組織のコンピュータやネットワークを不正アクセスなどの脅威から守ること

•

利用者・管理者のセキュリティ意識を向上させること

など，ネットワークシステムを含む社内情報システムの運用・利用の指針を，運用管理者や利用者に伝達，遵守させることを目的としている．また，ネットワークシステムを含む社内情報システムを円滑に運用するうえでの指針として，「何を」「どのように」「どの程度」行うのか，セキュリティ対策基準や個別具体的な実施手順などを含む．どの情報を誰が読み取れるようにするか，どの操作を誰に対して許可するか，どのデータを暗号化するかなど，情報の目的外利用や外部からの侵入，機密漏洩などを防止するための方針を定めたものや，コンピュータウイルス感染によるデータやシステムの破壊や，トラブルによる情報システムの停止，データの喪失などに対してどう対処していくか，といった項目まで含める場合もある．

セキュリティポリシーは細かく分類すると以下の

3

つから構成される．

•

エグゼクティブ・ポリシー（セキュリティ方針)

–

セキュリティ原則に基づく上位のポリシーで，社内規定に準ずる憲法のような存在

–

組織内のネットワーク/コンピュータシステム，運用実態から独立して規定守るべきこと（情報漏洩防止やルール厳守など）を記述

–

頻繁に更新しない

•

ポリシー・スタンダード（セキュリティ運用管理基準または安全対策基準）

–

企業リソースからプライオリティの高いリソースを決定

–

対策を実施カテゴリごとに分類し，リソースや実態を明記する法律のような存在組織内のネットワーク/コンピュータシステム，運用実態に則して規定

–

上位のポリシーに定められた守るべき情報を実現するための手段を記述

•

プロシージャ（セキュリティ手順書）

–

日々の手順を記述

–

一般社員，管理職，システム管理者，役員など，おのおのに適用される手順を規定

(10)

–

ポリシースタンダードを実践するための具体的な手段

セキュリティーポリシーを示すことにより，対外的なイメージや信頼性が向上するといったメリットもある．

1.3 セキュリティポリシーモデル

セキュリティポリシーモデルとは，システムが備えるべきセキュリティに関する要件を明解かつ簡潔に記述したものである

[4]．これは，システムのセキュリティを設計する際

に，セキュアなシステムの抽象概念を与えるガイドラインであると同時に，システムのセキュリティを形式的数理論理的に分析する基点となる．

計算機システムのセキュリティは個々の脅威に対する個別の対策の寄せ集めでは達成せず，システム全体のセキュリティを統一的に設計した上で構築し，そのセキュリティを評価すべきである．その際の統一的アプローチの理論的よりどころがセキュリティポリシーモデルである．したがってセキュリティポリシーモデルには，適用システム全体を抽象化し，セキュリティポリシーを正確に記述でき，システム全体のセキュリティ上の特性の分析を可能とすることが求められ，さらに構築したシステムがセキュアであることの検証にも利用できることが望ましい．そのためセキュリティポリシーモデルは数理論理学的な記法で記述することが多く，それによって自然言語による表現に伴う解釈の多様性や暗黙の了解のような曖昧さを排し，同時にモデルのセキュリティ上の性質の論理的な推論による証明を可能とする．

セキュリティポリシーモデルの研究の歴史は長い．古くは

1960

年代のタイムシェアリングシステムの発展の過程で，米軍の情報管理ポリシーであるマルチレベルセキュリティのモデル化と，オペレーティングシステム（OS）への実装が進められた．1980 年代には軍用以外のシステムにおいてもセキュリティポリシーのモデル化が盛んに行われた．会計システムなどのアプリケーションによるセキュリティポリシーにも目が向けられるようになった．

近年は，World Wide Web の普及に象徴されるように，情報処理環境が大きく変化し，

情報セキュリティに対する社会的要求も高度化かつ多様化している．それに伴って，セキュリティポリシーモデルが表現すべき内容やその記述形態についても多様な要求がある．そのため，特定のポリシーに特化したモデルだけではなく，多様なポリシーに対応可能な，表現力の高いモデルの研究が盛んである．大規模分散ミドルウエアなど，設計，構築にセキュリティポリシーモデルを適用すべきシステムは多い．

セキュリティポリシーモデルはそれぞれ表現能力に特色があり，秘匿性を重視したモデル，完全性を重視したモデル，秘匿性と完全性を兼ね備えた複合型モデル，中立型モデルに分類される．代表的なセキュリティポリシーモデルとしては

• Bell

−

LaPadula(Devid Bell&Len Lapadula)

• Biba Protection(Biba)

(11)

• CMW(John Woodward)

• Type Enforcement(Earl Boebert&Richard Kain)

• Role-based Access Control(David Ferraiolo&Richard Kuhn)

• Chinese Wall(Brewer&Nash)

• Clark-Wilson(Claerk&Willson)

• Infomation-Flow

• BMA

などがある．BMAは英国医学協会が考案した医学倫理の情報流れ制御を定義したモデルだが，これらのセキュリティポリシーモデルのほとんどは，米国国防総省がスポンサーとなって考案を委託したものである．

ただし，近年セキュリティポリシーという言葉の拡大解釈が進んだ結果，セキュリティポリシーモデルの定義はあやふやなものとなった．今日では，

ISO15408

の普及に伴い，プロテクションプロファイルやセキュリティターゲットなど，新しい用語の追加と再定義が実施され，システムの保護要件を表す言葉として分類して使われるようになった．

1.4 情報セキュリティの基準

セキュリティが要求される情報処理システムの提供者は，消費者からの「本当にセキュリティは守られているのか？」という問いには答えなければならない．また，システムを提供者も，システムの開発において同じ質問を自身に問いかけることになる．この問いに答えるための方法を提示したものが情報セキュリティの評価基準である．情報セキュリティの評価基準は，各国の国内基準から世界標準まで，多数存在する．

第三者機関による，セキュリティ基準に準じた評価と公的な認証により，IT製品・システムに関する知識が乏しい消費者でも，安心して製品・システムを選択することができる．また，提供者はセキュリティ設計への不安を取り除き，消費者に対しては，IT製品のセキュリティ向上に積極的に取り組む企業姿勢を強くアピールでき，製品セキュリティへの信頼と安心を確保できる．

1.4.1 ISO15408

かつては，情報セキュリティの基準に関し各国が独自で基準をもっていたが

(1985

年にアメリカ，1991年にフランス，イギリス，ドイツ，1993年にカナダに制定)，1990年から

ISO

でそのジャンルの国際標準の作成が進められ，ITセキュリティ評価のコモンクライテリア

(CC:Common Criteria)

が作られた．CCを元に，1996年

6

月に国際標準の情報

(12)

セキュリティの基準として

ISO15408(ISO/IEC 15408)

が制定された

[1]．またこれと同時

に，この標準のインポートによる国内標準化が開始され，2000年

7

月には

JIS

標準（JIS

X 5070）として制定さた．両者の規定内容は，同一のものとなっている．

評価・認証の手順

CC

では，多くのコミュニティのニーズに対処することができる

IT

セキュリティ基準のセットを定義している．これらはセキュリティ要件と呼ばれる．また，CCでは，評価対象のことを

TOE(Target of Evaluation)

と呼ぶ．TOEの開発は，まず

CC

の用意するセキュリティ要件を元に，TOEに対するプロテクションプロファイル，セキュリティターゲットの開発を行う．

プロテクションプロファイル(PP：セキュリティ要件仕様書)とは，

TOE

に対するセキュリティ要件を記述したものである．具体的なシステムの実装とは依存しない形式で書かれており，他の実装で再利用が可能となる．PPは，CCの

PP

に対する評価基準に照らし合わされ，完全で一貫しており，かつ技術的にしっかりしており，TOEに対する要件の記述として適しているか評価される．そして，PPは合否判定がなされ，合格した

PP

は登録される．

セキュリティターゲット(ST：セキュリティ設計仕様書)とは，評価済みの

PP

を基にして作成され，TOEの評価に対するセキュリティ要件に加え，設計仕様を記述したものである．システムが具体的に備える保護メカニズムと

TOE

がどのように結び付けられるかを，ある程度詳細に記述してある．STは，CCの

ST

に対する評価基準に照らし合わされ，

完全で一貫しており，かつ技術的にしっかりしており，TOEに対する要件の記述として適しているか評価される．そして，STは合否判定がなされ，合格した

ST

は登録される．

以上のステップを踏まえた上で，TOEは，STで記述される内容を具体化し，実装される．

1.5 本研究の背景と目的

1.5.1 背景

現在，情報化社会となり，政府から民間，個人に至るまで情報を扱う様々な活動が盛んに行われている．そこでは，必ずといっていいほど情報技術が関わるシステムが存在し，

活動を管理・支援している．情報技術が社会生活に及ぼす影響が大きくなり，ますます高信頼である情報化社会が求められ，それを実現するする様々な技術の研究が行われている．

(13)

ソフトウェアの開発では，その問題の多くが分析・設計などの上流工程で作りこまれ，

それが全体の生産性や品質に支配的な影響を及ぼしていることがよく知られている．このようなエラーを取り除くため，上流工程段階からモデルを形式化し，正しさを確認・検証しながらシステムの構築を行い，高信頼なソフトウェアの開発を実現しようとする研究が行われている．

一方，情報セキュリティが重要視される中，IT製品のセキュリティの標準化が行われてきた．それまでは，ソフトウェアごとにセキュリティ仕様は定めらていた．しかし，この状況は開発者は何を実現すればよいか不明瞭であったし，消費者にとっても何が守られているか不明瞭であった．この状況に対し，公的機関がセキュリティの標準化を行い，これにより，開発者にとっては実装すべきセキュリティ機能が明瞭かさた．また，消費者は製品の詳細を理解できなくとも，公的機関の標準規格を満たしているということで安心を得ることができるようになった．現在では，世界標準として

ISO15408

が用いられるようになった．

これから，セキュリティ標準が社会に浸透としていくことは間違いない．この状況の中，形式検証の対象としセキュリティという概念を扱うことが必要とされる．

1.5.2 目的

システムの開発には，そのシステムが満たすべき機能要求・セキュリティ要求がある．

また，システムの開発過程では，システムの形式モデルを抽象度の高い状態から具体化することで実装を行う．この形式モデルは，そのシステムに与えられた機能要求・セキュリティ要求を実際に満たしている保証はない．本研究では，高階述語論理

HOL[2]

による定理証明を用いて，形式モデルが機能要求・セキュリティ要求を満たしているか検証する方法を提案する．

検証により，上流工程の仕様書や形式モデルの機能要求に対する不具合・セキュリティ要求に対する不具合を発見できる．また，これを取り除くことにより，機能的・セキュリティ的に正しいことが論理的に証明された形式化モデルが得られる．

1.6 構成

本研究では，HOLを用いた検証により，形式化されたモデルが，それに対する機能要求やセキュリティ要求を満たされていることを示す方法と，一連の流れを事例ベースで述べる．事例として，STに準ずる一般的なファイアーウォール

(FW)

サーバに関する仕様書を前提とする．まず仕様書に関し，オブジェクト指向での形式化を行い，形式化モデルに対し検証を行う．検証までの流れは以下のようになる．

1. FW

サーバシステムの

ST

に準ずる仕様書を想定する

2.

仕様書を元に

UML

でモデル化をし，クラス図，コラボレーション図を作る

(14)

3.

モデル化したものをオブジェクト指向理論を用いて

ML

でコード化する

4. ML

コンパイラを用いて簡単な実行テストし，コード化で起こるようなバグを取り

除く

5.

コードを

HOL

形式に書き直す

6.

仕様書の内容を証明するための，システム上の述語で命題を定義

7.

命題の証明

第

2

章では，形式化と形式検証について説明する．第

3

章では，仕様書のオブジェクト指向による形式化方法と，UML，ML形式・HOL形式での記述について述べる．第

4

章では，FWサーバの

ST

を基にした事例について，UMLによるモデル化から

HOL

形式による記述までについて述べる．第

5

章では，4章で得られた形式化モデルに対しおこなった検証について述べる．第

6

章では考察を行い，第

7

章でまとめと今後の課題を述べる．

(15)

第 2 _{章検証手法}

2.1 形式検証

高信頼のソフトウェアを開発するために，開発の上流工程において早期に効率よくシステムの不具合を発見する手段として，形式検証の技術を開発に適用する試みが広がっている．形式検証はシステムの信頼性向上を目的とする技術であり，計算機支援を前提として数学的な基礎基づくことを特徴とする. 形式検証は，大きく分けて定理証明による演繹手法とモデル検査手法がある．

2.1.1 演繹手法

演繹手法では与えられた性質を対象システムが満たすことを論理体系にしたがって証明する．表現力の高い論理体系を用いると広範なシステムを検証対象にすることができる．

しかし，すべての定理を自動証明することは不可能であることがわかっている．このため，定理証明支援系の場合，人が証明の途中結果を理解した上で，帰納法などのルールを選択する必要がでてくる．演繹手法による検証方法では，対象が誤りを含む場合，対象記述のどこに誤りがあるかを見つけることが難しい．

2.1.2 モデル検査手法

モデル検査技法では対象を有限の状態空間で表現できるシステムに限定する．有限であることから状態の網羅的な探索が可能であり，自動検証が可能となっている．モデル検査技法では，対象が誤りを含む場合，網羅的な探索を行うことから反例を見つけることができる．

2.2 オブジェクト指向モデルにおける形式検証

現在，オブジェクト指向によるソフトウェアの開発が主流であり，本研究の検証対象である

FW

サーバシステムについても，オブジェクト指向によるモデル化と，オブジェクト指向に即した検証を行う．ここでは，まずオブジェクト指向は何かということを述べる．

次に，本研究で用いる検証法について述べる．

(16)

2.2.1 オブジェクト指向

オブジェクト指向はソフトウェアの開発技術の

1

つで，その名前が示すとおり「オブジェクト」という単位ですべてをとらえる考え方である．

•

システム化対象となるビジネスをオブジェクト間のコミュニケーションとして考える

•

システムをオブジェクトの集合ととらえる

•

オブジェクトの振る舞いをプログラムで記述する

というようにあらゆる事象をオブジェクトとして考えていくのがオブジェクト指向である．オブジェクト指向は，大規模・複雑化するソフトウェア開発において開発効率を向上させる技術として注目されている．

オブジェクト指向によるシステム開発では，

•

オブジェクト群がどのような構造を持っているのか

•

オブジェクトの間でどのようなメッセージが交わされるのか

など，さまざまな視点からオブジェクトをとらえる．これらは，図（ダイアグラム）を使って表される．こうした図のことをモデルという．モデルを用いることで，技術者間でより正確にオブジェクトに関する情報や考えを交換することが可能となる．これは，街を地図に表すことによって，特定の建物や場所の位置，あるいは標高といった情報が皆で共有できる情報として扱えるようになる様と似ている．しかし，モデルを正確に読み取るためには，モデルの描き方のルールを定める必要がある．そうしたモデルの描き方のルールを定めたものを表記法という．

以前は，オブジェクト指向の世界には，OMT法や

Booch

法といったオブジェクト指向を使ったシステム開発のための方法論が乱立し，それぞれで独自の表記法を作っていたため，多くのの表記法が存在した．そのような状況では，同じ「クラスの構造を表すモデル」を描くための表記法が何通りも存在し，方法論が変わるたびに，別の表記法を用いなければならなかった．また，異なるエンジニアの間で情報交換をする際も，表記法が違なるためにモデルが理解できず，スムーズな情報交換ができないという問題もあった．

そこで乱立する表記法を統一するために作られたのが

UML(Unified Modeling Language)

である．Unified（統一）という言葉の由来はそこから来ている．UMLはオブジェクト指向によるシステム開発で用いられるさまざまなモデルの表記法を標準化していき，1997 年に

OMG（Object Management Group:オブジェクト指向技術の標準化団体）の標準と

なった．以後，オブジェクト指向業界での表記法のデファクトスタンダードとして用いられるようになった．

(17)

2.2.2 オブジェクト指向の性質と検証法の選択

オブジェクト指向モデルでは，システムは複数のオブジェクトから構成され，それらの協調動作により，システム全体としての機能が実現される．これを状態遷移に基づく形式化により各オブジェクトの状態を状態遷移で表す場合，協調動作を検証するためには複数のオブジェクトの状態遷移図を合成する必要があり，状態爆発が起こる可能性がある．本研究の検証対象は，STなどの仕様書で記述される様なシステムであり，このようなシステムでは，多数のオブジェクトが存在することが予想され，状態遷移に基づいたモデル化は困難であると場合が多いと考えられる．

これに対し，矢竹ら

[3]

はコラボレーションに基づくオブジェクト指向モデルの検証法を提案し，オブジェクト指向理論を定理証明システム

HOL

上の論理モジュールとして定義した．オブジェクト指向理論では，システムの状態はひとつのデータ型として表現され，コラボレーションは，その上の関数適用列として表現される．これにより，システムの無限の状態を

1

つと扱うことができ，任意数のオブジェクトに対応することが可能となる．また，コラボレーションベースの検証法では，メソッド呼び出しという，オブジェクト間の協調動作を直接捉える視点でシステムの振舞いを定義できるため，段階的振舞いによる近似法のように，合成された状態遷移図から協調動作に代わる状態遷移図を抜き出すオーバーヘッドがなくなる．

以上の理由より，複数オブジェクトを扱うことを想定している本研究では，検証手法として矢竹らが提案したオブジェクト指向理論を用いて，HOL上において定理証明による検証を用いることにした．

2.2.3 コラボレーションベースの検証法

ここでは，本研究が扱うコラボレーションの定義を確認し，コラボレーションベースの検証法について説明する．

コラボレーション

コラボレーションとは，システムのまとまった機能を実現する複数オブジェクト間の協調動作である．システムのまとまった機能とは，オブジェクト間のメソッド呼び出しを複数個組み合わせて実現される．

本研究が対象とするコラボレーションは，演繹的証明において，システムの評価対象となる状態から，次の評価対象となる状態までの遷移を実現する関数列である．例えば，対話型のシステムの場合，ユーザがコマンドを打ち込んでから，次にシステムがコマンドを受け付けることができる状態になるまでの，システムの一連の動作がコラボレーションにあたる．

(18)

䉮䊙䊮䊄 ฃઃน⢻

䉮䊙䊮䊄 ฃઃਇน⢻

㪸

㪹㪺

図

2.1:

対話型システムの関数列とコラボレーションの関係

図

2.1

はこれをモデル化したものである．

a

，

b

，

c

は状態の遷移を引き起こす個別の関数とする．ここで，コマンド入力可能状態から，次のコマンド入力可能状態への遷移は，

関数列

abc

によってのみ実現される．関数列

abcabc

もコマンド入力可能状態から，コマンド入力可能状態への遷移ではあるが，途中で評価対象となる状態を通過しているため，

演繹証明の帰納段階とするのは不適切である．

システムには複数のコラボレーションが存在し，それらが繰り返し適用されることによりシステムは状態変化する．

演繹的手法による証明

オブジェクト指向におけるコラボレーションベースの定理証明について説明する．コラボレーションとは，システムのまとまった機能を実現するオブジェクト間の協調動作である．一般に，システムには複数のコラボレーションが存在し，それらが繰り返し適用されることによりシステムは状態変化する．すなわち，システムは次の

2

つの組で定義される．

System = (S, F )

S

はシステムのとりうる状態の集合であり，初期状態

s

₀を含む．

F

はコラボレーションの有限集合であり，各コラボレーションは状態を変化させる関数

f : S → S

である．¹

コラボレーションの平行性は考慮しない．つまり，それぞれのコラボレーションはアトミックに適用され，インターリーブすることはない．

前提となる状態に対する

S

上述語

P

_assumption，結果となる状態に対する

S

上述語

P

_conclusion とすると，

P

_assumption

(s) ⇒ P

_conclusion

(f (s)) (f ∈ F )

により，コラボレーション前後の状態に対する命題が与えられる．

1f はf :int→S→string∗S のように入出力を伴うことがある．ここでは簡単のため，入出力がない場合の定式化を示す．

(19)

特に，P_assumption

= P

_conclusionの場合，一般にこれを不変表明といい，システム上で常に成り立つ性質を述べるために使われる．不変表明の証明は，初期状態からの遷移列に関する帰納法を用いる．

•

初期段階

P (s

₀

)

•

帰納段階

P (s) ⇒ P (f (s)) (f ∈ F )

初期段階・帰納段階を示すことで，不変表明が常に成り立つことを演繹的に証明できる．

(20)

第 3 章形式検証までの流れ

本章では，自然言語の仕様書から形式化を行い，HOLによる定理証明を行う段階までについて述べる．全体の流れは

1. UML

のクラス図，コラボレーション図による，オブジェクト指向モデルの作成

2.

オブジェクト指向理論の論理モジュールを生成

3.

オブジェクト指向理論を用いた

ML

によるモデルのコード化

4. ML

形式での実行テスト

5. ML

形式による記述を

HOL

形式に変換

6. HOL

による証明

となる．

3.1 形式化

3.1.1 形式化とは

一般にソフトウェア開発の過程では，自然言語で記述されるような仕様書から，形式化を行う．抽象度の高い形式化された設計記述から設計記述の詳細化・細分化を行い，最終的にコード化し実装に至る．抽象度の高いモデル化では以下の

2

点に注意しなければならない．

•

各詳細化のレベルは，上位レベルの完全な具体化であること（すなわち，より高い抽象度で定義されたすべてのセキュリティ機能，特性，及びふるまいが，下位レベルにおいて実証的に提示されていなければならない）

•

各詳細化のレベルは，上位レベルの正確な具体化であること（すなわち，上位レベルにおいて必要のないセキュリティ機能，特性，及びふるまいが，より低い抽象度で定義されるべきでない）

(21)

また，そこから実行テスト，統合テストと繰り返し完成となる．この抽象度の高い過程は上流過程，コードに近い過程を下流過程と呼ばれる．形式検証とは，実装段階のコードによるシュミレーションではなく，抽象度の高い段階でのモデルに対し，モデル検査や定理証明によって検証を行うことである．

3.1.2 形式化モデルに対する検証の必要性

本研究では，ST程度の仕様書が前以って与えられていることを想定している．STは，

実装に依存しない形式である

PP

に実装に依存する情報を追加したものである．

ST

は，機能要求・セキュリティ要求について，自然言語や図表などにより非形式的な形で記述されたものである．

開発者は，STや

ST

を更に詳細化した仕様書に基づき，形式モデルを作ることになる．

ここで作り出される形式化モデルは，開発者が非形式的な仕様書の内容を満たすように，

創作したものであるが，そのモデルが仕様書の機能要求やセキュリティ要求を満たしている保証はない．そのため，作り出されたモデルが機能要求やセキュリティ要求を満たしているかを検証する必要がでてくる．

3.2 UML _{によるモデル化}

3.2.1 UML によるモデル化の必要性

上位レベルでの設計記述は，開発工程全体で参照されるセキュリティ機能，特性，及びふるまいを明確に理解しやすく示す必要がある．本研究で用いる，オブジェクト指向理論

による

ML(または HOL)

形式による記述でも，抽象度の高い設計記述は可能である．し

かし，ML形式で書かれた設計記述はコードに近い記述であり，開発に携わる者すべてにとり明確にわかり易く記述されたモデルであるとは言い難い．これには，現在最も一般的に用いられている

UML

による記述が適している．

検証は，UMLで示された設計記述を，オブジェクト指向理論による

HOL

形式に忠実に変換し，検証を行う．これにより，機能要求・セキュリティ要求を満たす

UML

モデルが得られることになる．

3.2.2 使用するダイアグラム

UML

は

9

種類のダイアグラムからなっており，用途に合わせ，それらを組み合わせて用いる．本研究では，UMLのダイアグラムとしてクラス図とシーケンス図，コラボレーション図を用いる．クラス図はシステムの静的構造を表すものであり，様々な種類のクラ

ス

(タイプ)

とそれらのクラス間の関係

(リレーションシップ)

で構成されている．クラス

図はオブジェクト指向分析・設計において最も重要なダイアグラムであり，オブジェクト

(22)

指向分析・設計の根幹をなす．シーケンス図・コラボレーション図は，複数のオブジェクトにまたがる協調動作を記述する動的モデルである．シーケンス図は時間に焦点をおき，

コラボレーション図は空間に焦点を置いているが，基本的に表現できることは同じである．

HOL

による検証では，システムのオブジェクト間の協調動作による状態の変化についての，演繹的な証明によっておこなう．よって，協調動作するオブジェクトを定義するクラス図と，演繹的証明に用いるための，状態の変化をもたらすコラボレーションを記述したシーケンス図（コラボレーション図）を作る必要がある．

3.2.3 オブジェクト指向理論を意識した UML の記述

UML

によるモデル化が完成すると，次のステップとして，オブジェクト指向理論を用いた，ML形式・HOL形式への変換を行う．これを念頭に置き，クラス図の属性値名や操作名，コラボレーション図のオブジェクト間のメッセージ通信における関数名，引数，

返り値，ガード条件などは，ML形式で共通で使う名称・形式が望ましい．

また，1つのコラボレーションは複数の操作のまとまった機能であるが，それを構成する操作もまた，複数の操作のまとまった機能である場合がある．これらの操作に対しても，その内容についてのコラボレーション図を描いておくことが望ましい．ただし，すべての操作を詳細化しコラボレーション図を書くのは，非常に労力がかかるため，内容を記述する必要のないような自明な操作についての記述は省いてよい．コラボレーション図を書く段階で，ある程度具体化をしておくと，HOL上での記述への変換がスムーズに行うことができる．

3.3 オブジェクト指向理論

矢竹ら

[3]

は，オブジェクト間の協調動作による状態の変化についての，演繹的な証明をおこなうためのシステムを実現するための土台として，オブジェクト指向理論を

HOL[2]

に定義した．HOLでは，システム状態はストアと呼ばれるデータ型で表現する．ストアは，直感的にはシステムに存在するすべてのデータを保持する環境であり，その上にオブジェクトを操作するためのいくつかの基本演算子が定義される．コラボレーション，および，証明する命題は，これらの基本演算子と

HOL

の理論ライブラリが提供する関数群を用いて定義される関数，述語である．

検証の流れとしては，まず，ユーザはシステムのクラスモデルを定義する．クラスモデルは

UML

のクラス図のように，システムの静的構造を定義するモデルである．具体的には，クラス名，属性名とその型，継承関係を定義する．クラスモデルは，特定の形式でファイルに宣言され，理論生成機に入力される．理論生成機とは，矢竹らが

HOL

のメタ言語である

Moscow ML [2]

で実装したツールであり，対象システムのクラスモデルに基づき，そのシステムの特化した理論を

HOL

理論モジュールとして構築する．理論モジュールとは，HOLにおけるここの理論の単位であり，型，定数，公理，および定理を格納す

(23)

る

ML

ストラクチャである．構築は

Definitional Extention

に従う．つまり，自然数やリストといった

HOL

の既存理論を，定義の導入のみにより拡張し，それらに関する定理を既存の推論規則によって証明する．これは

HOL

において健全な理論を構築する基本的な手法である．ユーザはこの理論に与えられる基本演算子と

HOL

が提供する関数郡を用いて，コラボレーション，および不変表明を，システムの初期状態からの遷移列に関する帰納法により証明する．

3.3.1 クラスモデル

クラスモデルは，システムの静的構造を定義する．具体的には，クラス名，属性名とその型，継承関係を定義する．定義に先立ち，型の集合

T ype

を導入する．T ypeの要素は，

HOL

における，各変数を含まない任意の型である．

クラスモデルは，以下の

5

つの組として定義される．

CM = (C, A, M

_attr

, M

_inher

, T )

• M

_attr

: C → P ow(A)

• M

inher

: C → P ow(C)

• T : C × A → T ype

C，A

はそれぞれ，システムに出現するクラス名の集合，属性名の集合である．M_attr は，クラスと，その属性集合を対応付ける写像である．Minherは，クラスと，その子クラス集合を対応付ける写像である．現在のところ，継承関係は，単一継承のみサポートしている．T は，クラスと属性に対し，その属性の型を対応付けている写像である．C

⊂ T

とし，クラス名をそのクラスに属するオブジェクトの型とする．

理論生成機に入力される，ファイルには，クラス名と属性名，属性名の型，属性の初期値を記述する．属性名の型，属性の初期値は

HOL

型と

ML

型の両方記述しておく．ファイルを理論生成機に入力すると，HOLの理論モジュールが出力され，理論モジュールを読み込むことで，クラスモデルに特化したオブジェクト指向理論を

HOL

上で使用できる．

クラスモデルを定義するファイルのフォーマットは以下のようになる．

class (1)

attr (2) holtype : (3) | (4) mltype : (5) | (6)

• (1):クラス名

• (2):属性名

• (3):属性の HOL

形式の型

(24)

• (4):属性の HOL

形式の初期値

• (5):属性の ML

形式の型

• (6):属性の ML

形式の初期値

具体例として，

2

次元座標上の位置を表すクラス

person

があるとする．クラス

position

は，属性として

int

型の

x

座標を表す

x，int

型の

y

座標を表す

y

を持つ．x，yはそれぞれ初期値

0，1

を持つとする．このときのクラスモデルを定義するファイルの記述は以下のようになる．

class person

attr x holtype : num | 0 mltype : int | 0 attr y holtype : num | 1 mltype : int | 1

ML

形式と

HOL

では，型の表記が多少異なる．HOLでは

int

型は無いため，num型とする．また，ペアの表記も異なり，int型のペアは

ML

形式では

int * int

，HOL形式では

num # num

となる．また，bool型の定数は

ML

形式では

true false

となるが，HOL 形式では

T F

となる．

3.3.2 ストアとオブジェクトの型

変数，定数の型として，bool，num，string，listなど，HOLの既存理論で提供されるものに加え，オブジェクト指向理論では，ストアやオブジェクトについての型が与えられる．

ストアは，型

store

として定義される．storeは定数として

store emp

をもつ．これは，

どのクラスのオブジェクトも生成されていない，空のストアを表す．

クラス

c ∈ C (C

はシステムに出現するクラス名の集合)に属するオブジェクトは，型

c

をもつ．各

c

は，定数として

c null

をもつ．これは，そのクラスの

NULL

オブジェクトを表す．NULLオブジェクトはストアには存在しない．

3.3.3 基本演算子

オブジェクト指向理論では，6種類の基本演算子がストア上に定義される．

new

演算子ストアに新たなオブジェクトを生成する関数

is

演算子オブジェクトが特定のクラスのインスタンスであるかを検査する述語

ex

演算子オブジェクトがストアに存在するかを検査する述語

cast

演算子オブジェクトの方変換を行う述語

(25)

get

演算子オブジェクトの属性値を取得する関数

set

演算子オブジェクトの属性値を更新する述語

これらの演算子は以下のように定義される．

• c new : store → c ∗ store (c ∈ C)

• c is d : c → store → bool (c, d ∈ C, c ¢

^∗

d)

• c ex : c → store → bool (c ∈ C)

• c cast a : c → store → d (c, d ∈ C, c ¢

⁺

d or d ¢

^∗

c)

• c get a : c → store → T (c, a) (c ∈ C, a ∈ Mattr(c))

• c set a : c → T (c, a) → store → store (c ∈ C, a ∈ Mattr(c))

ここで，¢，¢⁺，¢^∗は，クラスの継承関係を表す記号である．c

¢ d

は，cが

d

の親クラスであることを意味する．つまり，d

∈ Minher(c)

と等価である．さらに，c

¢

⁺

d

は，

c

が

d

の祖先クラスであることを，c

¢

^∗

d

は，c

= d

または

c

が

d

の祖先クラスであることを意味する．

3.3.4 関数，コラボレーションの記述

関数

関数は，基本演算子を組み合わせて記述する．例として，クラス

person

に関する関数の定義を示す．クラス

person

は，int型の属性として

x

座標

x，y

座標

y

持つとする．また，クラス

person

は関数

person move

を持つとする．

move

は，x座標，y座標それぞれ，

dx，dy

だけ移動させる．この関数は，属性

x，y

に対する

get

演算子，set演算子と，ML の整数ライブラリに提供される’+’を用いて，ML形式で以下のように定義される．

person_move : person -> int -> int -> store -> store fun person_move p dx dy store =

let

val x = person_get_x p store val y = person_get_y p store

val s0 = person_set_x p (x+dx) store val s1 = person_set_y p (y+dy) s0 in

s1

end;;

(26)

また，すでに定義された関数は，他の関数で使用できる．person move を用いて，x座標を

1

加える関数

person incX

は以下のように記述される．

person_incX : person -> store -> store

fun person_incX p store = person_move p 1 0 store;;

コラボレーションの記述

コラボレーションは，まとまった機能を実現する複数オブジェクトの協調動作である．

これは，複数の関数や基本演算子からなる，機能単位の関数である．よって，記述に関しては，基本的に関数の記述と同じである．

コラボレーションの例を挙げるため，もうひとつのクラス

history

を用意する．クラス

history

は，位置の履歴を残すためのクラスで，(int*int) list型の属性

record

をもつ．また，クラス

history

は関数

addRecord

を持つとする．これは，recordに履歴を追加する関数であり，以下のように定義できる

history_addRecord : history -> int -> int -> store -> store fun history_addRecord h x y store =

let

val record = history_get_record h store

val s0 = history_set_record h ((x,y)::record) store in

s0 end;;

ここで，personのを移動させ，移動先の位置履歴を記録するコラボレーション

moveAndAddHistory

を定義すると以下のようになる．

moveAndAddHistory : person -> history -> int -> int -> store -> store fun moveAndAddHistory p h dx dy store =

let

val s0 = person_move p dx dy store val x = person_get_x p s0

val y = person_get_y p s0

val s1 = history_addRecord h (x,y) s0 in

s1

end;;

(27)

3.3.5 公理

公理は，オブジェクト指向理論で定義した定数や演算子に関する基本的性質を記述したものである．公理は

36

種類存在する．証明の作業では，必要に応じ公理を用いることで，

証明内容の単純化や証明を得ることができる．以下に代表的な公理を

2

つ挙げる．

• ∀o s. c ex o s ⇒ (c get a o (c set a o x s) = x)

オブジェクト

o

がストアに存在するならば，その属性

a

を

x

に変換し，その直後に同じ属性を取得したとき，その値は

x

である．

• ∀o

1

o

2

s. ¬(o

1

= o

2

) ⇒ (c get a o

1

(c set a o

2

x s) = c get a o

1

s)

オブジェクト

o

₂の属性

a

を更新直後，それとは異なるオブジェクト

o

₁の同じ属性を取得したとき，その値は，更新前に得られる値と等しい，つまり，異なる

2

つのオブジェクトの属性は独立している．

これらの公理を用いて証明は行われる．証明の基本的な流れは以下のようになる．

1.

命題を基本演算子に分解しする．

2.

それぞれの形に適した公理を用いて，冗長な部分を削除・単純化する．

3.

公理を用いて，真理値を得る

矢竹らは，証明作業において，これらの公理を必要に応じて適応するタクティック

(証

明戦略)もいくつか提供している．

3.4 ML _形式， HOL _{形式での記述}

HOL

は

ML

の上に作られた定理証明器である．本研究での演繹的な証明は定理証明システム

HOL

を用いて行われる．そのため，

HOL

形式によるシステムの記述は必須事項である．しかしながら，HOLでは，関数を実行するという概念がない．したがって，UML 図から直接

HOL

形式の関数に変換した場合，実行テストができないので，関数の記述段階で起こりうるバグが取り除きづらいといえる．

本研究では，モデルの仕様に対する本質的な機能やセキュリティの不具合に関する証明を目的としており，HOLの証明段階でこのようなバグが含まれていた場合，不必要な混乱を引き起こす原因となる．そのため，HOL形式の記述段階では，下流工程で起こりうるようなバグが，取り除かれていることをが望ましい．

以上の理由より本研究では，まず

ML

形式で記述し，テスト実行を行った後

HOL

形式へ変換する．

(28)

3.4.1 ML 形式化とテスト実行

オブジェクト指向モデルの

ML

形式化を行う．具体的にはオブジェクト指向理論により与えられる基本演算子を用いて，システムのコラボレーションを関数として記述する．

システムのコラボレーションは，この段階では

UML

のシーケンス図（コラボレーション図）によって記述されており，それを元にコード化を行う．基本的な記述法については，

section 3.3.4

を参照されたい．

記述した関数，コラボレーションに対し，実行テストを行う．実行テストは，関数に具体的な値を入れ，返り値をチェックする．ただし，オブジェクト指向理論による関数の多くは，オブジェクトの中身の更新を行う関数であり，返り値は更新されたストアとなる場合が多い．このため，チェック対象となる属性を表示する関数を別途用意しする必要がある．例として，クラス

person

の属性

x，y

を知るためには，以下のような関数が必要となる．

info_person : person -> store -> (int*int) fun info_person p store =

let

val x = person_get_x p store val y = person_get_y p store in

(x,y) end;;

これにより，info personを用いて，person moveについて以下のような実行テストが行える．前提として，状態

store

で

person

型の

p

が，座標

(1,1)

にいるとする．

- info_person p store;;

- - > val it = (1, 1) : int * int

- val newStore = person_move p 1 2 store;;

- - > val newStore = store : store - info_person p newStore;;

- - > val it = (2, 3) : int * int - info_person p store;;

- - > val it = (1, 1) : int * int

ここでは，まず，初期状態でのストア（store）における，prerson型のオブジェクト

p

の位置

(1, 1)

を表示した．次に，pを

x

軸方向に

1，y

軸方向に

2

動かした（person move

p 1 2 store）．person move

は，返り値として更新されてストアを返すだけで，思ったとおりに機能したかは判定できない．次に，その更新されたストア（newStore）における

p

の位置

(2, 3)

を表示させた．

(29)

また，冗長であるが，再び初期状態でのストア（store）における，pの位置

(1, 1)

を表示させた．これにより，状態を表す変数ストアが，各状態を正しく保存していることがわかる．

3.5 _証明

システム対し，演繹的方法により証明を行う．システムは，そのとりうる状態の集合

S (s

₀

∈ S)，状態を変化させるコラボレーション f : S → S

の集合

F

の組によって定義さ

れる．

System = (S, F )

証明は

HOL

で行うため，まず

ML

形式で記述したものを

HOL

形式に変換する．

3.5.1 HOL 形式化

ML

で記述した関数を

HOL

形式に変換する．ML形式と

HOL

形式では，記述の文法が多少異なる．また，MLが提供する関数群と

HOL

が提供する関数群は異なる．共通である関数（+，-，etc.）は書き直す必要は無いが，HOLで定義されていない関数は，その関数に相当する

HOL

形式の関数に書き直さなければならない．

例えば，

filter fst snd hd ("stringA"^"stringB")

などは，それぞれ

FILTER FST SND HD (STRCAT "stringA" "stringB")

に書き直す．また，中には

ML

の関数に対応する

HOL

の関数が存在しない場合がある．

この場合，MLの関数に対応する関数を定義する必要がある．

ML

形式での定義と

HOL

形式の定義を比較する．ML形式の

person move

の定義は以下のように記述された．

fun person_move p dx dy store = let

val x = person_get_x p store val y = person_get_y p store

val s0 = person_set_x p (x+dx) store val s1 = person_set_y p (y+dy) s0 in

s1

end;;

(30)

HOL

形式では以下のように定義する．

val person_move =

Define ‘person_move p dx dy store =

let x = person_get_x p store in let y = person_get_y p store in

let s0 = person_set_x p (x+dx) store in let s1 = person_set_y p (y+dy) s0 in

s1 ‘;;

この定義の結果は以下のように表示される．

Definition has been stored under "person_move_def".

> val person_move =

|- !x y store.person_move p dx dy store = (let x = person_get_x p store in

let y = person_get_y p store in

let s0 = person_set_x p (x+dx) store in let s1 = person_set_y p (y+dy) s0 in

s1):thm

このようにして，ML形式の関数をすべて

HOL

形式に書き直す．

3.5.2 命題の設定

具体的な命題の作り方の例を挙げる．

HOL

上のオブジェクト指向理論では，システムの状態はストアで表現される．ストアに対する述語は，真理値を返す関数として記述できる．

例えば，「クラス

person

のオブジェクトが，座標

(1,1)

にいる」という述語

P personOn 1 1

は以下のように定義される．

val P_personOn_1_1=

Define ‘ P_personOn_1_1 p store =

let x = person_get_x p store in let y = person_get_y p store in

((x=1)/\(y=1))‘;;

この述語は，以下のような返り値を返す．

1.

ストア

s1

では，pの座標を

(1,1)

とすると

P personOn 1 1 p s1

は真となる．

(31)

2.

ストア

s2

では，pの座標を

(1,1)

以外とすると（例えば

(0,1)，(1,2)etc.）

P personOn 1 1 p s2

は偽となる．

また，証明の前提条件として，「store上に

p

が存在する」という述語

P exPerson

を以下のように定義する．

val P_exPerson =

Define‘ P_exPerson p store = person_ex p store‘;;

これらの述語を用いて命題を立てる．命題の例としては，以下のようものがかける．

! p store . (P_personOn_1_1 p store)/\

(P_exPerson p store) ==>

let newStore = person_move p 0 0 store in (P_personOn_1_1 p newStore)

これは，

「任意の

p store

に対し，

p

が

store

上に存在し，

p

が

(1,1)

にいるならば，

x

軸方向に

0，y

軸方向に

0

移動した後の

p

の位置は

(1,1)

である」

という命題である．

3.5.3 証明作業

ここでは，例としてあげた命題を実際に証明してみる．

まず，Goalの設定をする

g ‘! p store . (P_personOn_1_1 p store)/\

(P_exPerson p store) ==>

let newStore = person_move p 0 0 store in (P_personOn_1_1 p newStore) ‘;;

- - > val it =

Proof manager status: 1 proof.

1. Incomplete:

Initial goal:

!p store.

P_personOn_1_1 p store /\ P_exPerson p store ==>

(let newStore = person_move p 0 0 store in P_personOn_1_1 p newStore)

: proofs

(32)

これに対し，以下の

Tactics

を順に適用する．Tacticsの適用は，

この部分の証明手順と各

Tactics

の意味は，付録

D.1

に記述してある．

e (REPEAT GEN_TAC);;

e (LET_TAC);;

e (REWRITE_TAC [person_move]);;

e (LET_TAC);;

e (REWRITE_TAC [P_personOn_1_1]);;

e (LET_TAC);;

e (REWRITE_TAC [P_exPerson]);;

e (ROT_SLICE_TAC);;

e (OBJ_SIMP_TAC);;

e (RW_TAC arith_ss []);;

これにより，以下の結果が得られる．

> val it =

Initial goal proved.

|- !p store.

P_personOn_1_1 p store /\ P_exPerson p store ==>

(let newStore = person_move p 0 0 store in P_personOn_1_1 p newStore) : goalstack - -

以上により，Goalは証明された．証明された内容は，適当な名前をつけて，定理として利用できる．ここでは

lemma sample

と名づけるとする．

val lemma_sample = top_thm();;

drop();;

(33)

また，ここまでの処理は，

prove

というコマンドを用いて，まとめて以下のように書くこともできる．

val lemma_sample = prove

(‘‘! p store . (P_personOn_1_1 p store)/\

(P_exPerson p store) ==>

let newStore = person_move p 0 0 store in (P_personOn_1_1 p newStore) ‘‘,

EVERY

[REPEAT GEN_TAC, LET_TAC,

REWRITE_TAC [person_move], LET_TAC,

REWRITE_TAC [P_personOn_1_1], LET_TAC,

REWRITE_TAC [P_exPerson], ROT_SLICE_TAC,

OBJ_SIMP_TAC,

RW_TAC arith_ss []]);;

このように整理して保存しておき，必要なときに実行し，利用すると便利である．

組織内データセキュリティの定理証明による検証 に関する研究

JAIST Repository

修 士 論 文

組織内データセキュリティの定理証明による検証 に関する研究

徳田 拓

2006

3

修 士 論 文

組織内データセキュリティの定理証明による検証 に関する研究

片山 卓也 教授

片山 卓也 教授

二木 厚吉 教授

小川 瑞史 特任教授

410086 徳田 拓

2

目 次

1

1

1.1

. . . . 1

1.2

. . . . 2

1.3

. . . . 3

1.4

. . . . 4

1.4.1 ISO15408 . . . . 4

1.5

. . . . 5

1.5.1

. . . . 5

1.5.2

. . . . 6

1.6

. . . . 6

2

8 2.1

. . . . 8

2.1.1

. . . . 8

2.1.2

. . . . 8

2.2

. . . . 8

2.2.1

. . . . 9

2.2.2

. . . . 10

2.2.3

. . . . 10

3

13 3.1

. . . . 13

3.1.1

. . . . 13

3.1.2

. . . . 14

3.2 UML

. . . . 14

3.2.1 UML

. . . . 14

3.2.2

. . . . 14

3.2.3

UML

. . . . 15

3.3

. . . . 15

3.3.1

. . . . 16

3.3.2

. . . . 17

3.3.3

. . . . 17

3.3.4

. . . . 18

3.3.5

. . . . 20

3.4 ML

. . . . 20

組織内データセキュリティの定理証明による検証に関する研究

修士論文

組織内データセキュリティの定理証明による検証に関する研究

徳田拓

修士論文

組織内データセキュリティの定理証明による検証に関する研究

片山卓也教授

片山卓也教授

二木厚吉教授

小川瑞史特任教授

410086 徳田拓

目次