オブジェクト指向言語における セキュリティ解析アルゴリズムの提案と実現 横森 励士 井上研究室

研究の背景 (1/2) クレジットカード番号等、第三者に知られてはならない情報を扱うプログラムにおいて、不適切な情報漏洩を防ぐことは重要な課題 情報漏洩を防ぐアクセス制御法 アクセス アクセス不可 機密情報 x ……….. アクセス アクセス 公開情報 z ……….. 管理者 ユーザ secret public システム 修士論文発表会

研究の背景 (2/2) プログラムによって引き起こされる情報漏洩 プログラムによって引き起こされる情報漏洩を検出する、セキュリティ解析手法が提案されている アクセス (間接)アクセス 情報漏洩 アクセス不可 機密情報 x ……….. プログラムp ………… readln(x); writeln(x); アクセス アクセス 公開情報 z ……….. x ……….. 管理者 ユーザ secret public システム 修士論文発表会

研究の目的 セキュリティ解析手法は手続き型言語における手法の提案だけで、実現方法には触れていない 現在のプログラム開発環境では、C などの手続き型言語だけでなく、Java や C++ 等のオブジェクト指向言語の利用が高まっている オブジェクト指向プログラムにおける セキュリティ解析手法の提案と実現 修士論文発表会

情報フロー解析 静的な解析により情報フローを抽出し、プログラムの入力値のセキュリティクラスから出力値のセキュリティクラスを求めるセキュリティ解析手法 情報フロー プログラム中の変数間に存在するデータ授受関係 セキュリティクラス データの持つ機密度を束構造で表現したもの 修士論文発表会

情報フロー (Information Flow) プログラム中の変数間に存在するデータ授受関係 explicit flow 変数の定義・参照間に存在 implicit flow 分岐(繰り返し)命令の条件節と内部の文の間に存在 1: b = 5; 2: c = 5; 3: if ( c > 0 ) { 4: a = b; 5: } 修士論文発表会

セキュリティクラス (Security Class) データの持つ機密度を束構造で表現したもの(以下、SC) SC における演算 和: SC の最小上界 (例: low ＋ high = high) 積: SC の最大下界 (例: low × high = low) 以降、SC を { high, low } の二値で表現 high: 保護すべき情報 low: 保護する必要のない情報 修士論文発表会

情報フロー解析の例 情報フローを元に、プログラムの各地点における 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: } 修士論文発表会

情報フロー解析アルゴリズム† 連立方程式の繰り返し計算に基づく解析 プログラムの入力値に対して SC を設定 †國信, 高田, 関, 井上 :``束構造のセキュリティモデルに基づくプログラムの情報フロー解析'',電子情報通信学会技術研究報告,2000年11月 修士論文発表会

情報フロー解析アルゴリズムの実現 データフロー方程式に基づく解析 データフロー方程式 プログラム文の定義・参照変数に関する集合演算 プログラム文間の変数を介したデータの流れを抽出 SC の集合である SCset および その更新アルゴリズムを文の種類に応じて定義 SCset: 解析中に参照される変数が持つ SC の集合 解析手順 プログラムの入力値に対して SC を設定 プログラム文の実行順に従い、逐次 SCset を更新し、出力値の SC を得る

解析例 メソッドSample.Test()内の解析 解析前にクラスのメンバ変数、仮引数からSCsetを構築 実行順に従い解析 SCset = { (Y, 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); 実行順に従い解析 SCset = { (Y, high) } SCset = { (Y, high), （X, { (value, low) } ) } (文Base X = new Base(); 解析後) 呼び出し先のメソッドを解析 SCset = { (Y, high), （X, { (value, low) } ) } SCset = { (ｖ, high), （value, low) } (文X.mA();解析前) 出力文では参照している変数のSCを求める SCset = { (Y, high), （X, { (value, high) } ) } 文System.out.println(X.value);のSCはhigh 修士論文発表会

オブジェクト指向言語への対応 オブジェクト指向言語へ拡張する際に考慮すべき点 オーバーライドへの対応 クラス単位の解析から、インスタンス単位への解析への拡張 インスタンス属性の SC から、インスタンスの SC を導出する規則の定義 修士論文発表会

オーバーライドへの対応 メソッド呼び出し文単体では、 呼び出すメソッドを特定できない class Base { protected String value; public void mA(String v) { System.out.println(v); } class Derived extends Base { value = v; class Sample { public static void Test() { String Y = “high”; ← high Base X = new Derived(); X.mA(Y); メソッド呼び出し文単体では、 呼び出すメソッドを特定できない 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 { value = v; class Sample { public static void Test() { String Y = “high”; ← high Base X = new Derived(); X.mA(Y); 参照変数の指すインスタンスの型を特定する 参照変数ごとに、それが指すインスタンスが取りうる型についての情報を保持する X は Derived クラスのインスタンスを指している X.mA() の実体は Derived クラスの mA() メソッド呼び出し文の解析対象となるメソッドを限定可能 修士論文発表会

セキュリティ解析ツール 対象言語: Java C++ で記述 (約5500行) オーバーライドへの対応を実現 入力文: 「java.io.* 中の入力メソッド」を呼び出す文 出力文: 「java.io.* 中の出力メソッド」を呼び出す文 C++ で記述 (約5500行) Javaの構文解析、意味解析ライブラリを利用 オーバーライドへの対応を実現 修士論文発表会

適用例 (事例紹介) チケットの予約システム (500行) クレジットカード番号の認証を行うモジュールが組み込まれている クレジットカード番号に関する入力に高い SC を与えて解析を行う 決済失敗 通知 認証 予約処理 成功 失敗 失敗通知 予約通知 カード番号 修士論文発表会

適用例 (解析結果) 36 行の出力文中、35行が高い SC を持つことが判明 カード番号から予約処理への情報フローが存在する 予約処理が行われることで、カード番号の認証が行われたことが判明 決済失敗 通知 認証 予約処理 成功 失敗 失敗通知 予約通知 カード番号 決済失敗 通知 認証 予約処理 成功 失敗 失敗通知 予約通知 カード番号 修士論文発表会

適用例 (対策) 予約処理が成功した後にカード番号の認証を行う カード番号から予約処理への情報フローが消滅したことがわかる 認証に関する出力文の SC のみ高い SC を持つ (13 行) 予約処理モジュールの出力文の SC は低い カード番号から予約処理への情報フローが消滅したことがわかる 決済失敗 通知 認証 予約処理 成功 失敗 失敗通知 予約通知 カード番号 成功通知 決済失敗 通知 認証 予約処理 成功 失敗 失敗通知 予約通知 カード番号 成功通知 修士論文発表会

まとめ オブジェクト指向プログラムにおけるセキュリティ解析手法を提案し、ツールの試作を行った データフロー方程式に基づいた解析アルゴリズム 情報フローとセキュリティクラス データフロー方程式に基づく解析 解析アルゴリズムのオブジェクト指向言語への拡張 3つの考慮すべき点について考察 オーバーライドへの対応を実現 セキュリティ解析ツールの実現 Java を対象 プログラムの安全性確認への有効性を検証した 修士論文発表会

研究計画 (1/2) 情報フロー解析に基づくセキュリティ解析手法に関する研究 オブジェクト指向言語への拡張の実現 オーバーライドへの対応 クラス単位の解析から、インスタンス単位の解析への拡張 インスタンス属性の SC から、インスタンスの SC を導出する規則の定義 修士論文発表会

研究計画 (2/2) 動的解析によるセキュリティ解析手法の実現 現在の手法はソースプログラムに対する静的な解析 すべての経路が実行されうると仮定 implicit flow が強すぎるため、条件節で参照される変数の SC が分岐先へ大きく影響を与える 実行履歴に対する解析を行う 実際に起こりえない実行経路や情報フローを解析対象から除外 条件節での implicit flow を分岐先ごとに区別することにより、 implicit flow の影響を抑える 修士論文発表会