■モデル検査→セキュリティにも応用できる
・通信プロトコル
→SPINだけでなく、CSPやSMVも
・アクセス制御★(以下、これを書く)
・デジタル署名
■アクセス制御
・どの情報にだれがアクセスできるか、できないか
・ソフトがアクセス制御を守っているか?確認必要
人手では手間増大、抜けもある
→網羅的、機械的支援:モデル検査
■アクセス制御をモデル検査で、どうやるのか?
Spinを例に考える
・セキュリティポリシーをLTL式で記述
・システムをPromelaで記述
・2つをあわせてSPINで検証