|
本年度は、例外処理付きオブジェクト指向言語向けの情報流解析のための型システムを対象とする細粒度な型エラースライシング手法の洗練化および正当性の証明に取り組んだ。これにより、実際のソフトウェア開発に用いられているプログラミング言語に対して情報流解析と型エラースライシングを実現し、安全なソフトウェアの開発支援を可能とする。
情報流解析によって機密データを漏洩する可能性が存在することが判明したプログラムは修正する必要がある。このようなプログラムに対して可能な修正方法を列挙する手法を昨年度に提案したが、今年度はその手法を拡張した新しい手法を提案した。既存手法では実応用を難しくさせる制約が存在していたが、新手法では制約を取り除くことに成功し手法の有用性を向上させた。本提案が実現するプログラムの修正方法の列挙については本来の研究計画には含まれていなかったが、本研究の目的である機密データを漏洩しない安全なソフトウェアの開発支援の実現に寄与する重要な結果である。
本研究で対象とする情報流解析と型エラースライシングは偽陽性が存在しないように検査能力に制限を課している。しかし今後、検査能力を向上させることを考えると偽陽性の取り扱いを検討する必要が生じる。そこで本年度は、一般的な静的検査ツールにおける偽陽性を版間追跡を用いて開発者から隠蔽する手法を提案し、検査能力の向上に向けた準備を行った。
提案手法を実現するツールの開発と統合開発環境への組み込みに向けて、昨年度までに構築したプログラム解析基盤環境のテストを進めた。基盤環境を用いたツールの開発や統合開発環境への組み込みにも着手しているが、公開できる状態ではなく今後も開発を進めていく。
|
