情報リークの自動発見と定量化

情報フロー分析は、プログラムの実行中に露出された機密情報について考察するための強力な手法です。我々は、漏洩している情報を発見し、その包括的な定量的解釈を計算する情報フロー分析の最初の自動的方法を提示します。漏洩した情報は秘密のアーティファクトに対する同値関係によって特徴付けられ、対応するプログラム変数上の論理的主張によって表現されます。我々の測定手続きは、発見された同値クラスの数とそのサイズを計算します。これは、定量的情報フローにおけるすべての確立された情報理論的尺度を含む定量的特性のセットを計算するための基盤を提供します。我々の方法は、質的情報フローの形式モデルとプログラム検証技術との間の固有の関係を利用しています。プログラム検証と情報理論的分析の既存のツールに基づく我々の方法の実装を提供します。我々の実験評価は、提示した方法の実用性を示しています。