静的コード解析
静的コード解析 (せいてきコードかいせき、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
HTML
- Fortify SCA [8] （商用）
- W3C Markup Validation Service
- SonarQube
Java
Perl
- Checkmarx CxSuite （商用）
- fluff
- Perl::Critic
PHP
JSP
- Checkmarx CxSuite （商用）
- Fortify SCA [8] （商用）
- RIPS （商用）
VB.NET
ASP.NET
- Checkmarx CxSuite （商用）
- Fortify SCA [8] （商用）
Cold Fusion
- Fortify SCA [8] （商用）
SAP の ABAP
- Fortify SCA [8] （商用）
SQL
- Fortify SCA [8] （商用）
ASP
- Checkmarx CxSuite （商用）
- Fortify SCA [8] （商用）
COBOL
- Fortify SCA [8] （商用）
WSDL
- WSDL validator (Eclipse)
- Parasoft SOAtest （商用）
Objective-C
- Checkmarx CxSuite （商用）
- SonarQube（商用）
出典
- 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日閲覧。
- 多言語(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)
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.