北米
NSA - バイオメトリクスID認証を利用した入退室管理システム
| ドメイン |
|
| 開発対象 |
|
| 国 |
|
| 開発組織 |
|
| 形式手法（言語、ツール） |
|
| 適用範囲・規模（形式手法） |
|
| 適用対象のソフト種別 |
|
| 適用目的・工程 |
|
| 実装言語 |
|
| 実装規模 |
|
| 効果 |
|
（出典: David Cooper and Janet Barnes, Tokeneer ID Station EAL5 Demonstrator: Summary Report, 2008）
詳細情報
検証内容
-
部屋に入る権限を持つユーザがトークンリーダを通して自分のトークンをTIS (Tokeneer ID Station) に提供したとき、
もし、ユーザのトークンが正しいものであり、トークン内の認証と認可のデータがユーザの指紋と一致する指紋テンプレートを保有していたら、
ユーザが部屋に入ったらドアが閉まりロックされ、ユーザのトークンに権限付与証明書が与えられる。
等。
検証規模
-
SPARK Examinerが生成したVerification Condition292個のうち、223個はExaminer/Simplifierを利用して自動的に証明された。14個はInteractive Proof Checkerを利用して証明し、55個はレビューにより証明した。
期間
-
2003
判断
形式手法を利用した動機
-
EAL5レベルのシステムを、従来の開発プロセスよりもコストを抑えて開発することができるかどうかを実証するために形式手法を利用した。
手法・ツール選択理由
-
Zを利用した理由：
- notationがチェック可能であり、仕様作成時の小さい不具合も除去できる。
- 仕様作成時に詳細な設計について考える必要がない。
- 巨大なシステムを管理可能なサブコンポーネントに分割できる。
- 型チェックや検証のためのツールサポートがある。
障害と工夫
組織
体制
-
3名の技術者（2人はZの読み書きができ、セキュリティ等の専門知識を有していた。1人はZの解読はできるが記述スキルは不十分であった）
教育
その他
情報源
- David Cooper and Janet Barnes, Tokeneer ID Station EAL5 Demonstrator: Summary Report, 2008
- 形式手法適用調査 調査報告書、情報処理推進機構、2010