1. No category

形式手法と脆弱性評定を
組み合わせたセキュリティ評価
アーク・システム・ソリューションズ株式会社
研究開発課 池田 和博
©2014 Arc System Solutions Inc. All rights reserved.
1
本取り組みの主張
形式手法と脆弱性評定を組み合わせたセキュリティ評
価で実現できること！
① 脆弱性評定のフロントローディング化
② 脆弱性評定を形式検証で実施
③ セキュリティホールの作り込みの防止
©2014 Arc System Solutions Inc. All rights reserved.
2
背景と課題
【背景】
• セキュリティ脅威への対策の需要が増大している。
• セキュリティ製品の開発だけでなく、評価する技術も必要。
【課題】
• 通常のセキュリティ評価の課題の一部
① 製品開発後のセキュリティ評価時に問題が検出されることにより、
手戻りの工数が発生する。
 設計段階での不具合の場合、手戻りの工数が増大する。
② 従来のレビューでは脆弱性検出の漏れ抜けが発生しやすい。
 システムが複雑化、規模の増大が要因で発生する。
③ 要件定義や設計段階では、システムの脆弱性に対してAttackの検証
が困難である。
 評価対象製品(TOE:Target Of Evaluation) が存在しない。
©2014 Arc System Solutions Inc. All rights reserved.
3
Common Criteriaの脆弱性評定
• 情報セキュリティの評価・認証の基準を定めた国際規格
Common Criteria(ISO/IEC 15408, 以下CC)の脆弱性評定
(AVA_VAN)を用いて、システムのセキュリティ上の欠陥や
脆弱性を分析・評価する。
 CCの脆弱性評定のメリット
『通常のセキュリティ検査では、主に既に知られている脆弱性情報に基づいてブ
ラックボックステストが行われる。一方、CCの脆弱性評定は既に知られている
脆弱性に加えて、開発者の提示する設計書なども検査した上で、製品に存在する
可能性のある脆弱性を洗い出し、テストする。』
参考：JISEC 開発者のための脆弱性評価解説 2.1 CCの脆弱性評価の特徴
 CCの脆弱性評定で評価可能な範囲
『基本的に、すべての開発上の脆弱性は脆弱性分析（AVA_VAN）の範囲で考慮
することができる。これは、この保証ファミリがある種の攻撃シナリオに特定さ
れない幅広い評定方法を適用できるという事実に基づいている。』
参考：コモンクライテリア パート3 16. AVAクラス 脆弱性評定
©2014 Arc System Solutions Inc. All rights reserved.
4
課題①の対策：手戻り工数の削減
セキュリティ製品の開発だけでなく、評価する技術も必要
Common Criteriaおよび共通評価方法Common Evaluation Methodology(以下CEM)を
参照する。
脆弱性評定(AVA_VAN)を用いたセキュリティ評価を開発の上流工程に適用する。
脆弱性を
検出した場合
脆弱性評定の
一般的なタイミング
システム設計
システムテスト
要件定義
基本設計
手戻りの回避には
なるべく早い段階で
評価することが重要
総合テスト
検
証
詳細設計
結合テスト
単体テスト
手戻りが
発生する
実装
©2014 Arc System Solutions Inc. All rights reserved.
5
課題①の対策：設計成果物に対する脆弱性評定
開発終了後に実施するシステムの脆弱性評定を、
開発の上流工程で「設計成果物」に対して実施する。
【対象となる設計成果物の例】
1. セキュリティアーキテクチャ or セキュリティコンセプト
2. セキュリティ要求仕様書
3. 機能仕様書、外部インタフェース仕様書
4. 基本設計書
5. ガイダンス文書、ユーザーマニュアルなど
 Protection Profile(PP)、Security Target(ST)と合わせて評価する。
•
•
PPとは：CCを用いて評価対象製品（TOE）を評価する際に、そのTOEの種別に
応じた、実装に依存しないニーズがまとまった文書。
STとは：セキュリティ設計仕様書。セキュリティ開発方針を記述した文書。
設計に依存する、もしくは設計段階で混入する
脆弱性を識別する
©2014 Arc System Solutions Inc. All rights reserved.
6
課題②の対策：脆弱性の検証
従来手法
と同様
本取り組み
のポイント
CCの脆弱性評定フローと形式手法の適用範囲
対策が施されていないと判定された(識別された)脆弱性が、
攻撃者によって悪用できるかを検証する。
形式手法の中でも仕様の検証ができるEvent-Bを利用して検証する
©2014 Arc System Solutions Inc. All rights reserved.
7
課題②の対策：網羅的な検証方法
システムのセキュリティ仕様や動作・振舞いを形式モデル化す
ることで、システムの特性を表すことができる。
それにより、セキュリティ上の問題や矛盾を形式仕様記述の
「証明」によって網羅的に検証することも可能である。
例）Event-BモデリングのためのRodinプラットフォームのプラグイン
「ProB」のModel Checking機能を使えば、定義したイベント(アクシ
ョン)を実行して網羅的な検証ができる。
仕様
セキュリティ・
システム仕様
人
振舞い
人
機器
TOEと
TOEに関わるもの
©2014 Arc System Solutions Inc. All rights reserved.
形式モデル化
・・・
・・・
・・・
TOEの形式モデル化
8
課題③の対策：形式モデル化の例
攻撃者によって脆弱性を悪用することが可能かを検証するため脆弱
性に関連するシステム仕様の形式モデル化を行う。
 前提条件：形式モデル化の方針
– システムのライフサイクル：開発段階、運用環境、廃棄など
– 準拠する規格、規定：ISO/IEC15408
 形式モデルの要素（例:通信データの完全性を検証する場合）
–
–
–
–
資産：通信データ
Actor：送信者、受信者、外部からの攻撃者
Action：送信者から受信者へデータの送信、攻撃者による通信データの改ざん
リスク：通信データの盗聴・改ざんによって、正しいデータが取得できない
 保証すべきセキュリティ要件
– 通信データの完全性（改ざんされてないこと）
受信者が
持っている
データ
送信者が
持っている
データ
 攻撃者モデル
– 攻撃者による脅威を想定（⇔リスク）
– 攻撃方法のパターンを設定し、能力値を算出
©2014 Arc System Solutions Inc. All rights reserved.
9
課題③の対策：攻撃者モデルによる脆弱性の検証
• Event-Bのリファインメントによる証明を用いて検証する。
初期モデル
 脆弱性に関連する「セキュリティ機能が正しく動作して
いる状態」を表すモデルを初期モデルとして作成する。
 保証すべきセキュリティ要件を証明により保証する。
リファインメント
 初期モデルを詳細化・具体化する。
 初期モデルで定義されたもの以外で必要な「他の環境的
な要因」や「処理の振舞い」などを追加する。
攻撃モデル
 識別された脆弱性を悪用しようとする攻撃者モデルを作
成する。
 攻撃パターンを段階的に強化する。
• 「ProB」のModel Checking機能を利用して、攻撃者が脆弱性を
悪用する攻撃が成功するかどうかを検証する。
• 保証すべきセキュリティ要件の証明の反例が検出された場合
脆弱性が悪用可能であると
判断することができる！
©2014 Arc System Solutions Inc. All rights reserved.
設計に依存する脆弱性を改修、
下流工程への影響を未然に防ぐ
10
効果
• 上流工程でCCに基づいた脆弱性評定を実施することができる。
• 設計に依存する脆弱性を早期に発見、対策することができ、下流
工程での影響を未然に防ぐことができる。
• 形式手法を用いて、保証すべきセキュリティ特性を検証すること
により、脆弱性の悪用可能性の検証ができる。
• 形式手法による脅威モデルの段階的な強化により、脆弱性評定の
合否判定に利用できる。
V字開発における形式手法と脆弱性評定の適用工程
©2014 Arc System Solutions Inc. All rights reserved.
11
形式手法を活用した脆弱性評定
Common Criteriaの脆弱性評定を上流工程で実施するために
形式手法を活用する。
©2014 Arc System Solutions Inc. All rights reserved.
12
まとめ
① 脆弱性評定のフロントローディング化
– 上流工程において、CCの脆弱性評定を行い、設計に依存する脆弱性
を早期に検出することで、下流工程への影響を軽減するだけでなく
、セキュリティ品質の向上にも寄与する。
② 脆弱性評定を形式検証で実施
– 上流工程において、CCの脆弱性評定を実施するために、形式手法を
用いることで網羅的な検証ができる。
③ セキュリティホールの作り込みの防止
– 形式手法モデルに、攻撃者モデルを導入することで、脆弱性が悪用
可能か検証できる。
悪用される脆弱性を作り込まない
システム・ソフトウェアの開発が期待できる！
©2014 Arc System Solutions Inc. All rights reserved.
13
最後に
• 経済産業省－戦略的基盤技術高度化支援事業を活用
– H24～26年度採択テーマ「形式手法を活用した組込みセキュリティ
技術の確立と、安心・安全なCPS社会を支える無線通信ミドルウェ
アの開発」
経済産業省
産業技術総合研究所
名古屋大学
形式手法を活用した組込み
セキュリティ技術の確立と、
安全・安心な CPS 社会を支える
株式会社ヴィッツ 無線通信ミドルウェアの開発
Bメソッドで
実践開発を!!
委託
公立はこだて未来大学
川上・川下の連携による
コンソーシアム
アーク・システム・ソリューションズ㈱
株式会社テクノフェイス
株式会社iD
©2014 Arc System Solutions Inc. All rights reserved.
株式会社アトリエ
アドバイザ
国内有数メーカ
川下企業
14
ご清聴ありがとうございました。
アーク・システム・ソリューションズ株式会社
研究開発課 池田 和博
TEL：011-207-6460
E-Mail：[email protected]
©2014 Arc System Solutions Inc. All rights reserved.
15