静的コード解析

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

概要

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

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

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

医療用ソフトウェア - アメリカ食品医薬品局 (FDA) は医療機器で静的コード解析が活用されているとしている^[4]。
原子力関連のソフトウェア - イギリスの Health and Safety Executive は(原子炉保護系)（英語版）での静的コード解析の活用を推奨している^[5]。

VDC Research が行った調査（2012年）によれば、組み込みシステムのソフトウェア技術者の28.7%が静的コード解析ツールを既に使っており、39.7%が2年以内に使いたいと答えた^[6]。

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

形式手法

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

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

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

モデル検査は、有限の状態を持つシステムを対象とし、無限に状態を持つシステムを抽象化によって状態数を有限個に減らして行うこともある。
データフロー解析は、プログラムの各点で変数群の取りうる値についての情報を集める技法である。
抽象解釈は、プログラムの個々の文が抽象機械の状態に何らかの影響を与える様子をモデル化したものである（つまり、ソフトウェアを個々の文の数学的属性と宣言に基づいて「実行」する）。抽象機械は解析しやすいようになるべく単純化されるので、実際のプログラムを完全に表すわけではない（もとのシステムで真である属性が抽象システムで常に真とは限らない）。うまくいけば、抽象解釈は「健全」とされる（抽象システムで真である全属性はもとのシステムでも真だといえる）^[7]。例えば、Frama-cやPolyspaceといったツールは、抽象解釈の技法を使っている。
表明をプログラム内で使うことは、ホーア論理で最初に示唆された。一部のプログラミング言語は表明をツールとしてサポートしている（例えば、AdaのサブセットであるSPARK、ESC/JavaやESC/Java2を使った Java Modeling Language (JML)、C言語を ACSL (ANSI/ISO C Specification Language) で拡張する Frama-c WP（weakest precondition、最弱事前条件）プラグインがある）。

静的コード解析ツール

C言語とC++

anyWarp CodeDirector for C/C++ （商用, 日立ソリューションズ）
BLAST (Apache License)　→ CPA checker
Parasoft C++test （商用, Parasoft）
C99parser (GPL)
CCured - 一部動的解析（BSDライセンス）
CodeSonar （商用）
Coverity （商用）
cppcheck (GPL)
Cqual (GPL)
CScout - ソースコード解析とリファクタリング・ブラウザ。プリプロセッサの構文も扱う。
Checkmarx CxSuite - コンパイル不要。ソースコードのみで解析可能。（商用）
Flawfinder (GPL)
Goanna （商用）
Fortify SCA ^[8] （商用）
introspector (GPL) - C言語用だが、他の言語にも対応中。
Klocwork Insight （商用）
LDRA MISRA主要メンバ（商用）
MOPS （BSD風ライセンス）
OpenC++
QAC,QAC++ （商用）
富士通ソフトウェア PGRelief C/C++ （商用）
PMD's Copy/Paste Detector （BSD風ライセンス）
PolySpace （商用）
PREfast - Windows用のデバイスドライバを開発するのに使用するWDKの一部
Review-C （商用）
Smatch - C言語ソースチェッカー。主にLinuxカーネル用。
Sparse (GPL)
Stacktool
Splint (GPL)
Visual Studio
Clang Static Analyzer （BSD風ライセンス）
AdLint (GPL)

C#

Klocwork Insight （商用）
Visual Studio
Coverity （商用）
Checkmarx CxSuite （商用）
DevMetrics and DevAdvantage
Julia （商用）
Parasoft dotTEST （商用）
Fortify SCA ^[8] （商用）

CoffeeScript

Sider (商用)

FORTRAN

FTNCHEK

HTML

Fortify SCA ^[8] （商用）
W3C Markup Validation Service
SonarQube

Go

Sider (商用)
SonarQube

Java

AntiC
anyWarp CodeDirector （商用）
Checkstyle
Cobertura - 単体テスト網羅率を自動計算
Coverity （商用）
Checkmarx CxSuite （商用）
ESC/Java2
FindBugs
Fortify SCA ^[8] （商用）
Hammurapi
Julia （商用）
Klocwork Insight （商用）
Oracle JDeveloper
PMD
RIPS （商用）
SonarQube
Spoon
WALA
富士通ソフトウェア PGRelief J （商用）
Parasoft Jtest （商用）

AndroidのJava言語

Coverity （商用）
Checkmarx CxSuite （商用）
Fortify SCA ^[8] （商用）
Julia （商用）

Perl

Checkmarx CxSuite （商用）
fluff
Perl::Critic

PHP

php は -l をつけて起動すれば Lint 風の基本的なチェックを行う。例えば: for i in `find . -name \*.php`; do php -l $i | grep -v "No syntax errors"; done
Sider (商用)
Checkmarx CxSuite （商用）
PMD's Copy/Paste Detector
RIPS （商用）
Fortify SCA ^[8] （商用）
PhpMetrics^{[※ 1]}
SonarQube

Python

Sider (商用)
Fortify SCA ^[8] （商用）
PyChecker
Pyflakes
PyLint
SonarQube

JSP

Checkmarx CxSuite （商用）
Fortify SCA ^[8] （商用）
RIPS （商用）

VB.NET

Checkmarx CxSuite （商用）
Fortify SCA ^[8] （商用）
Parasoft dotTEST （商用）
Visual Studio
SonarQube（商用）

ASP.NET

Checkmarx CxSuite （商用）
Fortify SCA ^[8] （商用）

Cold Fusion

Fortify SCA ^[8] （商用）

SAP の ABAP

Fortify SCA ^[8] （商用）

SQL

Fortify SCA ^[8] （商用）

JavaScript

Sider (商用)
Checkmarx CxSuite （商用）
Fortify SCA ^[8] （商用）
Parasoft WebTest （商用）
SonarQube

ASP

Checkmarx CxSuite （商用）
Fortify SCA ^[8] （商用）

COBOL

Fortify SCA ^[8] （商用）

WSDL

WSDL validator (Eclipse)
Parasoft SOAtest （商用）

Ruby

Sider (商用)
Checkmarx CxSuite （商用）
SonarQube

Objective-C

Checkmarx CxSuite （商用）
SonarQube（商用）

注釈

^ PhpMetrics, static analysis for PHP - by Jean-François Lépine

出典

^ Wichmann, B. A., A. A. Canning, D. L. Clutterbuck, L. A. Winsbarrow, N. J. Ward, and D. W. R. Marsh. "Industrial Perspective on Static Analysis". Software Engineering Journal Mar. 1995: 69-75
^ Software Quality Objectives for Source Code. Proceedings Embedded Real Time Software and Systems 2010 Conference, ERTS2, Toulouse, France: Patrick Briand, Martin Brochet, Thierry Cambois, Emmanuel Coutenceau, Olivier Guetta, Daniel Mainberte, Frederic Mondot, Patrick Munier, Loic Noury, Philippe Spozio, Frederic Retailleau
^ Improving Software Security with Precise Static and Runtime Analysis, Benjamin Livshits, section 7.3 "Static Techniques for Security," Stanford doctoral thesis, 2006.
^ FDA (2010年9月8日). “Infusion Pump Software Safety Research at FDA”. Food and Drug Administration. 2010年9月9日閲覧。
^ Computer based safety systems - technical guidance for assessing software aspects of digital computer based protection systems,
^ VDC Research (2012年2月1日). “Automated Defect Prevention for Embedded Software Quality”. VDC Research. 2012年4月10日閲覧。
^ Jones, Paul (2010年2月9日). “A Formal Methods-based verification approach to medical device software analysis”. Embedded Systems Design. 2010年9月9日閲覧。
^ ^a ^b ^c ^d ^e ^f ^g ^h ⁱ ^j ^k ^l ^m ⁿ ^o ^p 多言語(17)混在のシステムでの横断的解析が可能

参考文献

Syllabus and readings for Alex Aiken’s Stanford CS295 course.
Nathaniel Ayewah, David Hovemeyer, J. David Morgenthaler, John Penix, William Pugh, "Using Static Analysis to Find Bugs," IEEE Software, vol. 25, no. 5, pp. 22–29, Sep./Oct. 2008, doi:10.1109/MS.2008.130
Brian Chess, Jacob West (Fortify Software) (2007). Secure Programming with Static Analysis. Addison-Wesley. ISBN (978-0-321-42477-8)
Flemming Nielson, Hanne R. Nielson, Chris Hankin (1999, corrected 2004). Principles of Program Analysis. Springer. ISBN (978-3-540-65410-0)
"Abstract interpretation and static analysis," International Winter School on Semantics and Applications 2003, by David A. Schmidt

外部リンク

The SAMATE Project
ASTRÉE project
Type Inference and Static Analysis for Object-Oriented Software by Jens Palsberg
Securing Web Application Code by Static Analysis and Runtime Protection
Integrate static analysis into a software development process
Code Quality Improvement - Coding standards conformance checking (DDJ)
.NET Static Analysis (InfoQ)

[9] PhpMetrics, static analysis for PHP - by Jean-François Lépine

[1] Wichmann, B. A., A. A. Canning, D. L. Clutterbuck, L. A. Winsbarrow, N. J. Ward, and D. W. R. Marsh. "Industrial Perspective on Static Analysis". Software Engineering Journal Mar. 1995: 69-75

[2] Software Quality Objectives for Source Code. Proceedings Embedded Real Time Software and Systems 2010 Conference, ERTS2, Toulouse, France: Patrick Briand, Martin Brochet, Thierry Cambois, Emmanuel Coutenceau, Olivier Guetta, Daniel Mainberte, Frederic Mondot, Patrick Munier, Loic Noury, Philippe Spozio, Frederic Retailleau

[3] Improving Software Security with Precise Static and Runtime Analysis, Benjamin Livshits, section 7.3 "Static Techniques for Security," Stanford doctoral thesis, 2006.

[4] FDA (2010年9月8日). “Infusion Pump Software Safety Research at FDA”. Food and Drug Administration. 2010年9月9日閲覧。

[5] Computer based safety systems - technical guidance for assessing software aspects of digital computer based protection systems,

[6] VDC Research (2012年2月1日). “Automated Defect Prevention for Embedded Software Quality”. VDC Research. 2012年4月10日閲覧。

[7] Jones, Paul (2010年2月9日). “A Formal Methods-based verification approach to medical device software analysis”. Embedded Systems Design. 2010年9月9日閲覧。

[FSCA-8] ^ ^a ^b ^c ^d ^e ^f ^g ^h ⁱ ^j ^k ^l ^m ⁿ ^o ^p 多言語(17)混在のシステムでの横断的解析が可能

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[※ 1]

ウィキペディア	ランダム
毎日	カテゴリ