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