静的コード解析

出典: フリー百科事典『ウィキペディア(Wikipedia)』
移動: 案内検索

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

概要[編集]

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

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

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

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

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

形式手法[編集]

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

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

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

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

静的コード解析ツール[編集]

C言語とC++[編集]

C#[編集]

FORTRAN[編集]

HTML[編集]

AndroidのJava言語[編集]

  • Coverity Quality Advisor (商用)
  • CxSuite コンパイル不要。ソースコードのみで解析可能。
  • Fortify SCA (多言語(19)混在のシステムでの横断的解析が可能、FindBugsとの連携も可能)[8]

Java[編集]

Perl[編集]

PHP[編集]

  • php は -l をつけて起動すれば Lint 風の基本的なチェックを行う。例えば: for i in `find . -name \*.php`; do php -l $i | grep -v "No syntax errors"; done
  • CxSuite コンパイル不要。ソースコードのみで解析可能。
  • PMD's Copy/Paste Detector
  • Fortify SCA [8]

Python[編集]

JSP[編集]

VB.NET[編集]

ASP.NET[編集]

Cold Fusion[編集]

SAP の ABAP[編集]

  • Fortify SCA (多言語(19)混在のシステムでの横断的解析が可能、SAP Workbenchとの連携も可能)[8]

SQL[編集]

JavaScript[編集]

ASP[編集]

COBOL[編集]

WSDL[編集]

Ruby[編集]

  • CxSuite コンパイル不要。ソースコードのみで解析可能。

Objective-C[編集]

  • CxSuite コンパイル不要。ソースコードのみで解析可能。

脚注[編集]

  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日閲覧。
  8. ^ a b c d e f g h i j k l m n o 多言語(17)混在のシステムでの横断的解析が可能

参考文献[編集]

関連項目[編集]

外部リンク[編集]