北米

NSA - バイオメトリクスID認証を利用した入退室管理システム

ドメイン
    その他
開発対象
    バイオメトリクスID認証ツールのアクセス管理等に利用されるセキュリティソフトウェアであるTokeneerを利用した入退室管理システム
    米国
開発組織
    Praxis High Integrity Systems
形式手法(言語、ツール)
    Z (fuzz type checker)、SPARK (SPARK Examiner)
適用範囲・規模(形式手法)
    Z及び英語テキスト:
  • 形式仕様・・118ページ
  • セキュリティプロパティ・・11ページ
  • 形式設計・・171ページ
適用対象のソフト種別
    制御系
適用目的・工程
    仕様記述、設計、コード検証
実装言語
    SPARK
実装規模
  • 宣言・・4964
  • 実行行数・・4975
  • SPARK flow アノテーション・・6036
  • SPARK proof アノテーション・・1999
  • コメント・・8529
  • 合計・・30278
効果
    多くの領域でEAL5の要求以上を達成した。形式手法を利用したことが結果的に効率的であった。

(出典: 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

このページの先頭へ戻る