Document

オブジェクト指向言語における
セキュリティ解析アルゴリズムの提案と実現
横森励士
井上研究室
Software Engineering Research Group, Graduate School of Engineering Science, Osaka University
研究の背景 (1/2)
クレジットカード番号等、第三者に知られてはならな
い情報を扱うプログラムにおいて、不適切な情報漏
洩を防ぐことは重要な課題
情報漏洩を防ぐアクセス制御法
アクセス
機密情報
x ………..
アクセス不可
アクセス
公開情報
アクセス
管理者
secret
z ………..
システム
ユーザ
public
2
修士論文発表会
Software Engineering Research Group, Graduate School of Engineering Science, Osaka University
研究の背景 (2/2)
プログラムによって引き起こされる情報漏洩
アクセス
アクセス
管理者
secret
機密情報
x ………..
アクセス不可
(間接)アクセス
公開情報
x ………..
z ………..
アクセス
プログラムp
…………
readln(x);
情報漏洩
writeln(x);
システム
ユーザ
public
プログラムによって引き起こされる情報漏洩を検出する、
セキュリティ解析手法が提案されている
3
修士論文発表会
Software Engineering Research Group, Graduate School of Engineering Science, Osaka University
研究の目的
セキュリティ解析手法は手続き型言語における手法
の提案だけで、実現方法には触れていない
現在のプログラム開発環境では、C などの手続き型
言語だけでなく、Java や C++ 等のオブジェクト指
向言語の利用が高まっている
オブジェクト指向プログラムにおける
セキュリティ解析手法の提案と実現
4
修士論文発表会
Software Engineering Research Group, Graduate School of Engineering Science, Osaka University
情報フロー解析
静的な解析により情報フローを抽出し、プログラムの
入力値のセキュリティクラスから出力値のセキュリティク
ラスを求めるセキュリティ解析手法
情報フロー
プログラム中の変数間に存在するデータ授受関係
セキュリティクラス
データの持つ機密度を束構造で表現したもの
5
修士論文発表会
Software Engineering Research Group, Graduate School of Engineering Science, Osaka University
情報フロー (Information Flow)
プログラム中の変数間に存在するデータ授受関係
explicit flow
変数の定義・参照間に存在
implicit flow
分岐(繰り返し)命令の条件節と内部の文の間に存在
1:
2:
3:
4:
5:
b = 5;
c = 5;
if ( c > 0 ) {
a = b;
}
6
修士論文発表会
Software Engineering Research Group, Graduate School of Engineering Science, Osaka University
セキュリティクラス (Security Class)
データの持つ機密度を束構造で表現したもの(以下、
SC)
SC における演算
和: SC の最小上界 (例: low ＋ high = high)
積: SC の最大下界 (例: low × high = low)
以降、SC を { high, low } の二値で表現
high: 保護すべき情報
low: 保護する必要のない情報
7
修士論文発表会
Software Engineering Research Group, Graduate School of Engineering Science, Osaka University
情報フロー解析の例
情報フローを元に、プログラムの各地点における SC を
求める
1: void method(int a ,int b, int c) {
2: int d = a + b + c;
3: if ( c > 0 ) {
4:
a = b;
5: }
6: printf(“%s\n”, a);
7: }
8
修士論文発表会
Software Engineering Research Group, Graduate School of Engineering Science, Osaka University
†
情報フロー解析アルゴリズム
連立方程式の繰り返し計算に基づく解析
プログラムの入力値に対して SC を設定
各文内・文間における情報フローに基づき、文実行前
後において各変数の SC 間で成り立つべき、再帰的な
関係式を定義する
再帰的な関係式を同時に満たす最小解を繰り返し計
算によって求め、出力値の SC を得る
†國信,
高田, 関, 井上 :``束構造のセキュリティモデルに基づくプログラムの情報フロー解析'',
電子情報通信学会技術研究報告,2000年11月
9
修士論文発表会
Software Engineering Research Group, Graduate School of Engineering Science, Osaka University
情報フロー解析アルゴリズムの実現
データフロー方程式に基づく解析
データフロー方程式
プログラム文の定義・参照変数に関する集合演算
プログラム文間の変数を介したデータの流れを抽出
SC の集合である SCset およびその更新アルゴリズムを
文の種類に応じて定義
SCset: 解析中に参照される変数が持つ SC の集合
解析手順
プログラムの入力値に対して SC を設定
プログラム文の実行順に従い、逐次 SCset を更新
し、出力値の SC を得る
10
Software Engineering Research Group, Graduate School of Engineering Science, Osaka University
解析例
メソッドSample.Test()内の解析
解析前にクラスのメンバ変数、仮
実行順に従い解析
呼び出し先のメソッドを解析
引数からSCsetを構築
出力文では参照している変数の
SCを求める
SCset
=={ (Y,
high)
}
SCset
{
(Y,
high),
SCset = { (Y, high) }
（X,SCset
{ (value,
low)high),
})}
= { (Y,
SCset = { (Y, high),
（X, { (value, high) } ) }
（X, { =(value,
low) }（value,
)}
SCset
{ (ｖ, high),
(文Base X = newlow)
Base();
} 解析後)
文System.out.println(X.value);
(文X.mA();解析前)
のSCはhigh
class Base {
public String value;
public void mA(String v) {
v = value;
}
}
class Sample {
Y ← high
public static void Test(String Y) {
Base X = new Base();
X.mA(Y);
System.out.println(X.value);
}
}
11
修士論文発表会
Software Engineering Research Group, Graduate School of Engineering Science, Osaka University
オブジェクト指向言語への対応
オブジェクト指向言語へ拡張する際に考慮すべき点
オーバーライドへの対応
クラス単位の解析から、インスタンス単位への解析への
拡張
インスタンス属性の SC から、インスタンスの SC を導出
する規則の定義
12
修士論文発表会
Software Engineering Research Group, Graduate School of Engineering Science, Osaka University
オーバーライドへの対応
メソッド呼び出し文単体では、
呼び出すメソッドを特定できない
X.mA(Y) を正しく解析するため
には、Base クラスの派生クラス
のメソッドについても考慮する必
要がある
X.mA() の実体は?
Base クラスの mA()
Derived クラスの mA()
class Base {
protected String value;
public void mA(String v) {
System.out.println(v);
}
}
class Derived extends Base {
public void mA(String v) {
value = v;
System.out.println(v);
}
}
class Sample {
public static void Test() {
String Y = “high”; ← high
Base X = new Derived();
X.mA(Y);
}
}
13
修士論文発表会
Software Engineering Research Group, Graduate School of Engineering Science, Osaka University
オーバーライドへの対応
参照変数の指すインスタンスの型を
特定する
参照変数ごとに、それが指すイ
ンスタンスが取りうる型について
の情報を保持する
X は Derived クラスのイン
スタンスを指している
X.mA() の実体は Derived
クラスの mA()
メソッド呼び出し文の解析対象
となるメソッドを限定可能
class Base {
protected String value;
public void mA(String v) {
System.out.println(v);
}
}
class Derived extends Base {
public void mA(String v) {
value = v;
System.out.println(v);
}
}
class Sample {
public static void Test() {
String Y = “high”; ← high
Base X = new Derived();
X.mA(Y);
}
}
14
修士論文発表会
Software Engineering Research Group, Graduate School of Engineering Science, Osaka University
セキュリティ解析ツール
対象言語: Java
入力文: 「java.io.* 中の入力メソッド」を呼び出す文
出力文: 「java.io.* 中の出力メソッド」を呼び出す文
C++ で記述 (約5500行)
Javaの構文解析、意味解析ライブラリを利用
オーバーライドへの対応を実現
15
修士論文発表会
Software Engineering Research Group, Graduate School of Engineering Science, Osaka University
適用例 (事例紹介)
チケットの予約システム (500行)
クレジットカード番号の認証を行
うモジュールが組み込まれている
クレジットカード番号に関する入
力に高い SC を与えて解析を
行う
カード番号
認証
成功
失敗
予約処理決済失敗
通知
成功
失敗
予約通知失敗通知
16
修士論文発表会
Software Engineering Research Group, Graduate School of Engineering Science, Osaka University
適用例 (解析結果)
36 行の出力文中、35行が高い
SC を持つことが判明
予約モジュールの出力文も高い
SC を持つことが判明
カード番号から予約処理への
情報フローが存在する
予約処理が行われることで、カー
ド番号の認証が行われたことが
判明
カード番号
認証
成功
失敗
予約処理決済失敗
通知
成功
失敗
予約通知失敗通知
17
修士論文発表会
Software Engineering Research Group, Graduate School of Engineering Science, Osaka University
適用例 (対策)
予約処理が成功した後にカード
番号の認証を行う
認証に関する出力文の SC の
み高い SC を持つ (13 行)
予約処理モジュールの出力文
の SC は低い
カード番号から予約処理への情
報フローが消滅したことがわかる
予約処理
成功
失敗
成功通知失敗通知
認証
成功
カード番号
失敗
決済失敗
予約通知
通知
18
修士論文発表会
Software Engineering Research Group, Graduate School of Engineering Science, Osaka University
まとめ
オブジェクト指向プログラムにおけるセキュリティ解析手
法を提案し、ツールの試作を行った
データフロー方程式に基づいた解析アルゴリズム
情報フローとセキュリティクラス
データフロー方程式に基づく解析
解析アルゴリズムのオブジェクト指向言語への拡張
3つの考慮すべき点について考察
オーバーライドへの対応を実現
セキュリティ解析ツールの実現
Java を対象
プログラムの安全性確認への有効性を検証した
19
修士論文発表会
Software Engineering Research Group, Graduate School of Engineering Science, Osaka University
研究計画 (1/2)
情報フロー解析に基づくセキュリティ解析手法に関す
る研究
オブジェクト指向言語への拡張の実現
オーバーライドへの対応
クラス単位の解析から、インスタンス単位の解析への
拡張
インスタンス属性の SC から、インスタンスの SC を導
出する規則の定義
20
修士論文発表会
Software Engineering Research Group, Graduate School of Engineering Science, Osaka University
研究計画 (2/2)
動的解析によるセキュリティ解析手法の実現
現在の手法はソースプログラムに対する静的な解析
すべての経路が実行されうると仮定
implicit flow が強すぎるため、条件節で参照される
変数の SC が分岐先へ大きく影響を与える
実行履歴に対する解析を行う
実際に起こりえない実行経路や情報フローを解析対
象から除外
条件節での implicit flow を分岐先ごとに区別する
ことにより、 implicit flow の影響を抑える
21
修士論文発表会
Software Engineering Research Group, Graduate School of Engineering Science, Osaka University

Download Report