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

Slides:



Advertisements
Similar presentations
紹介担当: 石尾 隆(大阪大学) Q11.  Feature Model によって定義される「プロダクトの集合」 (プロダクトライン)の振舞いを検証する手法の拡張 ◦ 通常の振舞い検証: たとえば Promela を使って,1プロダクトの 振舞いを表現したオートマトンの取りうる状態遷移を調べる ◦
Advertisements

関心事指向アーキテクチャモデリング環 境 Concern-oriented Architecture Modeling Environment 九州工業大学大学院情報工学府 情報科学専攻 鵜林研究室 M1 佐藤 友紀 1.
プログラミング言語論 第10回(演習) 情報工学科 木村昌臣   篠埜 功.
最大エントロピーモデルに基づく形態素解析と辞書による影響
Webサービスに関する基本用語 Masatoshi Ohishi / NAOJ & Sokendai
XHTML構文検証手法における スクリプト要素の静的解析アルゴリズム
Riding the Design Wave II
プログラミング言語としてのR 情報知能学科 白井 英俊.
Brittany Jonson†, Yoonki Song†, Emerson Murphy-Hill†, Robert Bowdidge‡
Vanessa Lopez, Michele Pasin, and Enrico Motta
SSR 論文調査 Safety and Cyber-Physical Systems
報告 (2006/9/6) 高橋 慧.
疫学概論 メタアナリシス Lesson 21. 健康政策と疫学 §D. メタアナリシス S.Harano, MD,PhD,MPH.
情報伝播によるオブジェクト指向プログラム理解支援の提案
2005年11月17日 Webサービス II (第6回) 年11月17日.
F11: Analysis III (このセッションは論文2本です)
【ICSE2012 勉強会】 Recovering Links between an API and Its Learning Resources 担当 : 岩崎 慎司(NTTデータ)
2007/1/11 山下 諒蔵 佐藤 春旗 前田 俊行 大山 恵弘 佐藤 秀明 住井 英二郎
リファクタリングのための 変更波及解析を利用した テスト支援ツールの提案
Research Session 17: Formal Verification
動的スライスを用いたバグ修正前後の実行系列の差分検出手法の提案
分散処理を用いた大規模ソフトウェアに対するコーディングパターン検出ツール
日本語解析済みコーパス管理ツール 「茶器」
変更文の移動を可能にした 静的単一代入形式上の部分冗長性除去
第8章 Web技術とセキュリティ   岡本 好未.
静的情報と動的情報を用いた プログラムスライス計算法
コードクローンに含まれるメソッド呼び出しの 変更度合の分析
コードクローンに含まれるメソッド呼び出しの 変更度合の調査
組込みシステムの外部環境分析のためのUMLプロファイル
パケットキャプチャーから感染種類を判定する発見的手法について
IIR輪講復習 #10 XML retrieval
オーバレイ構築ツールキットOverlay Weaver
インラインスクリプトに対するデータフロー 解析を用いた XHTML 文書の構文検証
Java Bytecode Modification and Applet Security
プログラム動作理解支援を目的とした オブジェクトの振舞いの同値分割手法
ソフトウェア設計検証 研究室の紹介 知能情報学部 准教授 新田直也.
オープンソース開発支援のための ソースコード及びメールの履歴対応表示システム
ソースコードの特徴量を用いた機械学習による メソッド抽出リファクタリング推薦手法
オープンソース開発支援のための リビジョン情報と電子メールの検索システム
柔軟に変更可能な字句解析機構を持つ コードクローン検出ツールの開発
UMLモデルを対象とした リファクタリング候補検出の試み
コードクローン検出に基づくデザイン パターン適用支援手法の提案と実現
連続領域におけるファジィ制約充足問題の 反復改善アルゴリズムによる解法 Solving by heuristic repair Algorithm of the Fuzzy Constraint Satisfaction Problems with Continuous Domains 北海道大学.
ファジィ制約充足問題への 連続領域の導入 Introducing continuous domains to
バイトコードを単位とするJavaスライスシステムの試作
コードクローン分類の詳細化に基づく 集約パターンの提案と評価
Javaバーチャルマシンを利用した 動的依存関係解析手法の提案
コーディングパターンの あいまい検索の提案と実装
Managing non-functional uncertainty via model-driven adaptivity
静的情報と動的情報を用いた Javaプログラムスライス計算法
プログラムスライスを用いた凝集度メトリクスに基づく 類似メソッド集約候補の順位付け手法
アスペクト指向言語のための視点に応じた編集を可能にするツール
メソッドの同時更新履歴を用いたクラスの機能別分類法
1. サイバー攻撃の予兆となる社会データを収集 2. サイバー脅威を観測し、ビッグデータを形成 3. 異種ビッグデータから攻撃の全体像の解明
計算機プログラミングI 第4回 2002年10月31日(木) 問題解決とアルゴリズム クラスメソッドと手続きの抽象化 最大公約数
統合開発環境のための プログラミング言語拡張 フレームワーク
発表者: 稲葉 一浩 複雑ネットワーク・地図グラフ セミナー 2017/1/19
Eijiro Sumii and Naoki Kobayashi University of Tokyo
エイリアス関係を考慮した Javaプログラム用静的スライシングツール
複雑度メトリクスを用いた JAVAプログラム品質特性の実験的評価
コードクローン解析に基づく デザインパターン適用候補の検出手法
データの改竄を防ぐ仕組み 2002/9/12 牧之内研究室「インターネット実習」Webページ
オブジェクト指向言語における セキュリティ解析アルゴリズムの提案と実現
GluonJ を用いたビジネスロジックからのデータベースアクセスの分離
1.2 言語処理の諸観点 (1)言語処理の利用分野
信頼関係に基づくシステムセキュリティ の構造記述
Static Enforcement of Security with Types
Detecting Software Modularity Violations
プログラミング 2 静的変数.
Presentation transcript:

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

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) を利用

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

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 を再度行う

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  論文の貢献 : –OCL による security signatures の記述方法 –OCL で記述された scenario や metrics signature をチェックするためのメタモデル (system-security metamodel) –SDM (system description model) と SSM (security specification model) を提案

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

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