研究課題
大規模な確率的システムからの秘密情報の漏洩量の推定を効率化・自動化することを目指し、本年度は昨年度に引き続いて定量的情報流解析の技術を改良するとともに、これを実装したツールHyLeakの開発に取り組んだ。その他に、暗号システムを記述した確率的プログラムの形式検証に関する解説論文を執筆した。1. 確率的システムに対する定量的情報流解析の手法には、記号的手法と統計的手法がある。本研究では昨年度、これらの二つの手法を融合させることにより、解析の品質と効率を両立させた新たな解析手法を考案していたが、本年度はこの新手法を改良した。具体的には、例えば、記号的手法に基づいてソースコードを解析することにより、解析の品質を保ちつつも、統計的手法におけるシミュレーションの実行回数を削減する手法を考案した。これらの研究成果をまとめ、査読付国際会議FM 2016（21st International Symposium on Formal Methods）で発表した。2. 前述の定量的情報流解析の新手法において、確率的プログラムの各部分に対して、記号的手法と統計的手法のどちらを用いて解析するとより効率的なのかを判定するヒューリスティクスを改良し完成させた。このヒューリスティクスを前述の解析技術と組み合わせることにより、確率的システムからの情報漏洩の度合いを、従来よりも高速かつ高品質に推定する解析技術を開発した。さらに、昨年度実装したプロトタイプを改良し、定量的情報流解析ツールHyLeakを開発し、公開した。また、HyLeakに関するツール論文を国際会議に投稿中である。3. 確率的システムの安全性検証に関して、定理証明支援系ベースの検証手法・ツールについて調査を行い、確率的システムの中でも暗号システムに焦点を当てて、安全性の形式検証の入門から計算機上での証明までを紹介する解説論文を執筆した。
28年度が最終年度であるため、記入しない。
すべて 2017 2016 その他
すべて 国際共同研究 (1件) 雑誌論文 (2件) (うち国際共著 1件、 査読あり 2件、 謝辞記載あり 2件、 オープンアクセス 1件) 学会発表 (2件) (うち国際学会 1件) 備考 (1件)
Proc. of the 21st International Symposium on Formal Methods (FM 2016), Lecture Notes in Computer Science
巻: 9995 ページ: 406-425
10.1007/978-3-319-48989-6_25
コンピュータソフトウェア
巻: 33(4) ページ: 67-83
10.11309/jssst.33.4_67
https://project.inria.fr/hyleak/
