@article{oai:kutarr.kochi-tech.ac.jp:00000117,
 author = {高田, 喜朗 and 王, 静 and 関, 浩之},
 issue = {4},
 journal = {電子情報通信学会論文誌. D, 情報・システム = The IEICE transactions on information and systems},
 month = {Apr},
 note = {プログラムが望ましくない動作を行うことを防ぐ動的アクセス制御機構として，Java仮想機械等に実装されているスタック検査が広く用いられている．しかし，スタック検査は，実行が完了したメソッド呼出しに関するセキュリティ情報が消失するという問題点をもつ．これを解決するため，実行履歴に基づく各種のアクセス制御機構が提案されている．本論文では，Abadiらのアクセス制御法を形式的に定義したHBACプログラムモデルを提案し，HBACプログラムに対するモデル検査法について考察する．具体的には以下の2点を行う．（ 1 ） HBACプログラムに対する検証問題は，現実的な仮定のもとでは多項式時間可解であるが，一般の場合は決定性指数時間完全であることを示す．（ 2 ） HBACプログラムの検証におけるいくつかの最適化法を提案する．試作検証ツールを使った簡単な実験により，現実的な時間と領域でHBACプログラムの検証が可能であることを示す．},
 pages = {847--858},
 title = {実行履歴に基づくアクセス制御の形式モデルと検証},
 volume = {J91-D},
 year = {2008}
}