セキュリティ解析アルゴリズムの実現とオブジェクト

セキュリティ解析アルゴリズムの実現と
オブジェクト指向言語への適用に関する一考察
横森励士† 大畑文明† 高田喜朗‡
関浩之‡ 井上克郎†‡
†大阪大学大学院基礎工学研究科
‡奈良先端科学技術大学院大学情報科学研究科
2015/10/1
「ソフトウェアサイエンス研究会」
発表内容

背景





セキュリティ解析
情報フロー解析
情報フロー解析アルゴリズムの実装
オブジェクト指向言語に対する適用
まとめ・今後の課題
2015/10/1
「ソフトウェアサイエンス研究会」
研究の背景（1/2）

クレジットカード番号等，第三者に知られてはならない情報を扱うプ
ログラムにおいて不適切な情報漏洩を防ぐことは重要な課題である

Mandatory Access Control と呼ばれるアクセス制御法が情報漏洩
を防ぐ手段としてよく用いられる



2015/10/1
データに対してその機密度を表すセキュリティクラス（SC）を定義
データ dの SCをSC(d)
ユーザ（プロセス）に対してどの機密度のデータまでアクセス可能か
を表すクリアランス（Clearance）を定義
ユーザ u のクリアランスを clear(u)
ユーザ u は clear(u) ≧ SC(d) のときかつそのときのみデータ d を読
める
「ソフトウェアサイエンス研究会」
研究の背景（2/2）

Mandatory Access Control に基づいてシステムを構築する
場合，次のような形で引き起こされる情報漏洩を防ぐ必要
がある




データ dを読む権限を持つユーザプログラム Pがデータ dを読む
そのユーザプログラム Pがデータ dの情報を，それを読む権限
がないユーザ uでも読める記憶域 W に書き出す
u が W上にある d に関する情報を読めてしまう …. 漏洩
このような情報漏洩を防ぐため，静的な解析により情報フ
ローを抽出しプログラムの入力値のSCから出力値のSCを
求める，セキュリティ解析手法が提案されている
2015/10/1
「ソフトウェアサイエンス研究会」
情報フロー
情報フロー:
プログラム中の変数間に存在するデータ授受関係
•
•
explicit flow
• 文 sにおける変数 xの定義の際
に文 tで定義された変数 y の値
を参照
• x(s)← y(t)
implicit flow
• 文 t が分岐（繰り返し）命令でそ
の分岐節が文 sを含む
• t で参照される変数 y
• s で定義される変数 x
• x(s)← y(t)
2015/10/1
1:
2:
3:
4:
5:
例：
b = 5;
c = 5;
if ( c > 0 ){
a = b;
}

explicit flow a(4)← b(1)
implicit flow a(4) ←c(3)

「ソフトウェアサイエンス研究会」
情報フロー解析

情報フロー解析†：
プログラムの入力値のSCから出力値のSCを求める
 プログラムの入力となる値に対してSCを設定する
 各文内・文間における情報フローに基づき文実行
前後において各変数のSC間で成り立つべき再帰的
な関係式を定義する
 それらの関係式を同時に満たす最小解を繰り返し
計算により求め，出力値のSCを得る
†國信, 高田, 関, 井上 :``束構造のセキュリティモデルに基づくプログラムの情報フロー解析'',電
子情報通信学会技術研究報告,2000年11月.
2015/10/1
「ソフトウェアサイエンス研究会」
研究の目的
情報フロー解析はその提案だけでその実現については触れられ
ていない
１：情報フロー解析を実装し，適用事例をまじえながら有効性を検証
現在のプログラム開発環境において，Cなどの手続き型言語だけ
でなく，Java，C++等いわゆるオブジェクト指向言語の利用が高まっ
ている
２：オブジェクト指向プログラムへの情報フロー解析アルゴリズムの適用
2015/10/1
「ソフトウェアサイエンス研究会」
発表内容（解析アルゴリズムの実装）

解析アルゴリズムの実装
 実装の方針
 情報フロー解析
 セキュリティ解析ツール
 ツールの適用事例
2015/10/1
「ソフトウェアサイエンス研究会」
実装の方針

解析対象言語： Pascalのサブセット


SCは二値で表す



ポインタや構造体には非対応
high: 機密度の高い情報を持っている
low: 機密度の低い情報しか持っていない
解析は2つのフェーズで構成

Phase 1: 前提条件の入力


Phase 2: 情報フロー解析


2015/10/1
プログラムの入力となる値に対してSCを設定
前提条件を元に情報フローを計算しながらプログラム中の各出
力文におけるSCを求める
繰り返し計算中に情報フローを逐次求め計算を行なう
「ソフトウェアサイエンス研究会」
Phase 2: 情報フロー解析（1/2）

手続き間解析の効率化



各手続き内部の解析結果は引数のSCの最小上界を入力とした結果
実利用においてはその時点での最小上界に対する結果のみを残す
大域変数への対応

大域変数は
 手続き呼び出し先に対する，仮想的な引数
 手続き呼び出し元に対する，仮想的な戻り値
として扱う

セキュリティ解析の前に各手続きで直接もしくは間接的に定義，
参照される大域変数を調べ，必要なだけの仮想的な引数（戻り
値）を用意する
2015/10/1
「ソフトウェアサイエンス研究会」
Phase 2: 情報フロー解析（2/2）

すべての手続きの解析結果が安定するまで，手続きを
繰り返し解析する



解析リスト（手続き呼び出し経路に基づく，手続きの解析順リ
スト）を用意
解析リストが空になった時点で解析を終了
手続きの解析




各手続きの解析前に局所変数，仮引数，参照されうる大域変
数からセキュリティクラス集合（Security Class Set，SCset）を用
意
SCsetの要素: (変数, SC)の組
手続き内の先頭の文からプログラムの実行順に従い，文の種
類に応じた解析アルゴリズムに基づき SCset を逐次更新する
手続き呼び出し文の解析時や手続きの解析の終了時には他
の手続きに情報を流し，必要に応じて解析リストを更新する
2015/10/1
「ソフトウェアサイエンス研究会」
情報フロー解析の例
1: program sample;
2: var a : integer;
3: …
4: function f(x :integer) :integer;
5: (* a,x ←low *)
6: var y : integer;
7: begin
8:
readln(y);( ←high *)
9:
a := y + a + 1;
10:
writeln(y);
11:
f := x + 1;
12: end
13: …
14: end.
2015/10/1
SCset={(a,low),(x,low),(y,low)}
SCset={(a,low),(x,low),(y,high)}
SCset={(a,high),(x,low),(y,high)}
出力文にhighを登録
SCset={(a,high),(x,low),(y,high),(f,low)}
「ソフトウェアサイエンス研究会」
セキュリティ解析ツール

ツールの実現:



スライスツールであるOsaka Slicing Systemに機能追加の形で
実現
追加部分は C で約1000行
解析手順:
1
2
3
4
2015/10/1
構文解析，意味解析
解析の前提条件を設定
前提条件を基にセキュリティ解析
SCの高い文を強調表示
「ソフトウェアサイエンス研究会」
ツールの適用事例（1/2）
ツールの利用目的: プログラムの安全性の確認


SCの高い出力を事前検出することで想定外の情報漏洩を防ぐ
SCの高い出力文を減らすことで情報漏洩の可能性を低くする
適用事例: チケットの予約システム


クレジットカードの認証を行なうモジュールが組み込まれている
クレジットカード番号に関する入力に高いSCを与えて解析
適用対象: 実装方針が異なる二つのプログラムに対し解析
A カード番号の認証が成功した後に予約処理を行なう
B 予約処理が成功した後にカード番号の認証を行なう
2015/10/1
「ソフトウェアサイエンス研究会」
ツールの適用事例（2/2）
解析結果:
[A] システム全体の35／36の出力文が高いSCを持つ
予約処理モジュールの出力文も含む
[B] システム全体の13／36の出力文が高いSCを持つ
クレジットカード認証に関する出力文のみ
予約処理モジュールの出力文は高いSCを持たない
考察:
[A ] カード番号から予約処理への情報フローが存在
「予約処理」が行なわれることで「与えられたカード
番号が認証される」ことが判明
[B] カード番号から予約処理への情報フローがない
実装の方法によって情報の流れは大きく変わるため
情報フロー解析による安全性の確認は重要
2015/10/1
「ソフトウェアサイエンス研究会」
カード番号
A
成功
認証
予約処理
成功
予約通知
失敗
決済失敗通知
失敗
失敗通知
ツールの適用事例（2/2）
解析結果:
[A] システム全体の35／36の出力文が高いSCを持つ
予約処理モジュールの出力文も含む
[B] システム全体の13／36の出力文が高いSCを持つ
クレジットカード認証に関する出力文のみ
予約処理モジュールの出力文は高いSCを持たない
考察:
[A ] カード番号から予約処理への情報フローが存在
「予約処理」が行なわれることで「与えられたカード
番号が認証される」ことが判明
[B] カード番号から予約処理への情報フローがない
実装の方法によって情報の流れは大きく変わるため
情報フロー解析による安全性の確認は重要
2015/10/1
「ソフトウェアサイエンス研究会」
B
予約処理
成功
失敗
成功通知
認証
成功
決済通知
失敗通知
カード番号
失敗
決済失敗通知
発表内容
（オブジェクト指向プログラムへの適用）
オブジェクト指向プログラムへの情報フロー
解析アルゴリズムの適用



2015/10/1
インスタンスに関する問題とその対策
インスタンス自身の SCと属性の SCの関連
についての考察および定義規則の提案
（オーバーライドに関する問題とその対策）
「ソフトウェアサイエンス研究会」
オブジェクト指向言語に対する適用
現在のプログラム開発環境において，Cなどの手続き型言語だけで
なくJava，C++等いわゆるオブジェクト指向言語の利用が高まっている
オブジェクト指向プログラムへの情報フロー解析アルゴリズムの適用
手続き型言語には無い，オブジェクト指向言語に特有の新しい概念
が存在するため，既存のアルゴリズムをそのまま適用すると様々な問
題が生じる
クラス（Class）
インスタンス（Instance）
継承（Inheritance）
それらの問題点を考察・対策手法を提案
2015/10/1
「ソフトウェアサイエンス研究会」
インスタンスに関する問題（1/2）
問題点:クラスのインスタンスは一般に複数存在するため，クラス単
位で解析を行なう場合，同一クラスのインスタンス間で情報が共有さ
れるため，解析結果がインスタンスが持つSCの上界となる
System.out.println(x.test_())
では高い SC の情報を出力

System.out.println(y.test_())
では低い SC の情報を出力

クラス単位の解析では
Base 内の test()，test_()，
valueに対する解析結果を共
有しなければならないため
System.out.println(y.test_())
で SC の高い情報を出力と判定

2015/10/1
class Base {
protected String value;
public void test(String v) { value = v; }
public String test_(){ return(value); }
}
class Sample {
protected String value;
public static void main(String[] args) {
Base x = new Base();
Base y = new Base();
x.test(args[0]); // args[0] ← high
System.out.println(x.test_());
y.test(args[1]); // args[1] ← low
System.out.println(y.test_());
}
}
「ソフトウェアサイエンス研究会」
インスタンスに関する問題（2/2）
対策: セキュリティ解析をインスタンス単位で行なう
属性のSCをインスタンス単位で保
持し，メソッドに対する解析もインス
タンスそれぞれに対して行なう


x.valueとy.valueのSCを区別して
保存
Base 内の test()，test_()に対する
解析も x,y それぞれのインスタ
ンス別に行なう
System.out.println(y.test_())でSC
の低い情報を出力と判定できる
2015/10/1
class Base {
protected String value;
public void test(String v) { value = v; }
public String test_(){ return(value); }
}
class Sample {
protected String value;
public static void main(String[] args) {
Base x = new Base();
Base y = new Base();
x.test(args[0]); // args[0] ← high
System.out.println(x.test_());
y.test(args[1]); // args[1] ← low
System.out.println(y.test_());
}
}
「ソフトウェアサイエンス研究会」
インスタンス自身のSCに関する考察
手続き型プログラムにおいて全ての変数に対して SCを設定して解析
していたことを考えると，オブジェクト指向プログラムに対して適用する
場合にはインスタンス自身のSCについても考慮しなければならない
基本方針 :
「インスタンス自身のSCは，
インスタンス属性のSC
インスタンスメソッドの存在およびそれらに渡される実引数のSC
により決定される」
インスタンス自身の SC の利用例 :
インスタンス自身のSCは属性の SC の情報を集約したものとなるため
「自分以外のクラスに対してはインスタンスの属性のSCを持たずに，
インスタンス自身のSCを解析に利用する」ことで解析を効率化できる
2015/10/1
「ソフトウェアサイエンス研究会」
定義規則
規則1: インスタンス属性に代入される SC やメソッドの実引
数のSC の最小上界
最も実現が容易であるが，属性値を操作しないメソッドの影響を受
けやすくインスタンス自身のSCが高くなりやすい
規則2: インスタンス属性が持つ SCの最小上界
各メソッドにおいて，引数とインスタンス属性間の情報フローの把握
が必要であるが，インスタンス属性に影響を与えない実引数のSC
を計算対象から排除できる
規則3: 外部に参照されうる可能性のあるインスタンス属性
が持つSCの最小上界
どの属性の情報が（メソッドを介して）外部に流れるかの把握が必
要であるが，インスタンスの外部に情報が流れない属性を計算対
象から排除できる
2015/10/1
「ソフトウェアサイエンス研究会」
定義規則の適用例
規則1: 代入される SC やメソッドの実
引数のSC の最小上界
赤い部分全てがhigh
規則2:
文x.test(args[0])でのA::test()では
A::valueの SC は lowのままであるた
めx が指すインスタンスのSCはlow
青くなる部分がlowとなる
規則3:
文 y.test(args[0]) での B::test()では
属性B::valueのSC はhigh であるが，
値が外部から取り出されないため
yが指すインスタンスのSCはlow
さらに青くなる部分がlowとなる
2015/10/1
class A{
private String value;
public void test(String v) { value =
nil; }
}
class B{
private String value;
public void test(String v) { value= v; }
}
class Sample {
public static void} main(String[] args) {
A x = new A();
B y = new B();
x.test(args[0]); // args[0] ←high
y.test(args[0]);
}
}
「ソフトウェアサイエンス研究会」
定義規則の適用例
規則1:
赤い部分全てがhigh
規則2:属性が持つ SCの最小上界
文x.test(args[0])でのA::test()では
A::valueの SC は lowのままであるため
x が指すインスタンスのSCはlow
青くなる部分がlowとなる
規則3:
文 y.test(args[0]) での B::test()では属
性B::valueのSC はhigh であるが，値が
外部から取り出されないため yが指す
インスタンスのSCはlow
さらに青くなる部分がlowとなる
2015/10/1
class A{
private String value;
public void test(String v) { value =
nil; }
}
class B{
private String value;
public void test(String v) { value= v; }
}
class Sample {
public static void} main(String[] args) {
A x = new A();
B y = new B();
x.test(args[0]); // args[0] ←high
y.test(args[0]);
}
}
「ソフトウェアサイエンス研究会」
定義規則の適用例
規則1:
赤い部分全てがhigh
規則2:
文x.test(args[0])でのA::test()では
A::valueの SC は lowのままであるた
めx が指すインスタンスのSCはlow
青くなる部分がlowとなる
規則3:外部に参照されうる属性が持つ
SCの最小上界
文 y.test(args[0]) での B::test()では
属性B::valueのSC はhigh であるが，
値が外部から取り出されないため
y が指すインスタンスのSCはlow
青くなる部分がさらにlowとなる
2015/10/1
class A{
private String value;
public void test(String v) { value =
nil; }
}
class B{
private String value;
public void test(String v) { value= v; }
}
class Sample {
public static void} main(String[] args) {
A x = new A();
B y = new B();
x.test(args[0]); // args[0] ←high
y.test(args[0]);
}
}
「ソフトウェアサイエンス研究会」
解析結果の精度と計算コスト
オブジェクト指向プログラムへの情報フロー解析アルゴ
リズム適用における問題点に関する対策を提案
これらの対策を適用することで
解析結果の精度が向上するが
計算コストの増大が避けられない
解析結果の精度と計算コストはトレードオフの関係
実利用においては手法の比較検討が必要
2015/10/1
「ソフトウェアサイエンス研究会」
まとめ

手続き型言語に対するセキュリティ解析
手法を実装し適用事例をまじえながら有
効性を検証

オブジェクト指向プログラムへのセキュリ
ティ解析アルゴリズムの適用について問
題点を考察しそれに対する対処法を提案
2015/10/1
「ソフトウェアサイエンス研究会」
今後の課題

オブジェクト指向言語に対するセキュリティ解析
アルゴリズムの実装
対象言語として JAVA を想定して実装予定

解析アルゴリズムの違いによる，精度とコストの
トレードオフ関係の検証
2015/10/1
「ソフトウェアサイエンス研究会」

Download Report