講演抄録/キーワード |
講演名 |
2016-10-27 15:30
#SMTツールを用いた量的情報流解析手法の高速化 ○中島聖斗・Trung Chu Bao・橋本健二・酒井正彦・関 浩之(名大) SS2016-26 DC2016-28 |
抄録 |
(和) |
プログラムの量的情報流(QIF)を解析する手法の一つとして,プログラムを背景理論付き論理式へ変換し出力変数に投射したモデル計数(#SMT)による方法がある.本研究では#SMTツールを用いたQIF解析手法の高速化を目指し,#SMTツールにおいて充足不能コアとモデルのキャッシュを利用する改良をそれぞれ試みる.また,モデル計数時の投射する論理変数の選択順の変化によるQIF解析時間への影響を測定し,その結果に基づき,前処理としてプログラムの静的解析を行うことで効率の良い選択順を得る手法を考察する. |
(英) |
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 use unsatisfiable core and model caching in a #SMT tool. We also measured the impact of the selection order of the projected variables to the efficiency. Based on the result, we propose a method that determines an efficient selection order by static analysis of a program as a preprocessing. |
キーワード |
(和) |
量的情報流 / 投射モデル計数 / SMT / / / / / |
(英) |
quantitive information flow / projected model counting / SMT / / / / / |
文献情報 |
信学技報, vol. 116, no. 277, SS2016-26, pp. 49-54, 2016年10月. |
資料番号 |
SS2016-26 |
発行日 |
2016-10-20 (SS, DC) |
ISSN |
Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 |
著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します.(許諾番号:10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) |
PDFダウンロード |
SS2016-26 DC2016-28 |