ソフトウェアバグを根絶する静的コード解析

Size: px

Start display at page:

Download "ソフトウェアバグを根絶する静的コード解析"

すずりりゅうとう
4 years ago
Views:

1 ソフトウェアバグを根絶する静的コード解析 ~ 組込みシステムのセキュリティ脆弱性の検出と安全性を証明 ~ MathWorks Japan アプリケーションエンジニアリング部 ( 制御 ) アプリケーションエンジニア田中康博 2018 The MathWorks, Inc. 1

2 自動運転のサイバーセキュリティソフトウェアは安全性だけではなくセキュリティも重要車載通信 & V2X 通信通信の増加 V2I リモートスタート Wi-fi ホットスポットインターネット上のノードサイバー攻撃の脅威にさらされるワイヤレスキーインターネット接続 V2V TPMS ecall Bluetooth 接続安全性セキュリティ 2

自動運転のサイバーセキュリティ (2) コードレベルでセキュリティを作り込むことが重要ソフトウェアの脆弱性

セキュリティに対する知識セキュリティレベルの差出典 2015年 http://www.blogcdn.

jpg セキュリティ強化後もハッキング可能だった出典 2017年 http://techon.

3 自動運転のサイバーセキュリティ (2) コードレベルでセキュリティを作り込むことが重要ソフトウェアの脆弱性 Jeepハック後に140万台をリコールセキュリティ対策を困難にする要因: H/WとS/Wのスペックセキュリティに対する知識セキュリティレベルの差出典 2015年セキュリティ強化後もハッキング可能だった出典 2017年 mn/15/425482/ /?p=3 コードのセキュリティを何で検証するのか 3

4 Polyspace ソフトウェアのコード静的解析ソリューションコードのセキュリティと安全性の確保は静的解析が有効な手段 Polyspace Bug Finder によるセキュリティ脆弱性の検出セキュリティ Polyspace Code Prover による安全性の証明安全性 4

5 アジェンダ 1. サイバー攻撃の事例紹介 2. セキュリティ脆弱性の検出 3. ソフトウェアの安全性の証明 4. ユーザー事例 & まとめ 5

6 Jeepハック出典: 2015年 6

7 組込みソフトウェアのセキュリティ - 外部インターフェース外部インターフェースを介して攻撃されるリスクが高まっているネットワーク 3 rd パーティーソフトファイルシステム Control Algorithm, Fault Detection, Supervisory Logic Utility (I/O Driver, Lookup Table, etc.) RTOS, Fault Logging, Service Tool Interface ユーザ入力 HSM センサー 8

8 組込みソフトウェアのセキュリティ脆弱性外部インターフェースが多ければ攻撃されるリスクは更に高まるネットワークファイルシステムネットワーク接続操作の順序が正しくない汚染されたデータ相対パス記法を悪用汚染されたデータ Utility RTOS, TOCTOU攻撃 Control (I/O Driver, Fault Logging, Algorithm, 脆弱なパス操作 (パストラバーサル) 汚染されたデータ Lookup Service Tool Fault Detection, Table, Interface Supervisory 保護されていない一時ファイルの使用 etc.) 3 rdパーティーソフトユーザ入力 Logic HSM 定数シードからの確定的なランダム出力脆弱な疑似乱数ジェネレーターヒープメモリがリリース前に未クリア汚染されたデータセンサー 9

9 組込みソフトウェアのセキュリティ脆弱性最大の問題: 出典 2016年 Industrial Control Systems (ICS) Cyber Emergency Response Team (ICS-CERT) 不適切な入力確認クレデンシャル管理 10

10 Jeep ハック - 決定論的乱数発生器 (DRNG) 1970/01/ /01/19 今日不可能製造不可能 time() = integer 2,147,483,647 可能 (2 32-1) Polyspace Bug Finder 11

11 アジェンダ 1. サイバー攻撃の事例紹介 2. セキュリティ脆弱性の検出 3. ソフトウェアの安全性の証明 4. ユーザー事例 & まとめ 14

MISRA 準拠を確認コードメトリックス解析コードの複雑度を測定開発プロセスの上流で不具合を発見!

12 Polyspace Bug Finder のスピーディー解析素早い欠陥検出修正を可能とする! セキュリティ脆弱性バグ検出コード作成後すぐに欠陥を検出修正コーディングルールチェックエラー予防と再利用性向上 MISRA 準拠を確認コードメトリックス解析コードの複雑度を測定開発プロセスの上流で不具合を発見! コードを統合前に多くの欠陥を修正! コード開発の効率に繋がる! 時間を掛けずに大部分のバグを識別コード作成修正 Bug Finder 解析レポート自動生成 15

セキュリティ脆弱性バグ検出項目数値動的メモリデータフローリソース管理ゼロ割オーバーフローメモリリーク読取りのない書込み読取り専用リソースに書込み標準ライブラリ数学ルーチン前に解放したポインター未初期化変数以前に閉じられたリソースを使用の無効な使用の使用静的メモリセキュリティ同時実行データレース適切な手法未使用のパラメータ

13 セキュリティ脆弱性バグ検出項目数値動的メモリデータフローリソース管理ゼロ割オーバーフローメモリリーク読取りのない書込み読取り専用リソースに書込み標準ライブラリ数学ルーチン前に解放したポインター未初期化変数以前に閉じられたリソースを使用の無効な使用の使用静的メモリセキュリティ同時実行データレース適切な手法未使用のパラメータ配列の範囲外アクセス NULLポインターパス操作が脆弱疑似乱数発生器が脆弱デッドロック値渡しの大きな引数プログラミング汚染されたデータ等号演算子による浮動汚染された文字列形式小数点の比較汚染されたサイズでの宣言の不一致メモリの割り当て 16

14 サイバーセキュリティ業界活動と標準自動車業界に見られるコーディング標準実践 CERT C セキュアコーディングスタンダード ISO/IEC TS Cセキュアコーディングルール CWE 共通脆弱性タイプ MISRA-C:2012 Amendment 1 セキュリティ 17

15 コーディングルールチェック MISRA C 2004 チェッカー MISRA C 2004 AC AGC チェッカー自動生成コード用 MISRA C 2012 チェッカー MISRA C++ チェッカー JSF ++ チェッカー新しいコーディング規約に対応 (全ての required と mandatory) 新しい指針 (directive) 1 新しいルール (rules) 13 既存のルール変更 [21.8] 18

16 MISRA-C:2012 改訂 1 の新しい指針 4.14 の例汚染されたデータによる除算 19

17 アジェンダ 1. サイバー攻撃の事例紹介 2. セキュリティ脆弱性の検出 3. ソフトウェアの安全性の証明 4. ユーザー事例 & まとめ 20

18 バグを見つけることができますか? ゼロ割の可能性オーバーフローの可能性未初期化の可能性 actuator_position = x / (x - y); 21

19 Polyspace Code Prover の実行結果あらゆる条件でコードの安全性を証明テストを行わずに網羅的に解析実行時エラー条件による実行時エラー到達不能なコード actuator_position = x / (x - y); 22

Polyspace Code Prover でコードの正しさを証明全ての実行パスの結果を証明する Quality 品質

C/C++/Ada Process プロセスランタイムエラーの早期検出自動生成コードハンドコードの解析可能

$static int int int void pointer_arithmetic (void) { array[100];$ $エラー実行される度にランタイムエラー if (get_bus_status() > 0) { if$ local pointer p i++; (pointer to int 32, size: 32bits): } }

local pointer p i++; (pointer to int 32, size: 32bits): } }

条件によってランタイムエラー buffer of 400 bytes, so is outside i =

20 Polyspace Code Prover でコードの正しさを証明全ての実行パスの結果を証明する Quality 品質ランタイムエラーの証明測定向上管理 Usage 使用方法コンパイルプログラム実行テストケースは不要対応言語 C/C++/Ada Process プロセスランタイムエラーの早期検出自動生成コードハンドコードの解析可能コードの信頼性を測定実機実験前にコード信頼性を確保して手戻りを削減グリーン正常ランタイムエラーが存在しない static int int int void pointer_arithmetic (void) { array[100]; *p = array; i; for (i = 0; i < 100; i++) { *p = 0; p++; } レッドエラー実行される度にランタイムエラー if (get_bus_status() > 0) { if (get_oil_pressure() > 0) { *p = 5; } else { Dereference of local pointer p i++; (pointer to int 32, size: 32bits): } } Points to 4 bytes at offset 400 in グレーデッドコード無実行オレンジ Unproven 条件によってランタイムエラー buffer of 400 bytes, so is outside i = get_bus_status(); bounds. if (i >= 0) { *(p - i) = 10; } パープル Violation MISRA-C/C++, JSF++ } 変数値範囲ツールチップ 23

21 Polyspace Code Prover - ソフトウェアの安全性の確保 MISRA ルール違反の安全性の証明機能安全規格に準拠グローバル変数の同時アクセスの特定 MBD との統合による安全性の確保 24

22 MISRA ルール違反の安全性の証明 MISRA ルール違反安全性の証明 ( オーバーフロー無し ) Polyspace Code Prover MISRA ルール違反の正当化の根拠として Polyspace を活用可能 25

23 グローバル変数の同時アクセスの特定マルチタスク時のレビューを効率化対話的なレビュー手法グラフィカルなレビュー手法グリーン : 同時アクセスから保護グレー : 定義しているが未使用オレンジ : 競合の可能性あり 26

Polyspace Code Prover ISO26262適用 Table 8 Design principles for software unit

No implicit type conversions 1j No recursions (安全性要求レベル) A(低) B C D(高) + ++ ++ ++

software unit design and implementation ソフトウェアユニット設計の検証方法 Methods ASIL 再帰呼び出しの識別

24 Polyspace Code Prover ISO26262適用 Table 8 Design principles for software unit design and implementation ソフトウェアユニット設計と実装の基本原則 Methods MISRAルール違反の安全性の証明 ASIL 1g No implicit type conversions 1j No recursions (安全性要求レベル) A(低) B C D(高) 暗黙の型変換の禁止再帰呼び出しの禁止 + 強く推奨推奨 Table 9 Methods for the verification of software unit design and implementation ソフトウェアユニット設計の検証方法 Methods ASIL 再帰呼び出しの識別 1g Data flow analysis データフロー解析 (安全性要求レベル) A(低) B C D(高) 強く推奨推奨グローバル変数の同時アクセスの特定 27

25 規格準拠に向けて Polyspace製品で目標規格達成をアシストしますコーディング規約 MISRA-C MISRA-C++ JSF++ ソフトウェアメトリクス HIS Source Code Metrics 認証規格 DO-178B DO Qualification Kit IEC 61508, ISO 26262, EN IEC Certification Kit 28

26 モデルベースデザインとの統合 PolyspaceのSimulink連携機能でモデル修正が容易 Simulink 環境からPolyspace解析を実行 Polyspace解析結果を該当ブロックで強調表示ブロックにPolyspaceの注釈を追加 S-Functionコードの検証 MISRA C のチェック Polyspace 29

27 アジェンダ 1. サイバー攻撃の事例紹介 2. セキュリティ脆弱性の検出 3. ソフトウェアの安全性の証明 4. ユーザー事例 & まとめ 30

Polyspace ユーザー事例医療航空自動車など様々な分野で利用されています Miracor Eliminates Run-Time Errors and Reduces Testing Time for Class III Medical Device Software From a developer s perspective, the main advantage of

Polyspace Code Prover helps Miracor demonstrate this quality and correctness to the regulatory community, including the FDA, to prove that our device is safe.

html Solar Impulse Develops Advanced Solar-Powered Airplane From a developer s perspective, the main advantage of - Lars Schiemanck, Miracor Medical Systems https://jp.mathworks.

28 Polyspace ユーザー事例医療航空自動車など様々な分野で利用されています Miracor Eliminates Run-Time Errors and Reduces Testing Time for Class III Medical Device Software From a developer s perspective, the main advantage of Polyspace Code Prover is a higher level of quality and correctness in the code. Polyspace Code Prover helps Miracor demonstrate this quality and correctness to the regulatory community, including the FDA, to prove that our device is safe. - Lars Schiemanck, Miracor Medical Systems Solar Impulse Develops Advanced Solar-Powered Airplane From a developer s perspective, the main advantage of Polyspace Code Prover is a higher level of quality and correctness in the code. Polyspace Code Prover helps Miracor demonstrate this quality and correctness to the regulatory community, including the FDA, to prove that our device is safe. - Lars Schiemanck, Miracor Medical Systems 日産自動車ソフトウェアの信頼性を向上 Polyspace 製品によって高レベルなソフトウェアの信頼性を確保することができますこれは業界内の他のツールにはできないことです - 菊池光彦氏, 日産自動車課題ソフトウェア品質を向上させるために発見が困難なランタイムエラーを特定するソリューション MathWorks のPolyspace製品を使用して日産とサプライヤーのコードを包括的に解析する結果サプライヤーのバグを検出して評価ソフトウェアの信頼性が向上日産のサプライヤーが Polyspace 製品を採用 31

29 Polyspace まとめ静的解析によるコード検証でセキュリティと安全性の確保 Polyspace Bug Finder によるセキュリティ脆弱性の検出 Polyspace Code Prover による安全性の証明セキュリティ脆弱性とバグの早期検出あらゆる条件でコードの安全性を証明コーディングルールのチェックソフトウェアの安全性の確保セキュリティ項目のドキュメンテーション MISRAルール違反の安全性の証明推奨アクショングローバル変数の同時アクセスの特定機能安全規格のツール認証に対応 MBDとの統合による安全性の確保 32

30 Polyspace まとめ静的解析によるコード検証でセキュリティと安全性の確保 Polyspace Bug Finder によるセキュリティ脆弱性の検出 Polyspace Code Prover による安全性の証明セキュリティ脆弱性とバグの早期検出あらゆる条件でコードの安全性を証明コーディングルールのチェックソフトウェアの安全性の確保セキュリティ項目のドキュメンテーション MISRAルール違反の安全性の証明推奨アクショングローバル変数の同時アクセスの特定 MBDとの統合による安全性の確保機能安全規格のツール認証に対応 33

31 Polyspace の有効活用に向けて短期間で習得していただけるような教育カリキュラムをご提供します 34

ご清聴ありがとうございました Accelerating the pace of engineering and science 2018 The MathWorks, Inc. MATLAB and Simulink are registered trademarks of The MathWorks, Inc. See www.

32 ご清聴ありがとうございました Accelerating the pace of engineering and science 2018 The MathWorks, Inc. MATLAB and Simulink are registered trademarks of The MathWorks, Inc. See for a list of additional trademarks. Other product or brand names may be trademarks or registered trademarks of their respective holders. 35

MATLAB EXPO 2015 Japan 次世代モデルベース検証ソリューションでテスト・デバッグ改善

MATLAB EXPO 2015 Japan 次世代モデルベース検証ソリューションでテスト・デバッグ改善次世代モデルベース検証ソリューションでテストデバッグ改善 MathWorks Japan アプリケーションエンジニアリング部 ( 制御 ) リャンティファニー 2015 The MathWorks, Inc. 1 アジェンダはじめに検証作業におけるチャレンジ & 新しいソリューションまとめ 2 モデルベースデザイン / 開発 (MBD) が量産制御ソフト開発に求められる背景課題解決策効果