ディペンダブル・システムのための形式手法の実践ポータル

Mondex International、 Altran Praxis - MULTOS認証システム(Global Key Center)

ドメイン	通信
開発対象	MULTOS (ICカードのプラットフォーム) の認証局 (ICカードの活性化等を行う)
国	イギリス
開発組織	Mondex International、Altran Praxis
形式手法（言語、ツール）	Z、CSP、SPARK (Examiner)
適用範囲・規模（形式手法）	重要な部分のみ形式手法を適用。28のセキュリティポリシモデルがあった
適用対象のソフト種別	エンタプライズ系
適用目的・工程	要求仕様（Z）、設計（Z->CSP）、自動コード生成（CSP->Ada）、コード検証（Adaに対してSpark Examinerの利用）
実装言語	SPARK（30％）、Ada95（30％）、C++（30％）、C（5％）、SQL（5％）
実装規模	10万行程度
効果	実装前に問題点を理解することができる 各工程をより厳密に進めることができる 可用性99.999％を達成 形式手法を用いないで開発したシステムよりも、バグの数を少なく抑えることができた。（2002年時点でバグは4つのみ発見されている）

（出典: MULTOSウェブサイト）

詳細情報

検証内容

• CSPモデルに対して、デッドロックがないこと、セキュリティが特に重要な機能において並行プロセスが存在しないことを検証した。
• SPARKのインフォメーションフロー解析を実施した。
• Communications-Electronics Security Groupのマニュアルである「F」を簡潔にして実践した。

検証規模

期間

判断

形式手法を利用した動機

UK ITSECスキームの最も高いレベル（E6）に準拠する必要があった。E6では、初期段階から形式手法を使うことを求めている。

手法・ツール選択理由

• SPARKは、ITSEC E6の要求（プログラミング言語は、ソースコード中の全ての文に対し不明瞭でない意味を定義することが求められる）を満たし、実際に産業界で利用可能なほぼ唯一の言語である。
• 実装すべきセキュリティモデルの多くが、Zを利用することで直接モデル化可能であった

障害と工夫

• 既存製品を利用するとセキュリティ検証が煩雑になるため、できるだけ自前で実装した。
• システムを、セキュリティが特に重要な部分、セキュリティに関連する部分、セキュリティとは無関係な部分に分割した。セキュリティが特に重要な部分はSPARKを用いて開発を行った。
• CSPのモデルをコードに変換するルールを作成し、適用した。

組織

体制

教育

その他

情報源

Anthony Hall and Roderick Chapman, Correctness by Construction: Developing a Commercial Secure System, IEEE Software, Jan/Feb 2002, pp18-25

このページの先頭へ戻る