| 研究課題/領域番号 |
17K00098
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
ソフトウェア
|
|---|
| 研究機関 | 名古屋大学 |
|---|
研究代表者 |
橋本 健二 名古屋大学, 情報学研究科, 助教 (90548447)
|
|---|
| 研究期間 (年度) |
2017-04-01 – 2021-03-31
|
| 研究課題ステータス |
完了 (2020年度)
|
| 配分額 *注記 |
4,550千円 (直接経費: 3,500千円、間接経費: 1,050千円)
2019年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
2018年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
2017年度: 2,210千円 (直接経費: 1,700千円、間接経費: 510千円)
|
|---|
| キーワード | 投射モデル計数 / 量的情報流解析 / BDD / 阻止節 / 変数順序 / d-DNNF / 成分キャッシュ |
|---|
| 研究成果の概要 |
ソフトウェアのセキュリティ・プライバシー解析における定量的尺度としてどの程度情報が漏洩したかを表現する量的情報流という概念が知られている。量的情報流解析の一手法として、命題論理式の解の個数を計算するモデル計数ソルバを利用した方法がある。本研究課題では、投射モデル計数の様々な計数技術を複合的に利用できる実行基盤を目指して、複数の計数手法を同じSATソルバ上に実装した上で、各々計算手法の実装の高速化や省メモリ化を実現した。また、量的情報流解析の一種である動的情報流解析に対して、実装したBDD/d-DNNF構築ツールを利用することで解析が高速化できることを確認しその有効性を示した。
|
| 研究成果の学術的意義や社会的意義 |
モデル計数・列挙技術を共通のSATソルバ上に実装することでそれらを複合的に利用できる環境を構築した。投射モデル計数・列挙を行うツールは一般のモデル計数・列挙のためのツールに比べて公開されているものはまだ少ない。今回、投射モデル計数を行うGPMCや投射モデル集合を表現するROBDDの構築を直接的に行うツールPC2BDDを開発し一般公開した。投射モデル計数・列挙は、量的情報流解析に限らず、規模の多い解析対象の部分的な性質を解析するのに有用であり今回のツールはそのような解析にも役立つ。
|
