動的職責分離を記述できるアクセス制御モデルの形式的検証手法

摘要

近年，企業の不祥事により内部統制の強化が求められるようになった．内部統制の要求事項の一部に内部の人間の不正を抑止するための職責の分離がある．人的リソースの観点から，動的な職責分離を整備する方が，組織にとって人的リソースの有効活用や人件費の削減など，メリットがある場合がある．しかしながら，動的職責分離では，サブジェクトとオブジェクトのすべての状態の組み合わせにおいての不適切なアクセス認可が行われないかを確認しなければ，職責の分離が達成できているとは言えない．説明責任の観点からも動的職責分離の検証が必要である．人手による検証は非効率的であり，十分でない．本研究では，形式的手法を用い，動的職責分離を記述可能とするアクセス制御モデルの検証手法を提案する．