次世代システムに求められるソフトウェア検証技術～静的解析の価値と有効性～

MathWorks Japan
Application Engineering
Application Engineer
能戸 フレッド ・ Fred Noto

© 2017 The MathWorks, Inc.
1

Polyspace®のコード証明

Polyspaceは品質保証の上、検証工数の削減に貢献します

コード内のエラーをどう検出しますか？
• Polyspaceはコードの安全性を保証するための静的解析を提供します• コードの品質を証明することにより、検証プロセスの効率化に繋がります2

アジェンダ

次世代システムの検証に関する課題～動的テストと静的解析の目的～

Polyspace静的解析ソリューションの価値と有効性



ユーザ事例 ＆ まとめ

3

次世代システムのトレンド
IoT

自律システムスマートシステム

新機能

高機能

高性能

等々．．．
市場への早期参入

品質向上

等々．．．

コンシューマー4次世代システムのトレンド

多数のチャレンジ！ セキュリティ脆弱性
自律システムIoTシステムの複雑化
スマートシステム
等々．．．
ソフトウェアの大規模化
新機能

高機能
市場への早期参入
スケジュールの最小化品質の確保
等々．．．
高性能
品質向上

複雑・高品質ソフトウェアをより早く開発！

効率的な検証手法が必須！
コンシューマー開発者・エンジニア
5次世代システムの検証に関する課題
多くの検証目的が存在し、テスト時間が膨張する

動的テスト• 要求仕様通りの設計かを確認• 要求仕様に問題がないことを確認

CC
C
機能の検証

• エラー・欠陥の存在を確認• スタンダード準拠の確認!

Cソフトの検証6

動的テスト実行に関する課題

動的テストは動作確認で必要だが、エラー検証には非効率
従来のソフト検証手法：動的テスト
テスト
ケース 1

問題点：

テスト
ケース 2

テスト
ケース 3

エラー検出の遅れ

リワーク

テスト
ケース 4

テスト
ケース 5

納期の延期

ユニットテスト＆統合テスト…

納品物でエラーが発生

多数の繰り返し作業

7

複雑系の故障
Ariane-5, ロケット
– エラータイプ ： オーバーフロー– 結果 ： ロケットの破壊

USS Yorktown,タイコンデロガ級ミサイル巡洋艦– エラータイプ ： ゼロ割り
– 結果 ： 巡洋艦の推進システムが故障

Therac-25, 放射線療法機器– エラータイプ ： オーバーフローと競合状態– 結果 ： 数人の患者を死亡させた
8

ソフトウェア品質確保の効率化に向けて
提案：静的解析によるソフトウェア品質の確保

従来的なテスト手法  テストケースの作成、実行、確認が必要

カバレッジのためのテスト

全ての欠陥を検出するためのテスト

x / (x - y)
• 未初期化変数• オーバーフロー• ゼロ除算int32 の場合、4.61 x 1018 のテストケースが可能

全て可能なテストケースの作成・実行・レビューは不可能！
9ソフトウェア検証のストリームライン
検証目的により適切な検証手法を使用してプロセスを効率化

動的テスト

静的検証

• 要求仕様通りの設計かを確認• 要求仕様に問題がないことを確認

CCC
機能チェック• エラー・欠陥の存在を確認• スタンダード準拠の確認!

C
ソフト品質10

静的解析の種類について
Polyspaceはコード証明を含むソフト品質確保のソリューション

静的解析手法の種類：
シンタックス解析

制御フロー解析
モデル検査
セマンティックス解析
データフロー解析
形式手法

手法の目的：
コーディング規約への準拠コードメトリクス測定
欠陥の検出

コード証明

11

https://www.mathworks.com/company/events/conferences/matlab-conference-switzerland/2015/proceedings/solar-impulse-firstround-the-world-solar-flight-attempt.pdf

12アジェンダ

次世代システムの検証に関する課題～動的テストと静的解析の目的～

Polyspace静的解析ソリューションの価値と有効性



ユーザ事例 ＆ まとめ

13

Polyspaceによる検証作業の効率化：活用例

早期段階でのコーディング
ルールチェックと、バグやセキュリティ脆弱性の検出

コードレビューの効率化

潜在的な構造的エラーを予防

14

Polyspace Bug FinderTM のスピーディー解析


バグ検出– コード作成後、すぐに欠陥を検出・修正

コーディングルールチェック– エラー予防と再利用性向上– MISRA準拠を確認



コードメトリックス解析

時間を掛けずに大部分のバグを識別

コード作成– コードの複雑度を測定
開発プロセスの上流で不具合を発見！
コードを統合前に多くの欠陥を修正！
コード開発の効率に繋がる！

修正Bug Finder解析
レポート自動生成

素早い欠陥検出・修正を可能とするPolyspace Bug Finder

15

Polyspace Bug Finder：検出項目の種類
数式エラー
 静的メモリーエラー
 動的メモリーエラー
 プログラミングエラー
 データフローエラー
 同時実行 セキュリティ
 汚染されたデータ
 その他


Polyspace Bug Finder GUI16

Polyspace Bug Finder：検出項目リスト（1/2）
Numerical
1. Integer division by zero
2. Float division by zero
3. Float conversion overflow
4. Integer conversion overflow
5. Unsigned integer conversion
overflow
6. Sign change integer
conversion overflow
7. Float overflow
8. Integer overflow
9. Unsigned integer overflow
10. Invalid use of std. library
integer routine
11. Invalid use of std. library
float routine
12. Shift of a negative value
13. Shift operation overflow

Dataflow
1. Write without further read
2. Non-initialized variable
3. Non-initialized pointer
4. Variable shadowing
5. Missing or invalid returnstatement
6. Unreachable code
7. Dead code
8. Useless if
9. Partially access array
10. Uncalled function
11. Pointer to non initialized
value converted to const
pointer
12. Code deactivated byconstant false condition

Static memory
1. Array access out of bounds
2. Null pointer3. Buffer overflow fromincorrect string format
specifier4. Destination buffer overflow instring manipulation
5. Destination buffer underflow
in string manipulation
6. Pointer access out of bounds
7. Pointer or reference to stackvariable leaving scope
8. Unreliable cast of function
pointer
9. Unreliable cast of pointer10. Invalid use of std. librarymemory routine
11. Invalid us of standard librarystring routine
12. Arithmetic operation with
NULL pointer13. Use of path manipulation
function without maximum
sized buffer checking
14. Wrong allocated object sizefor cast

Programming
1. Assertion
2. Bad file access mode orstatus
3. Call to memset with
unintended value
4. Declaration mismatch
5. Exception caught by value
6. Exception handler hidden by
previous handler
7. Format string specifiers andarguments mismatch
8. Improper array initialization
9. Incorrect pointer scaling
10. Invalid assumptions about
memory organization
11. Invalid use of == (equality)
operator
12. Invalid use of = (assignment)
operator
13. Invalid use of floating pointoperation
14. Invalid use of standard
library routine

Invalid va_list argument
16. Copy of overlapping memory
17. Missing null in string array
18. Modification of internal buffer
returned from nonreentrant standardfunction
19. Overlapping assignment
20. Possible misuse of sizeof
21. Possibly unintended evaluation ofexpression because of operator
precedence rules
22. Qualifier removed in conversion
23. Standard function call with incorrect
arguments
24. Use of memset with size argumentzero
25. Wrong type used in sizeof
26. Writing to const qualified object
27. Variable length array with
nonpositive size
15.

17Polyspace Bug Finder：検出項目リスト（2/2）
Concurrency
1. Data race
2. Data race including atomicoperations
3. Deadlock
4. Double lock5. Double unlock
6. Missing lock
7. Missing unlock
Resource management
1. Closing a previously closed
resource
2. Resource leak
3. Use of previously closed
resource
4. Writing to read-only
resource
Dynamic memory
1. Use of previously freedpointer2. Unprotected dynamic
memory allocation
3. Release of previously
deallocated pointer4. Invalid free of pointer5. Memory leak
6. Invalid deletion of pointerTainted data
1. Array access with taintedindex
2. Command executed fromexternally controlled path
3. Execution of externallycontrolled command
4. Host change using
externally controlledelements
5. Library loaded fromexternally controlled path
6. Loop bounded with taintedvalue
7. Memory allocation withtainted size
8. Pointer dereference withtainted offset
9. Tainted division operand
10. Tainted modulo operand
11. Tainted NULL or non-nullterminated string
12. Tainted sign change
conversion
13. Tainted size of variable
length array
14. Tainted string format
15. Use of externally controlledenvironment variable
16. Use of tainted pointerObject oriented
1. *this not returned in copy
assignment operator
2. Base class assignment operator
not called
3. Base class destructor not virtual
4. Copy constructor not called ininitialization list
5. Incompatible types prevent
overriding
6. Member not initialized inconstructor
7. Missing explicit keyword
8. Missing virtual inheritance
9. Object slicing
10. Partial override of overloaded
virtual functions
11. Return of non const handle toencapsulated data member
12. Self assignment not tested inoperator

Other
1. Invalid use of other standard
library routine
2. Large pass-by-value argument
3. Assertion
4. Format string specifiers andarguments mismatch
5. Line with more than one
statement

Security
1. File access between time of check
and use (TOCTOU)
2. File manipulation after chroot
without chdir
3. Use of non-secure temporary file
4. Vulnerable path manipulation
5. Vulnerable permission
assignments
6. Function pointer assigned withabsolute address
7. Incorrect order of network
connection operations
8. Mismatch between data length andsize
9. Missing case for switch condition
10. Sensitive data printed out11. Sensitive heap memory not cleared
before release
12. Umask used with chmod-style
arguments
13. Uncleared sensitive data in stack
14. Unsafe standard encryptionfunction
15. Unsafe standard function
16. Use of dangerous standard
function

Use of obsolete standard function
18. Deterministic random output fromconstant seed
19. Predictable random output frompredictable seed
20. Vulnerable pseudo-random
number generator
21. Execution of a binary from a
relative path can be controlled by
an external actor
22. Load of library from a relative pathcan be controlled by an external
actor
17.

18

Polyspaceによる検証作業の効率化：活用例

早期段階でのコーディング
ルールチェックと、バグやセキュリティ脆弱性の検出

コードレビューの効率化

潜在的な構造的エラーを予防

19

コードレビューの課題
コードレビューでのランタイムエラー検出は高コストで全てカバーできないstatic void pointer_arithmetic (void) {int array[100];int *p = array;
int i;for (i = 0; i < 100; i++) {*p = 0;p++;}if (get_bus_status() > 0) {if (get_oil_pressure() > 0) {*p = 5;} else {i++;}}

下記のような情報がありましたら如何でしょうか？
Pointer ‘p’ (pointer to int32, size 32bits)
Pointer is not null
Points to 4 bytes at offset of 400 in buffer of 400 bytes, so is outside bounds
Pointer may point to ‘array’, local to function ‘pointer_arithmetic’.

i = get_bus_status();if (i >= 0) {*(p - i) = 10;}}20

Polyspace Code ProverTMでコードの正しさを証明
Quality（品質）– ランタイムエラーの証明– 測定、向上、管理Usage（使用方法）– コンパイル、プログラム実行、テストケースは不要– 対応言語：C/C++/Ada



Process（プロセス）– ランタイムエラーの早期検出– 自動生成コード、ハンドコードの解析可能

グリーン：正常ランタイムエラーが存在しない

static void pointer_arithmetic (void) {int array[100];int *p = array;
int i;for (i = 0; i < 100; i++) {*p = 0;p++;
variable ‘I’ (int32): [0 .. 99]}
assignment of ‘I’ (int32): [1 .. 100]

レッド：エラー
実行される度にランタイムエラー

if (get_bus_status() > 0) {if (get_oil_pressure() > 0) {*p = 5;} else {i++;}}グレー：デッドコード
無実行

オレンジ：Unproven
条件によってランタイムエラー

i = get_bus_status();– コードの信頼性を測定

if (i >= 0) {*(p - i) = 10;}

パープル：Violation

実機実験前にコード信頼性を確保して手戻りを削減

MISRA-C/C++, JSF++}

変数値範囲
ツールチップPolyspaceは全ての実行パスの結果を証明する！

21

Polyspace Code ProverのKey Point“実行パス” x “変数レンジ” を検証して全てのテストケース実行に同等！
 抽象解釈 （abstract interpretation） により“ランタイムエラーフリー” なコードを証明します– コードの正しさの数学的な証明

不具合の不在をPROVEする事がPolyspaceの特徴
22

Polyspaceによる検証作業の効率化：活用例

早期段階でのコーディング
ルールチェックと、バグやセキュリティ脆弱性の検出

コードレビューの効率化

潜在的な構造的エラーを予防

23

Polyspaceによる同時実行問題の特定
ソフトウェア内のグローバル・共有変数の使用をレビューを加速化
対話的なレビュー手法

グラフィカルなレビュー手法

24

Polyspaceによる検証作業の効率化：活用例

早期段階でのコーディング
ルールチェックと、バグやセキュリティ脆弱性の検出

コードレビューの効率化

潜在的な構造的エラーを予防

25

Polyspaceは下記の検証作業を加速化します
検証プロセスを効率化する静的解析のソリューションMISRAチェック

ISO、IEC、DO認証

コーディングルール準拠

認証サポート

設計・構造の最適化

バグがないソフトを確保

コードメトリクス

コード証明

コード品質の測定

動的テストの工数を削減

包括的な静的解析

ソフトウェアロバスト性の解析
26

アジェンダ

次世代システムの検証に関する課題～動的テストと静的解析の目的～

Polyspace静的解析ソリューションの価値と有効性



ユーザ事例 ＆ まとめ27

Polyspaceユーザー事例

http://www.mathworks.com/tagteam/77497_91488v01_Nissan_UserStory_final.pdf

https://www.mathworks.com/company/events/conferences/automotive-conferencemichigan/2015/proceedings/introducing-polyspace-products-into-software-development-process.pdf

28

Polyspaceをどう活用しますか？

早期段階でのコーディングルール
チェックと、バグやセキュリティ脆弱性の検出

潜在的な構造的エラーを予防

コードレビューの効率化

認証とレポート生成29

最後に．．．

Polyspaceの評価にご興味がありましたらご連絡ください（fred.noto@mathworks.co.jp）

Polyspace詳細にご興味がありましたら展示ブースにお立寄りください30

Thank You For Your Attention

ご清聴ありがとうございました© 2017 The MathWorks, Inc. MATLAB and Simulink are registered trademarks of The
MathWorks, Inc. See www.mathworks.com/trademarks for a list of additional
trademarks. Other product or brand names may be trademarks or registeredtrademarks of their respective holders.

31