ソフトウェアのセキュリティ・プライバシー解析における定量的尺度としてどの程度情報が漏洩したかを表現する量的情報流という概念が知られている。量的情報流解析の一手法として、命題論理式の解の個数を計算するモデル計数ソルバを利用した方法がある。本研究課題では、投射モデル計数の様々な計数技術を複合的に利用できる実行基盤を目指して、複数の計数手法を同じSATソルバ上に実装した上で、各々計算手法の実装の高速化や省メモリ化を実現した。また、量的情報流解析の一種である動的情報流解析に対して、実装したBDD/d-DNNF構築ツールを利用することで解析が高速化できることを確認しその有効性を示した。
|