静的コード解析

出典: フリー百科事典『ウィキペディア（Wikipedia）』

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

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

ソフトウェアメトリックやリバースエンジニアリングも静的解析の一部とみなすこともある。

静的解析の商業利用は、重要なコンピュータシステムで使用されるソフトウェアの検証や潜在的なセキュリティホールを検出する必要性が増大したことを意味する。

[編集] 形式手法

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

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

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