静的コード解析

静的コード解析  または静的プログラム解析  とは、コンピュータのソフトウェアの解析手法の一種であり、実行ファイルを実行することなく解析を行うこと。逆にソフトウェアを実行して行う解析を動的プログラム解析と呼ぶ。静的コード解析はソースコードに対して行われることが多いが、少数ながらオブジェクトコードに対して行う場合もある。また、この用語は以下に列挙するツールを使用した解析を意味することが多い。人間が行う作業はインスペクション、コードレビューなどと呼ぶ。日本語では静的コード分析とも訳される。

1. 概要
-----

ツールが行う静的コード解析の洗練度は、個々の文や宣言だけを検証するものから、プログラム全体を解析するものまで様々である。解析結果の利用も様々で、Lintのように単に指摘するだけのものから、形式手法を使ってそのプログラムの特性を数学的に証明するものまである。

ソフトウェア測定法やリバースエンジニアリングも静的解析の一部とみなすこともある。特に組み込みシステムの開発において、ソフトウェア測定法と静的コード解析が品質向上の一助として活用されることが多くなっている。

静的解析の商業利用が増えているのは、重要なコンピュータシステムで使用されるソフトウェアの検証や潜在的なセキュリティホールを検出する必要性が増大したことを意味する。以下のような分野で、複雑さを増していくソフトウェアの品質向上に静的コード解析が使われている。

医療用ソフトウェア - アメリカ食品医薬品局  は医療機器で静的コード解析が活用されているとしている。
原子力関連のソフトウェア - イギリスの Health and Safety Executive は原子炉保護系での静的コード解析の活用を推奨している。VDC Research が行った調査によれば、組み込みシステムのソフトウェア技術者の28.7%が静的コード解析ツールを既に使っており、39.7%が2年以内に使いたいと答えた。

アプリケーションのセキュリティの分野では Static Application Security Testing  という用語が使われている。

2. 形式手法
-------

形式手法は、ソフトウェアやハードウェアの解析に用いられる用語であり、厳密に数学的な手法によって解析結果を得ることを意味する。数学的手法としては、表示的意味論、公理的意味論、操作的意味論、抽象解釈などがある。

実行時エラーを全て検出することは不可能であることが証明されており、任意のプログラムが正しく動作するかエラーになるかを判定する機械的手法はない。これは1930年代のアラン・チューリングやライスの研究で判明した。決定不能な問題ではあるが、近似的な解でも有効である。

形式的な静的コード解析の実装方法には以下のようなものがある:

モデル検査は、有限の状態を持つシステムを対象とし、無限に状態を持つシステムを抽象化によって状態数を有限個に減らして行うこともある。
データフロー解析は、プログラムの各点で変数群の取りうる値についての情報を集める技法である。
抽象解釈は、プログラムの個々の文が抽象機械の状態に何らかの影響を与える様子をモデル化したものである。抽象機械は解析しやすいようになるべく単純化されるので、実際のプログラムを完全に表すわけではない。うまくいけば、抽象解釈は「健全」とされる。例えば、Frama-cやPolyspaceといったツールは、抽象解釈の技法を使っている。
表明をプログラム内で使うことは、ホーア論理で最初に示唆された。一部のプログラミング言語は表明をツールとしてサポートしている例えば、Adaのサブセットである[[:en:SPARK programming language。

3. 静的コード解析ツール
-------------

事前コンパイラは、言語仕様には適合しているもののロジックの正当性が疑わしいようなコードや、未定義動作を引き起こすようなコードを検出して、警告を出すものがほとんどである。ただし、コンパイラではカバーしきれない事項もあるため、独立した静的コード解析専用のツールを補助的に併用することも多い。統合開発環境に標準搭載されているものもあれば、プラグインやアドオンとして開発者が追加できるようになっているものもある。コードエディター上で問題のある個所をハイライト表示するなど、ソースコードをコンパイルすることなくリアルタイムに指摘してくれるものもある。

3.1. C言語とC++
------------

[1]
[2] 　→ CPA checker
Parasoft [3]
[4] 
[5] - 一部動的解析
[6]
[7]
[8] 
[9] 
[10] - ソースコード解析とリファクタリング・ブラウザ。プリプロセッサの構文も扱う。
[11] - コンパイル不要。ソースコードのみで解析可能。
[12] 
[13]
Fortify SCA
[14]  - C言語用だが、他の言語にも対応中。
Klocwork [15]
[16] MISRA主要メンバ
[17]
[18]
[19],[20]
富士通ソフトウェア [21]
[22]
[23]
[24] - Windows用のデバイスドライバを開発するのに使用するWDKの一部
[25]
[26] - C言語ソースチェッカー。主にLinuxカーネル用。
[27] 
[28]
[29] 
Visual Studio
[30]
Clang-Tidy
[31] 

3.2. C#
-------

Klocwork Insight
Visual Studio
[32]
Checkmarx CxSuite
[33]
[34]
Parasoft [35]
Fortify SCA

3.3. CoffeeScript
-----------------

Sider 

3.4. FORTRAN
------------

[36]

3.5. HTML
---------

Fortify SCA
W3C [37]
[38]

3.6. Go
-------

Sider 
[39]

3.7. Java
---------

[40]
anyWarp CodeDirector
[41]
[42] - 単体テスト網羅率を自動計算
[43]
Checkmarx CxSuite
[44]
[45]
Fortify SCA
[46]
[47]
Klocwork Insight
Oracle [48]
[49]
RIPS
[50]
[51]
[52]
富士通ソフトウェア [53]
Parasoft [54]
IntelliJ IDEA

3.8. AndroidのJava言語
-------------------

[55]
Checkmarx CxSuite
Fortify SCA
[56]
Android Studio

3.9. Perl
---------

Checkmarx CxSuite
[57]
[58]

3.10. PHP
---------

php は -l をつけて起動すれば Lint 風の基本的なチェックを行う。例えば: for i in `find . -name \*.php`; do php -l $i | grep -v "No syntax errors"; done
Sider 
Checkmarx CxSuite
[59]
RIPS
Fortify SCA
PhpMetrics
[60]

3.11. Python
------------

Sider 
Fortify SCA
[61]
[62]
[63]
[64]

3.12. JSP
---------

Checkmarx CxSuite
Fortify SCA
RIPS

3.13. VB.NET
------------

Checkmarx CxSuite
Fortify SCA
Parasoft dotTEST
Visual Studio
[65]

3.14. ASP.NET
-------------

Checkmarx CxSuite
Fortify SCA

3.15. Cold Fusion
-----------------

Fortify SCA

3.16. SAP の ABAP
----------------

Fortify SCA

3.17. SQL
---------

Fortify SCA

3.18. JavaScript
----------------

Sider
Checkmarx CxSuite
Fortify SCA
Parasoft [66]
[67]
ESLint

3.19. ASP
---------

Checkmarx CxSuite
Fortify SCA

3.20. COBOL
-----------

Fortify SCA

3.21. WSDL
----------

[68] 
Parasoft [69]

3.22. Ruby
----------

Sider 
Checkmarx CxSuite
[70]

3.23. Objective-C
-----------------

Checkmarx CxSuite
[71]

4. 脚注
-----

4.1. 注釈
-------

4.2. 出典
-------

5. 参考文献
-------

[72] for [73]’s Stanford CS295 course.
Nathaniel Ayewah, David Hovemeyer, J. David Morgenthaler, John Penix, William Pugh, "[74]," IEEE Software, vol. 25, no. 5, pp.   22–29, Sep./Oct. 2008,
[75] International Winter School on Semantics and Applications 2003, by [76]

6. 関連項目
-------

動的プログラム解析
シェープ解析
プログラム意味論
形式的検証
ソフトウェアテスト
ドキュメンテーションジェネレータ

7. 外部リンク
--------

[77]
[78]
[79] by Jens Palsberg
[80]
[81]
[82]
[83]