12th WOCS2 形式手法と脆弱性評定を組み合わせたセキュリティ評価池田和博† 12th WOCS2 Security assessment that combined formal methods and vulnerability assessment Ikeda Kazuhiro ねらい上流工程でのセキュリティ評価として、形式手法と脆弱性評定を組み合わせた評価を実施することにより、セキュリティ仕様・品質を保証し、下流工程への影響を軽減させる。キーワードコモンクライテリア，脆弱性評定，侵入テスト，形式手法，Event-B，セキュリティ評価 Target: By implementing the security assessment that combine the vulnerability assessment and formal methods, ensures the security specifications and quality in the upstream process, and reduces the impact on downstream processes. Keywords: Common Criteria, vulnerability assessment, penetration test, formal methods, Event-B, security assessment ィが要求されるソフトウェア開発を行う際の国際規格１．想定する読者・聴衆には、情報セキュリティを評価し、認証する基準を定本テーマの想定する読者・聴衆は、組み込みシステめた国際規格 Common Criteria（ISO/IEC 15408：以下ムのセキュリティ設計・検証を行う技術者、特に、上 CC）[3]と、評価機関が CC の評価を行うための方法が流工程におけるセキュリティ品質向上に取り組んでい記載された共通評価方法 Common Evaluation る技術者である。組み込みシステムに限らず、ソフト Methodology（以下 CEM）[4]がある。ウェアセキュリティや形式手法を用いたセキュリティ検証に対して関心のある技術者も対象となる。 CEM の脆弱性評定（AVA クラス）では、Security Target、機能仕様、ガイダンス文書などと合わせて評価対象（TOE）が必要となる。CEM に基づく評価では、TOE の運用環境における脆弱性を公知の脆弱性情報などか 2．背景ら探索し、侵入テストにより脆弱性の悪用可能性を検 CPS（Cyber Physical System）社会の実現に向けて、証する必要がある。しかし、開発者自身が開発中のソ家電製品から自動車、航空機に至る様々な組込みシスフトウェアの上流工程の成果物（例えば、セキュリテテムとネットワークの接続が今後ますます加速する中ィアーキテクチャ記述、機能仕様、基本モジュール設で、組み込みシステムのセキュリティ対策がひっ迫し計など）を評価しようとした場合、まだ TOE が作成さた課題となっている。れていないため評価を実施することが出来ない。また、近年の組み込みシステムの開発規模の増加 [1] やネットワークにおけるセキュリティ脅威の高まり [2] により、組込みシステムに含まれるソフトウェアのセキュリティ対策の需要が拡大し、その開発コストも増加している傾向にある。 4．提案・実験通常、脆弱性評価は評価機関が開発終了後に実施するが、本実験では、開発者がソフトウェア開発の上流しかし、信頼性のあるセキュリティ対策を実現する工程で、開発成果物に対して実施する。例えば、要件ためには開発工程での厳密な設計が実現されていなけ定義工程では、機能仕様書およびその上位文書であるればならない。また、それらは評価によって保証され Protection Profile、Security Target[3]などに対して CEM のなければならない。脆弱性評定を行う。脆弱性の悪用可能性の検証は形式手法を利用して評価する。このように、上流工程で CEM 3．課題を用いた評価を実施することで、セキュリティ対策の考慮漏れ、ガイダンス文書による利用者の誤使用防止第三者によるセキュリティ評価は開発物を含めた評情報の不足、暗号アルゴリズムの既知の脆弱性対策の価を行うことが多いため、開発完了後にセキュリティ不備など、設計に依存する脆弱性を事前に評価するこ対策の不備が発見された場合、大きな手戻りとなる。とができる。また、開発者が行う設計物の脆弱性評定こうした問題を防ぐためにも開発者自身が開発工程のの評価内容を形式手法による数学的な証明により裏付なるべく早い段階でセキュリティ対策の品質を確保すけ、評価結果の根拠とする。るための評価を実施する必要がある。情報セキュリテ † ① 脆弱性探索アーク・システム・ソリューションズ株式会社開発部研究開発課 1 〒060-0001 北海道札幌市中央区北 1 条西 7 丁目 1 番地 15 あおいビル 8D TEL：(011)207-6460 FAX：(020)4622-5064 E-mail: [email protected] 開発物であるセキュリティコンセプト、セキュリテフサイクルを通して分析しマトリクスを作成するこィ要求仕様、機能仕様などに対して欠陥仮定法を用いとで、脆弱性によって影響が及ぼされる資産を特定し、た脆弱性の探索を行った。欠陥の仮定の基となる情報その資産に関わる Actor や Action を抽出した。例えば、は IPA の脆弱性対策情報データベース（JVN iPedia）通信時の通信データの完全性を検証する場合では、資を参照した。その際、JVN iPedia の脆弱性分類で使用産は「通信データ」、Actor は「送信者」と「受信者」、されている共通脆弱性タイプ一覧（CWE：Common 「外部からの攻撃者」、Action は「送信者から受信者 Weakness Enumeration）の 20 項目[5]を参考に脆弱性をへデータの送信」、「攻撃者による通信データの改ざん」網羅的に探索し、機能ごとの欠陥を仮定した。などとなる。さらに、攻撃者の能力によって、どのよ次に、仮定した欠陥に対する脆弱性有無の識別のため、脆弱性の対策が記載されているかを設計物から確認した。 ② うなリスクがあるかを想定し、攻撃方法を段階的に強化することを想定した。これらの要素を元に、Actor や Action によって“セ形式手法を用いた脆弱性の検証欠陥仮定法により識別された脆弱性のうち、設計物キュリティ機能が正しく動作している状態”を表す初期の形式モデルを Event-B によって作成し、保証すべに対策が記載されていない脆弱性に対する悪用可能きセキュリティ要件を証明により保証する。例えば、性の検証を、形式手法を用いて実施した。通信データの完全性を保証する場合、「受信者が受信したデータは送信者が送信したデータである」ことを、どのような Action が起こった場合でも不変であることを証明する。次に、その状態に対して脆弱性を悪用する攻撃モデルを導入することで、正しく動作している状態に影響があるかを証明により検証する。初期モデルで保証した証明が完了しない場合、Event-B の Plug-In ツール図 1. CC の脆弱性評価の流れと形式手法の適用工程 ProB[6]を用いて更に分析し、攻撃モデルの Action が Fig1. Flow of the CC vulnerability assessment and applying process of 成功する反例が発見されれば、脆弱性の悪用が可能と formal methods 形式手法の中でも仕様の検証ができる Event-B を用いて、前提条件（システムのライフサイクルや国際判断できる。また、ProB の ModelChecking 機能を使用することで、モデルの全てのシーケンスを網羅的に検証し、脆弱となる状態を導出することもできる。規格）、Actor（ユーザ、攻撃者など）、Action（機器操さらに、攻撃方法を段階的に強化することで、どの作、処理制御など）、資産、リスクなどの複雑な条件程度の脅威にまで対抗できているかを検証することに起因する脆弱性を検証した。ができ、CEM の脆弱性評定で使用する攻撃者の能力値による合否判定に応用することができた。 5．効果 CEM の脆弱性評定によって上流工程での設計に依存する脆弱性を評価することができ、下流工程への影響を未然に防ぐことができた。また、上流工程で実施できる TOE に対する侵入テスト以外の評価方法として形式手法を用いることで、脆弱性の悪用可能性を検証で図 2. 形式モデル化の要素と関係性き、脆弱性評価に利用することができた。形式手法を Fig2. The relationship of the elements for the formal method modeling 用いることで数理論的な証明による厳密な検証と、形式手法のモデル化の方針として、前提条件となる ProB のモデル検査による網羅的な検証により、脆弱性システムのライフサイクルや準拠する国際規格を考の漏れ抜けを防ぐことも可能である。従来手法では、慮する。例えば、ライフサイクルは「運用環境」、国脆弱性評価に対して、セキュリティ専門家によるレビ際規格は「CEM の脆弱性評定」などとなり、モデルューを経て妥当性を確認するが、その前段階で形式手化の方針は「システム運用時の、識別された脆弱性に法の検証によりレビュー対象の完成度を高めることが関わるセキュリティ機能のモデル化を行う」となる。でき、レビュー指摘による戻り作業を防止することで形式モデル化の要素は、CRUD 図を用いてデータ開発コストの低減を図る。が、どの機能で作成、参照、更新、削除されるかライ 2 6．まとめ上流工程で CEM の脆弱性評定を実施するために、形式手法を用いることで、悪用される脆弱性を検証することができ、設計に依存する脆弱性を軽減したソフトウェア開発が実現できる。それにより、下流工程で発生する設計不具合による改修コストを軽減することができ、ソフトウェアのセキュリティ品質の向上にも寄与できる。ここで評価できるのは設計で混入する脆弱性であり、実装で混入する脆弱性については侵入手テストによる評価を行う必要はあるが、下流工程での設計の評価は省略することができる。本テーマは、経済産業省－戦略的基盤技術高度化支援事業 H24～26 年度採択テーマ「形式手法を活用した組込みセキュリティ技術の確立と、安心・安全な CPS 社会を支える無線通信ミドルウェアの開発」にて取り組んでいる内容である。 7. 文献 [1] 経済産業省「組込みシステム産業の課題と政策展開（参考）組込みソフトウェアの規模の拡大」 , http://www.jasa.or.jp/et/ET2011/visitor/images/pdf/S1_web_data1 11116.pdf, [2] 2011 総務省「情報通信白書平成 25 年度版第 1 部第 3 章第 2 節 (1) 情報セキュリティに関する脅威の動向」 , http://www.soumu.go.jp/johotsusintokei/whitepaper/h25.html, 2013 [3] IPA 「情報技術セキュリティ評価のためのコモンクライテリアバージョン 3.1」, http://www.ipa.go.jp/security/jisec/cc/, 2012 [4] IPA 「情報技術セキュリティ評価のための共通方法バージョン 3.1」, http://www.ipa.go.jp/security/jisec/cc/, [5] IPA 「共通脆弱性タイプ一覧 CWE 2012 概説」 https://www.ipa.go.jp/security/vuln/CWE.html, 2014 [6] ProB 「 The ProB Animator and Model Checker 」 http://www.stups.uni-duesseldorf.de/ProB/index.php5/The_ProB_ Animator_and_Model_Checker, 2014 WOCS2: workshop on critical software systems． IPA: Information-technology Promotion Agency TOE: Target Of Evaluation, TOE は評価の対象となる製品、またはシステムの一部 Protection Profile: TOE の種別に対するセキュリティニーズについての実装に依存しないステートメント Security Target: 識別された特定の TOE に対するセキュリティニーズについての実装に依存するステートメント 3