1 ET 2014 IPA ブースプレゼン GSN (Goal Structuring Notation) を用いたアシュアランスケース セーフティーケース作成支援 ~ 認証支援のための方法論 ~ 2014 年 11 月 20 日 ( 独 ) 産業技術総合研究所 セキュアシステム研究部門システムライ

1 ET 2014 IPA ブースプレゼン GSN (Goal Structuring Notation) を用いたアシュアランスケース セーフティーケース作成支援 ~ 認証支援のための方法論 ~ 2014 年 11 月 20 日 ( 独 ) 産業技術総合研究所 セキュアシステム研究部門システムライフサイクル研究グループ 田口研治 相馬大輔

2 自己紹介 経歴 産業技術総合研究所招聘研究員 ( 併任 ) 2010 年 4 月 ~ ( 株 ) シーエーブイテクノロジーズ代表取締役社長 2011 年 4 月 ( 設立 ) ~ 産業界における 11 年間の経験 ソフトウェア業界における研究開発 コンサルティング 大学 研究機関での 13 年間の経験 海外の大学教員 (5 年間 ) Uppsala Uni. (Sweden), Bradford Uni. (UK) 国立情報学研究所特任教授 ( 5 年間 ) 専門分野 + 高信頼システム開発方法論 ( 形式検証 国際規格認証 システム保証 安全 脅威分析方法論 ) + 形式手法 ソフトウェア工学 システムアシュアランスに関する 多くの主要な国際会議の PC 等を歴任 (FM 05, HASE 04, ASSURE 04, ICECCS 03) 規格 国際会議関連 International Conference on Formal Engineering Methods 2012 のプログラム委員長 OMG System Assurance Platform Task Force の co-chair FP7 OPENCOSS プロジェクトの External Advisory Board Member SICE 認証工学 WG 主査 共同研究 + 新列車制御システムの安全評価

3 著書 ( 編者 著者 ) Integrated Formal Methods (ifm) 国際会議設立 (1999 年 ) 共同編者 ソフトウェア科学基礎 近代科学社 2008 年 共同著者 ACM SIGCSE, inroads Bulletin, 2009 年 共同編者 (Special Issue on Formal Methods Education and Training) セキュリティ要求工学の実効性 情報処理学会学会誌 2009 年 共同編者 International Conference on Formal Engineering Methods (ICFEM) 国際会議 2012 年 共同編者

4 アシュアランスケースに関するこれまでの実績 国際標準規格策定関連 OMG SACM (Structured Assurance Case Metamodel) RTF (Revision Task Force) メンバー セーフティケースに関連する国際会議関連での学会活動 ASSURE (International Workshop on Assurance Case for Software-intensive Systems) 2013, 2014 PC AAA (International Workshop on Argument for Agreement and Assurance) 2013 Program co-chair SASSUR (International Workshop on System Assurance Approaches for Safety-Critical Systems) 2013, 2014 PC 論文発表 Y. Matsuno, K. Taguchi: Parameterised Argument Structure for GSN Patterns: QSIC 11 K. Taguchi, D. Souma, H. Nishihara, T. Takai: Linking Traceability with GSN, ASSURE 14 その他 External Examiner, ヨーク大学 Linling Sun, Establishing Confidence in Safety Assessment Evidence (2012) ( 指導教官 : Tim Kelly)

5 内容 (1) 安全を担保するセーフティーケース制度に関する説明と セーフティーケースの作成を支援する記法である GSN (Goal Structuring Notation) がどのような背景から生まれたかを説明します 背景 セーフティーケースがなぜ生まれたか? セーフティケース制度 (Safety Case Regime) がどのような規格 ガイドラインにより社会制度として確立しているか 問題点はあるのか? セーフティーケース作成を支援する表記法である GSN の文法 利用方法

6 セーフティーケース制度 (Safety Case Regime) の始まり 1988 年 7 月における 北海油田における Piper Alpha 事故 167 名死亡 (229 名中 ) 270 億円の被害を生じた Cullen 卿による事故調査レポートにより安全ケースの重要性が強調された Compliance with detailed prescriptive regulations was not sufficient to ensure safety The Offshore Installations (Safety Case) Regulations 1992 に導入 ( 最新版 2005 [1]) 法規 規格に書かれた通りにすれば安全であるという考え方への反省から セーフティケースの提出 アセスメント方式の厳格化などについて社会的基盤の形成 研究が進んだ セーフティーケース制度 (Safety Case Regime) の導入!

7 セーフティケースの定義 英国の防衛規格 (Defence Standard 00-56) による定義 与えられた運用環境におけるシステムの適用に関して 安全であることを 強制的かつ理解可能 妥当な事例として提供する 根拠資料の集まりにより支援された構造化された議論 A structured argument, supported by a body of evidence that provides a compelling, comprehensible and valid case that a system is safe for a given application in a given operating environment.

8 セーフティーケースの提出が義務付けられている分野 規格 EUROCONTROL 航空管制システムにおける安全性の保証 Rail Yellow Book 英国における鉄道信号システムの安全性の保証 Railway Safety Case Regulations 英国における鉄道安全法規 IEC 62425/EN 50129 鉄道システムのセーフティーケース規格 ISO 26262 車載組込みシステムの機能安全規格 他にも 防衛 原子力 海上設備 医療機器 など

9 米国における軍事製品調達におけるシステム保証 米国における戦略的な Safety Case への取り組み DHS (Department of Homeland Security) Common Body of Knowledge (CBK) DoD (Department of Defense) Engineering For System Assurance 2008

10 セーフティーケースとは? 鉄道におけるセーフティーケース規格 (IEC 62425) を例として アセスメントの対象となる構造化された文書 Part 1: システムの定義 Part 2: 品質管理報告書 Part 3: 安全管理報告書 Part 4: 技術安全報告書 Part 1: はじめに Part 2: 正しい運用の保証 Part 3: 故障の影響

11 セーフティーケースが必ずしも有効でなかった例 ( Nimrod の事故例 ) 指摘された問題点を記述 ( 未完成 )

12 セーフティーケース アシュアランスケース自体に関する規格 OMG (Object Management Group) による SACM (Structured Assurance Case Metamodel) 規格 ISO/IEC 15026-2 Systems and software engineering -- Systems and software assurance -- Part 2: Assurance case 日本からの貢献 SACM は産総研 田口が参加 15026 は神奈川大 木下教授が参加 ケース のための記法 GSN (Goal Structuring Notation) T. Kelly らによる GSN Community Standard

13 内容 (2) セーフティーケースを記述する記法である GSN (Goal Structuring Notation) と その書き方を説明します 背景 セーフティーケース作成を支援する記述法の 1 つである GSN について説明 どのような書き方が正しいか? 規格への適合性確認を支援する際の書き方

14 Goal Structuring Notation (GSN) システム保証のための構造化された議論の記述方法 T. Kelly (York University) により開発 詳細な記法は GSN Community Standard トップダウン手法 Goal : 議論を構成する主張 Strategy : ある Goal とそれ以外の一つ以上の Goal の間に存在する推論の説明 Supported by : 推論関係や証拠関係 Goal Strategy Solution をつなぐ Solution : 証拠となるものへの参照 Context : Goal や Strategy の内容に対する補足情報 In Context of : 文脈上の関係 Goal Strategy から Context などへつなぐ

15 GSN による議論の記述例 機能安全規格に従うことで どのように安全性が保障されるか その記載内容を GSN で記述することで示す 対象 : IEC 62278 鉄道分野の機能安全規格

16 IEC 62278 とその GSN 記述について 開発プロセスは 14 の段階から構成される 各段階が適切に実施されているかを GSN により記述 ここでは第 3 段階 リスク分析 を対象とする 対象

17 IEC 62278 各段階の構成 IEC 62278 の各段階は以下のような項目から構成されている Objective : 段階で達成するべき事項 Input : 段階で必要となる情報やドキュメント Requirement : 目的を達成の sub-goal や成果物への記載内容など Deliverable : 段階で作成されるドキュメント Verification : 段階で実施しなくてはならない検証項目

IEC 62278 第 3 段階の GSN 図全体像 Argument for achieving objectives Argument for input Argument for safety analysis Argument for process for on-going risk management IEC 62278 第 3 段階 : 2 ページ GSN 図 : Goal 36, Strategy 14, Solution 29, Context 14 18

19 GSN による記述の説明範囲 GSN による記述 1 GSN による記述 2

第 3 段階が適切に実施されたことをトップゴールとして配置 GSN による記述 1 6.3 第 3 段階 : リスク分析 6.3.1 目的この段階の目的は 次のとおり a) 当該システムに関わるハザードを特定する b) ハザードの発生につながる事象を特定する c) ハザードに付帯するリスクを明らかにする d) リスクを継続的に管理数 r プロセスを確立する 6.3.2 インプットこの段階へのインプットは 6.3.3 要求事項 6.3.4 成果物 6.3.5 検証 IEC 62278 ( 英和対訳版 ) より 目的ごとに達成されていることを議論する 20

6.3 第 3 段階 : リスク分析 成果物が証拠となる GSN による記述 2 ハザード特定の十分性を示す方法ごとに議論する 参照する文書 条件などをコンテキストとして配置 サブゴールとして要求事項などを配置する 6.3.1 目的この段階の目的は 次のとおり a) 当該システムに関わるハザードを特定する b) ハザードの発生につながる事象を特定する c) ハザードに付帯するリスクを明らかにする d) リスクを継続的に管理数 r プロセスを確立する 6.3.2 インプット 6.3.3 要求事項 6.3.3.1 この段階の要求事項その1は 次の事項を行うことである a) その適用環境で当該システムに関わるすべての合理的に予見可能なハザードを体系的に特定し 順位付けを行う このハザードには 次の原因で発生するものを含む システムの正常運用 6.3.4 成果物 6.3.4.1 この段階で得た結果は この段階で行ったすべての仮定と正当性の証明とともに文書化しなければならない 6.3.4.2 リスク分析の結果はハザードログに記録されなければならない 6.3.5 検証 6.3.5.1 この段階では 次の検証を行わなければならない c) リスク査定の完全性の査定 g) この段階の業務を行ったすべての担当者の力量の査定 IEC 62278 ( 英和対訳版 ) より 21

22 内容 (3) セーフティーケースや GSN などの記法に関連する話題についてより詳細な説明をします 背景 GSN の書き方 どう書けば良いのか? GSN の意味論的背景

23 GSN 記述の注意 一つの要素 (Goal, Context, Solution) に複数の内容を含めない 明確に記述する 文の構造や語が複数の解釈が可能とならないようにする Context により曖昧な語の意味を添える 論理の飛躍に注意する

24 GSN の問題点 表記法としての問題点 意味論の欠如 論理的導出? それとも 特定のデータ構造 ( 木構造 グラフ構造 ) を持った図表現? 公理的意味論? 表示的意味論? どのような意味論があるのか? 論理的導出からの逸脱 本来 論理的導出を基本にしていたので ある程度は 論理的な導出と同じ しかし Justification, Assumption, Context, Solution など論理的に解釈が難しい要素が導入されている 利用の問題点 論理的導出だから正しいという誤った判断に導かれやすい 図表現としての曖昧さを利用して 様々な本来の意図とは異なる利用方法が容易に可能 A 論理学の導出規則 ( 自然演繹 ) A B - 導入 論理的導出の例 A A B C (A B) C - 導入 - 導入 ここまでは容易に対応関係が言えるが 他の構文要素 (context など ) が入ると 伝統的論理学からは逸脱する A B A B GSN の例 - 導入

25 議論構造の検討について 以下は全てのハザードに対し十分対抗されている際に安全とする場合の GSN 図の例 どちらが良い?

26 GSN で表せること A) どのように保証を行うかの考え方を表現 例 : パターン言語を使用 B) セーフティーケースなどの規格やガイドラインへの適合性確認のための根拠資料の支援 A) の例 GSN のパターン言語 B) の例認証支援

27 ソフトウェアの安全性の保証規則 : 安全ソフトウェア要件 (SSR) は 抽象度が高いものから 詳細なものに分解される SSR は各階層において 設計と連携している 上位の階層から下位に洗練される R. Hawkins より引用

28 まとめ セーフティーケース制度による安全の保証についての概要 ( 背景 歴史 様々な法規制 規格 など ) セーフティーケース作成支援のための記法 GSN (Goal Structuring Notation) の概要 利用方法 動画による解説 https://www.youtube.com/watch?v=vedmkvmcbeg https://www.youtube.com/watch?v=s32klhbt96c

29 認証工学にご興味がある人 SICE の 認証工学 WG では この発表のような GSN による認証支援を含む様々な国際規格や認証に関する課題が話合われています 国際規格策定や製品 プロセス認証に関する工学的 科学的方法論の確立のためには 課題やその解決方法について 幅広く議論が出来る場が必要です そのために メーカー 認証機関 研究機関が 認証や規格に関する諸問題を研究するためのフォーラムとして設立されました 認証に関する新たな学問分野 認証工学 を確立し 新たな知見を創出する場として今後活動します ご支援の程 宜しくお願い申し上げます