自己合成法に基づく再帰プログラムの情報流解析法の提案

伊藤 信裕 (0651013)


近年,過失や故意による重要なデータの情報漏洩が深刻化している. 企業では社員に情報管理教育を徹底するなどの対策を行っている. しかし,プログラムの複雑な動作が原因で起こる情報漏洩に対する根本的な対策は難しい.

この問題を解決する重要な技術として,プログラムに入力した情報がどの出力から流出するかを調べる情報流解析が知られている. 情報流解析法として,型推論に基づく解析法が一般に知られている. 一方,型推論に基づく手法より精密な解析が行える場合もある自己合成法が近年注目されている. また,TerauchiとAikenは,型推論の結果を利用して自己合成法の精度と効率を向上させる手法(TA法と略記)を提案した. しかし,TA手法は再帰プログラム(再帰関数を含むプログラム)を対象としていない.

そこで本研究では,再帰関数を含むプログラムの解析を行えるようTA法を拡張した手法を二つ 提案し,それらの健全性を証明した. 一つ目の手法(手法1)は,検証ステップにおいて有限状態モデル検査器を利用することを前提とした 手法である.そのため,自己合成ステップにおいて関数の再帰呼出しを削除する必要がある. 具体的に,人間が各関数の型付けに対する予測を行い,それに基づいて自己合成ステップを実行し,検証ステップでは 有限状態モデル検査器を用いて非干渉性と型付けの正しさを同時に検証する. 二つ目の手法(手法2)は,検証ステップにおいてプッシュダウンシステム(PDS)モデル検査器を 利用することを前提とした手法である.

本発表では,まず,従来の情報流解析法を概観した後,二つの提案手法について説明する. 次に,手法1における有限状態モデル検査器としてBLASTを, また手法2におけるPDSモデル検査器としてMopedを用い, いくつかの単純な再帰プログラムをベンチマークとして, 提案する二つの手法による解析精度と解析効率を実測した結果について説明する.