ホーム > 応用事例DB > 地域 > 北米

北米

Galois - Trusted Services Engine (TSE)

ドメイン
    通信
開発対象
    Bell-LaPadulaモデルに対応した分散ファイルシステム
国
    米国
開発組織
    Galois (SPAWAR: Space and Naval Warfare Systems Command, NAS: National Security Agencyのファンドを受ける)
形式手法（言語、ツール）
    Isabelle
適用範囲・規模（形式手法）
    一部のソフトウェアコンポーネントであるBAC (Block Access Controller)
適用対象のソフト種別
    エンタプライズ系
適用目的・工程
    設計
実装言語
    C
実装規模
    780行 (Cコード)
効果
    EAL 6の認証基準への準拠

（出典: Christopher Gunderson, Worldwide Consortium for the Grid (W2COG) Research Initiative Phase 1 Final Report, 2006）


詳細情報

検証内容

    [Isabelleによる検証]
  • TSEのセキュリティポリシとモデルが正しく対応していること
  • エラー状態へ到達しないこと
  • 高いセキュリティレベルのコンポーネントによるアクションが、低いセキュリティレベルのコンポーネントから不可視であること
    • [QuickCheck toolによる検証]
  • HOLコードとCの実装が正しく対応していること
  • QuickCheck toolにより、HOLモデルからテストケースを生成し、Cで記述されたコードに対してテストを実施した。
  • 同一レベルで書かれたデータを読めること
  • 正しい読み取りができること
  • 高いセキュリティレベルの読み取りができないこと
  • 高いセキュリティレベルのコンポーネントによるアクションが、低いセキュリティレベルのコンポーネントから不可視であること
    • [人による検証]
  • 各ラインについて最低2人がHOLコードとCコードを見比べてレビューを行った。

検証規模

期間

判断

形式手法を利用した動機

    EAL 6の認証基準に基づいて開発を行う必要があった。

手法・ツール選択理由

障害と工夫

組織

体制

教育

その他

情報源

    Christopher Gunderson, Worldwide Consortium for the Grid (W2COG) Research Initiative Phase 1 Final Report, 2006

カテゴリ

, , ,

このページの先頭へ戻る