抄録
B-023
RBACモデルの形式検証
◎鈴木大輝・岡本圭史・小林秀幸・高橋　薫（仙台高専）
アクセス制御を用いて不正な利用から情報システムを守る手法としてRBAC(Role-Based Access Control)がある．RBACでは，パーミッションをロールごとに割り当てることで,複雑化したアクセス制御を効率よく行うことができる.しかしRBACモデルの記述は主に人手で行われるため，矛盾や誤りが含まれる可能性がある．そのため，具体的に記述されたRBACモデルが意図通りに表現できているか検証を行う必要がある．
本校では具体的に記述されたRBACモデルの検証手法を提案する．検証には，ソフトウェアや組み込みシステム検証において有効なモデル検査の手法を応用する．