オブジェク卜指向言語の情報流解析における機密度のパラメータ化

摘要

本論文では，Banerjeeらのォブジェクト指向言語に情報流解析のための機密度に関するパラメトリック多相を導入する.情報流解析は機密情報の流出可能性の検出に有用である.しかし，型検査に基づく情報流解析ではプログラム中に型として機密度を指定する必要があるため，コレクションフレームワークのような任意の機密度のデータを扱うクラスを定義できない.そこで，機密度をパラメータに取るクラス定義と機密度パラメータを含む機密度の構造を提案する.機密度パラメータにどんな機密度が割り当てられても，型付け可能なプログラムは機密情報を流出させないことを保証できる型付け規則を構築し，非干渉性に対して健全であることを示す. In this paper, we introduce a parametric polymorphism of secrecy for information flow analysis to an object-oriented programming language. Information flow analysis is useful to detect invalid information leaks. However, it is difficult to define classes having any secrecy of data such as Collection Framework, since type-based information flow analysis requires specifying a secrecy of each data as a type in the program. We propose a way to declare classes parameterized over secrecy and a structure of secrecy as a type. We also propose typing rules to ensure that typable programs do not leak confidential information even if any secrecy is substituted for the secrecy parameter. We prove proposed type system is sound for noninterfering.