| 講演名 | 2017-03-09 モデル計数を用いた量的情報流解析のための論理式簡約と静的解析 中島 聖斗(名大), 橋本 健二(名大), 酒井 正彦(名大), 関 浩之(名大), |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | プログラムの量的情報流（QIF）解析手法の一つとして，プログラムを背景理論付き論理式へ変換しプログラムの出力値を表す論理変数集合に投射したモデル計数（#SMT）に帰着する方法がある．本稿では，QIF解析の際に用いられる#SMTツールの高速化を目指し，モデル計数における出力候補値の探索空間を小さくする手法として，失敗リテラル検査による論理式簡約を行う手法とプログラムの抽象解釈による静的解析に基づく手法の二つを提案し，それらの有効性を実験的に評価する． |
| 抄録(英) | Model counting is one of the promising methods for quantitative information flow analysis. In this paper, we focus on the model counting of the formula modulo theories (#SMT) obtained from a given program. To improve the efficiency of the model counting, we propose two preprocessing methods that make the search space smaller and experimentally evaluate the methods. One is the logical formula simplification based on failed literal probing and the other one is the static analysis of a program based on abstract interpretation. |
| キーワード(和) | 量的情報流 / 投射モデル計数 / SMT / FLP / 抽象解釈 |
| キーワード(英) | quantitative information flow / projected model counting / SMT / FLP / abstract interpretation |
| 資料番号 | SS2016-61 |
| 発行日 | 2017-03-02 (SS) |
| 研究会情報 | |
| 研究会 | SS |
|---|---|
| 開催期間 | 2017/3/9(から2日開催) |
| 開催地（和） | てんぶす那覇 |
| 開催地（英） | |
| テーマ（和） | 一般 |
| テーマ（英） | |
| 委員長氏名（和） | 緒方 和博(北陸先端大) |
| 委員長氏名（英） | Kazuhiro Ogata(JAIST) |
| 副委員長氏名（和） | 中田 明夫(広島市大) |
| 副委員長氏名（英） | Akio Nakata(Hiroshima City Univ.) |
| 幹事氏名（和） | 小林 隆志(東工大) / 肥後 芳樹(阪大) |
| 幹事氏名（英） | Takashi Kobayashi(Tokyo Inst. of Tech.) / Yoshiki Higo(Osaka Univ.) |
| 幹事補佐氏名（和） | 島 和之(広島市大) |
| 幹事補佐氏名（英） | Kazuyuki Shima(Hiroshima City Univ.) |
| 講演論文情報詳細 | |
| 申込み研究会 | Technical Committee on Software Science |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | モデル計数を用いた量的情報流解析のための論理式簡約と静的解析 |
| サブタイトル（和） | |
| タイトル（英） | Logical Formula Simplification and Static Analysis for Quantitative Information Flow Analysis using Model Counting |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 量的情報流 / quantitative information flow |
| キーワード(2)（和/英） | 投射モデル計数 / projected model counting |
| キーワード(3)（和/英） | SMT / SMT |
| キーワード(4)（和/英） | FLP / FLP |
| キーワード(5)（和/英） | 抽象解釈 / abstract interpretation |
| 第 1 著者 氏名（和/英） | 中島 聖斗 / Masato Nakashima |
| 第 1 著者 所属（和/英） | 名古屋大学(略称：名大) Nagoya University(略称：Nagoya Univ.) |
| 第 2 著者 氏名（和/英） | 橋本 健二 / Kenji Hashimoto |
| 第 2 著者 所属（和/英） | 名古屋大学(略称：名大) Nagoya University(略称：Nagoya Univ.) |
| 第 3 著者 氏名（和/英） | 酒井 正彦 / Masahiko Sakai |
| 第 3 著者 所属（和/英） | 名古屋大学(略称：名大) Nagoya University(略称：Nagoya Univ.) |
| 第 4 著者 氏名（和/英） | 関 浩之 / Hiroyuki Seki |
| 第 4 著者 所属（和/英） | 名古屋大学(略称：名大) Nagoya University(略称：Nagoya Univ.) |
| 発表年月日 | 2017-03-09 |
| 資料番号 | SS2016-61 |
| 巻番号（vol） | vol.116 |
| 号番号（no） | SS-512 |
| ページ範囲 | pp.7-12(SS), |
| ページ数 | 6 |
| 発行日 | 2017-03-02 (SS) |