スタック検査機能を持つプログラムの
制御フロー解析に基づくセキュリティ検証法

伊加田 恵志 (9951003)


Java development kit 1.2のように, プログラム実行時に制御スタックを検 査することでアクセス制御を行うようなプログラム環境がある. このような環 境下で実行されるプログラムが与えられたとき, どのような実行に対しても, あ る望ましい性質(検証条件)が成り立つかどうかを保証できることが望ましい.
本発表では, このような検証問題に対する検証法として形式言語を用いた手法 を提案する.

Jensenらは, プログラムと時相論理式を用いて記述した検証条件を与えたとき に, プログラムの到達可能な状態全てが検証条件を満たすかどうかを決定する 問題として検証問題を定義した. そして, 彼らの論文では, 相互再帰を含まな いプログラムのクラスに対して検証問題が決定可能となることが示されている.

本発表では, プログラムのトレース集合がインデックス言語となることを示し, その系として検証問題が決定可能となることを示す. 本手法は, 検証条件を時 相論理式よりも真に表現能力の大きい正規言語で記述することができ, かつ, 任意のプログラムに対して検証可能となるため, Jensenらの結果を真に改善し ている.
さらに, 検証問題の計算複雑さについても述べ, 効率良く解ける検証問題の部 分クラスを提案する.