V. Security and Privacy 本資料は ICSE2013 の以下の 2 件の論文の要約です。 Automated Software Architecture Security Risk Analysis using Formalized Signatures Path Sensitive.

Presentation on theme: "V. Security and Privacy 本資料は ICSE2013 の以下の 2 件の論文の要約です。 Automated Software Architecture Security Risk Analysis using Formalized Signatures Path Sensitive."— Presentation transcript:

1 V. Security and Privacy 本資料は ICSE2013 の以下の 2 件の論文の要約です。 Automated Software Architecture Security Risk Analysis using Formalized Signatures Path Sensitive Static Analysis of Web Applications for Remote Code Execution Vulnerability Detection

2 V3: Path Sensitive Static Analysis of Web Applications for Remote Code Execution Vulnerability Detection  Background ： RCE (Remote Code Execution) は重大な問題である。 –OWASP によると PHP ではもっとも流行した問題である –XSS (Cross-site Scripting) の一種であるが、 stateful なアタックである – 文字列以外の値も扱う必要がある  Related work ： – 静的文字列解析があるが、 string constraint と non-string constraint の mixed constraint を 扱えないものが多い CFG-based のもの : path-sensitive ではない – いくつか mixed constraint を扱えるものがあるが、不十分である Symbolic execution ベース 文献 [12][25]: 実行パスに対して解析 & 固定の文字列長 Mixed constraint を一つの制約言語に変換 文献 [28]: non-string constraint に弱い 「 limited 」であると主張しているけど、具体的に扱えない例を出していない気がします。  Approach: – プログラムから string constraint / non-string constraint を区別して抽出し、 iterative かつ alternative な方法で解く  Contributions: –Context- and path-sensitive な静的解析であり、 string solver と SMT solver を用いる方 法 – プログラムを string / non-string な二つのサブプログラムへ分割して、それぞれの制約を 抽出し、これらの制約を同時に解く –10 個の Web アプリに適用し 21 個の RCE を発見した。そのうち 8 個は未報告のものだっ た！ – その他いろいろ工夫： stateful な部分、ファイルの動的 inclusion 、など  Evaluation: –LLVM を利用 (SSA 変換のため ) –STP (non-string constraint solver) と HAMPI (string constraint solver) を利用

3 脆弱性の例 脆弱性の要点： 1. config.inc.php には getConfigFile() から返る値を書き込む。 2. getConfigFile() では、 $_SESSION[“ConfigFile0”][“Servers”] のキーの値 $code が返る。 3. $code には、 arbitrary_php_script を記述できる。

4 Mixed 制約解消のアルゴリズム  前提 : –Loop は unroll する – プログラムを string と non-string の部分に分割し、それぞれの制約を N, P とする  手続き driver ： –N を STP solver で充足判定 UNSAT なら安全 (UNSAT) SAT の場合、解（充足する assignment ）を R とする –P を HAMPI で充足判定 UNSAT なら安全 (UNSAT) –P を R の条件で HAMPI で充足判定 SAT なら R を返す  手続き iterSolver : 再帰的な手続きで充足するパス（変数への割り当て）を探す –R が空なら S を返す (S は解 ) –R から一つずつ変数 b と値 bv を取り出して、 b=bv を S に加えて P を S の条件で充足判定し SAT なら、 b=bv を R から取り除いて interSolver を行う b!=bv のときの N の充足判定を行い、 UNSAT なら UNSAT を返す b!=bv のとき、 P についても同様に充足判定を行い、 UNSAT なら UNSAT を返す b!=bv を除外して、 interSolver を再度行う

5 V4: Automated Software Architecture Security Risk Analysis using Formalized Signatures  Background: 開発前におけるソフトウェアアーキテクチャのセキュリティ・レ ビューは重要である。 – アーキテクチャの評価には大きく分けて、シナリオベースとメトリクスベースのものが ある – セキュリティの評価においては、特定の事前定義されたルールによって行われる 攻撃シナリオによる評価 : セキュリティ上の要求や目的からシナリオを導出 Security metrics による評価 : 決まったものが実装されている  動機（扱う問題） : – アーキテクチャを解析するツールがない – アーキテクチャ評価基準を記述するための言語がない  アプローチ : –Attack scenario や security metrics / signature を OCL (Object Constraint Language) を 用いて記述し、 attack scenario や security metrics を求める – 脆弱性を OCL で書いてコード解析を行った研究の拡張 M. Almorsy, J. Grundy, and A. S. Ibrahim, "Supporting Automated Vulnerability Analysis using Formalized Vulnerability Signatures“, ASE, 2012, pp. 100-109.  論文の貢献 : –OCL による security signatures の記述方法 –OCL で記述された scenario や metrics signature をチェックするためのメタモデル (system-security metamodel) –SDM (system description model) と SSM (security specification model) を提案

6 Scenario と Metrics の例  Architecture Security Analysis Scenarios –CAPEC (Common Attack Pattern Enumeration and Classification) のパターン 例： Man-in-the-Middle, Denial of Service, Data Tampering, Injection  Architecture Security Metrics –System Architecture Security Metrics These metrics can be used to assess the exposure, exploitability, and attack-ability of the software system given its architecture, design, and may be code details. Attack Surface Metric, Compartmentalization Metric, Least Privilege Metric, Fail Securely Metric –Security Architecture Metrics Defense-In-Depth (Layered Security) Metric, Isolation Metric

7 評価方法  評価における問題 – アーキテクチャまで資料として残るプロジェクトの欠如  解決方法 –Manual でコードからアーキテクチャを復元 1 万～ 40 万行のオープンソースソフトウェア  結果 –Precision, recall, f-measure のいずれも 90% 前後で検出 – アーキテクチャ等を manual で作成しているので、やや bias がかかっていると思うが、メ タモデル (system-description model) に基づく OCL だけで、それだけ書けることが分かっ たことが重要（だと思う）