静的コード解析
静的コード解析の最新ニュースをまとめて検索！
静的コード解析（Static Code Analysis）とは、コンピュータのソフトウェアの解析手法の一種であり、実行ファイルを実行することなく解析を行うこと。逆にソフトウェアを実行して行う解析を動的プログラム解析と呼ぶ。静的コード解析はソースコードに対して行われることが多く、少数ながらオブジェクトコードに対して行う場合もある。また、この用語は以下に列挙するツールを使用した解析を意味することが多い。人間が行う作業はインスペクション、コードレビューなどと呼ぶ。
ツールが行う静的コード解析の洗練度は、個々の文や宣言だけを検証するものから、プログラム全体を解析するものまで様々である。解析結果の利用も様々で、Lintのように単に指摘するだけのものから、形式手法を使ってそのプログラムの特性を数学的に証明する（仕様記述と振る舞いが一致しているかどうかを検証する）ものまである。
ソフトウェア測定法やリバースエンジニアリングも静的解析の一部とみなすこともある。
静的解析の商業利用は、重要なコンピュータシステムで使用されるソフトウェアの検証や潜在的なセキュリティホールを検出する必要性が増大したことを意味する。
目次 |
[編集] 形式手法
形式手法は、ソフトウェアやハードウェアの解析に用いられる用語であり、厳密に数学的な手法によって解析結果を得ることを意味する。数学的手法としては、表示的意味論、公理的意味論、操作的意味論、抽象解釈などがある。
実行時エラーを全て検出することは不可能であることが証明されており、任意のプログラムが正しく動作するかエラーになるかを判定する機械的手法はない。これは1930年代のアラン・チューリングやライスの研究で判明した（チューリングマシンの停止問題およびライスの定理）。決定不能な問題ではあるが、近似的な解でも有効である。
形式的な静的コード解析の実装方法には以下のようなものがある:
- モデル検査は、有限の状態を持つシステムを対象とし、無限に状態を持つシステムを抽象化によって状態数を有限個に減らして行うこともある。
- 抽象解釈は、プログラムの個々の文が抽象機械の状態に何らかの影響を与える様子をモデル化したものである（つまり、ソフトウェアを個々の文の数学的属性と宣言に基づいて「実行」する）。
[編集] 静的コード解析ツール
- Fortify SCA （多言語(17)混在のシステムでの横断的解析が可能）
- Klocwork Insight （商用）
- anyWarp CodeDirector for C/C++ (商用)
- BLAST
- C++test (商用)
- C99parser (GPL)
- CCured BSDライセンス。一部動的解析。
- Coverity Prevent (商用)
- Cqual
- CScout ソースコード解析とリファクタリング・ブラウザ。プリプロセッサの構文も扱う。
- Flawfinder (GPL)
- introspector (GPL) C言語用だが、他の言語にも対応中。
- MOPS （BSD風ライセンス）
- OpenC++
- QAC,QAC++ (商用)
- PGRelief (商用)
- PMD's Copy/Paste Detector
- PolySpace (商用)
- PREfast ドライバ開発用 DDK の一部（マイクロソフト）
- Review-C (商用)
- Smatch C言語ソースチェッカー。主にLinuxカーネル用。
- Sparse (GPL)
- Stacktool
- Splint (GPL)
- Visual Studio 2005 Team Edition のみ。
- Fortify SCA （多言語(17)混在のシステムでの横断的解析が可能）
- Klocwork Insight （商用）
- Visual Studio - Visual Studio 2005 Team Suite または Team Edition for Software Developers のみ。
- Coverity Prevent (商用)
- DevMetrics and DevAdvantage
- W3C Markup Validation Service
- Fortify SCA （多言語(17)混在のシステムでの横断的解析が可能）
- Fortify SCA （多言語(17)混在のシステムでの横断的解析が可能、FindBugsとの連携も可能）
- Klocwork Insight （商用）
- AntiC
- anyWarp CodeDirector (商用)
- Checkstyle
- Cobertura - 単体テスト網羅率を自動計算
- Coverity Prevent (商用)
- ESC/Java2
- FindBugs
- Hammurapi
- Oracle JDeveloper
- PMD
- Spoon
- WALA
- PHP は -l をつけて起動すれば Lint 風の基本的なチェックを行う。例えば:
for i in `find . -name \*.php`; do php -l $i | grep -v "No syntax errors"; done - PMD's Copy/Paste Detector
- Fortify SCA （多言語(17)混在のシステムでの横断的解析が可能）
- Fortify SCA （多言語(17)混在のシステムでの横断的解析が可能）
- Fortify SCA （多言語(17)混在のシステムでの横断的解析が可能）
- Fortify SCA （多言語(17)混在のシステムでの横断的解析が可能）
- Fortify SCA （多言語(17)混在のシステムでの横断的解析が可能）
- Fortify SCA （多言語(17)混在のシステムでの横断的解析が可能）
- Fortify SCA （多言語(17)混在のシステムでの横断的解析が可能）
- Fortify SCA （多言語(17)混在のシステムでの横断的解析が可能）
- Fortify SCA （多言語(17)混在のシステムでの横断的解析が可能）
- WSDL validator Eclipse.org
[編集] 関連項目
[編集] 外部リンク
- The SAMATE Project
- ASTRÉE project
- PREfix マイクロソフトのプロジェクト（ppt形式）
- Type Inference and Static Analysis for Object-Oriented Software by Jens Palsberg
- Securing Web Application Code by Static Analysis and Runtime Protection
最終更新 2009年10月28日 (水) 03:28 （日時は個人設定で未設定ならばUTC）。
【静的コード解析】変更履歴
