静的プログラム解析

コンピュータ科学において、静的プログラム解析（静的解析または静的シミュレーションとも呼ばれる）は、プログラムを実行せずに実行されるコンピュータプログラムの解析であり、統合環境でプログラムの実行中に実行される動的プログラム解析とは対照的である。^{[ 1 ] [ 2 ]}

この用語は通常、自動化ツールによって実行される分析に適用され、人間による分析は一般的に「プログラム理解」、「プログラム解析」 、または「コードレビュー」と呼ばれます。最後のコードレビューでは、ソフトウェア検査やソフトウェアウォークスルーも使用されます。ほとんどの場合、分析はプログラムのソースコードのいずれかのバージョンに対して実行され、場合によってはオブジェクトコードのいずれかの形式に対して実行されます。

リソース認証における主要なアプローチは、静的解析（SA）と暗黙的計算複雑性（ICC）の2つです。SA​​はアルゴリズム的な性質を持ち、特定のプログラミング言語に焦点を当て、構文解析によってその言語で記述されたプログラムが実行可能かどうかを判定します。一方、ICCは、複雑性クラスを定義する専用のプログラミング言語や手法を最初から作成しようとします。したがって、SAはコンパイル時に焦点を当てており、プログラマーに要求を課しません。それに対し、ICCは言語設計の分野と言えます。

静的解析という分野は、コーディングスタイルの誤りをチェックするプロセスであるリンティングと混同してはならない。

ツールによって実行される分析の高度さは、個々のステートメントや宣言の動作のみを考慮するもの^{[ 4 ]}から、プログラムのソースコード全体を分析対象に含めるものまで様々です。分析から得られた情報の用途は、コーディングエラーの可能性を強調表示すること（例：lintツール）から、特定のプログラムに関する特性を数学的に証明する形式手法（例：その動作が仕様と一致すること）まで多岐にわたります。

ソフトウェアメトリクスとリバースエンジニアリングは、静的解析の一形態として説明できます。ソフトウェアメトリクスと静的解析の導出は、特に組み込みシステムの作成において、いわゆるソフトウェア品質目標を定義することによって、ますます一緒に使用されるようになっています。^{[ 5 ]}

静的解析の商業的な用途として、安全性が極めて重要なコンピュータシステムで使用されるソフトウェアの特性の検証や、潜在的に脆弱なコードの特定がますます増えています。^{[ 6 ]}例えば、以下の業界では、ますます高度化・複雑化するソフトウェアの品質向上手段として、静的コード解析の利用が認識されています。

1. 医療ソフトウェア：米国食品医薬品局（FDA）は、医療機器における静的解析の使用を認めています。^{[ 7 ]}
2. 原子力ソフトウェア：英国では、原子力規制局（ONR）が原子炉保護システムの静的解析の使用を推奨している。^{[ 8 ]}
3. 航空ソフトウェア（動的解析との組み合わせ）。^{[ 9 ]}
4. 自動車および機械（機能安全機能は、自動車製品開発の各段階において不可欠な部分を構成する、ISO 26262、セクション8）。

VDC Research が 2012 年に実施した調査では、調査対象となった組み込みソフトウェアエンジニアの 28.7% が静的解析ツールを使用しており、39.7% が 2 年以内に使用する予定であると報告されています。^{[ 10 ]} 2010 年の調査では、ヨーロッパの研究プロジェクトでインタビューを受けた開発者の 60% が、基本的な IDE に組み込まれている静的アナライザーを少なくとも使用していることがわかりました。しかし、追加の (おそらくより高度な) 解析ツールを使用しているのは約 10% に過ぎません。^{[ 11 ]}

アプリケーションセキュリティ業界では、静的アプリケーションセキュリティテスト（SAST）という名称も使用されています。SASTは、Microsoftが定義したSDL ^{[ 12 ]}などのセキュリティ開発ライフサイクル（SDL）の重要な部分であり、ソフトウェア企業では一般的な手法です^{[ 13 ] 。}

OMG（オブジェクト管理グループ）は、ソフトウェア品質の測定と評価に必要なソフトウェア分析の種類に関する研究を発表しました。この「CISQ推奨事項に沿った、回復力があり、安全で、効率的で、変更しやすいITシステムを提供する方法」という文書では、3つのレベルのソフトウェア分析について説明しています。^{[ 14 ]}

ユニットレベル

特定のプログラムまたはサブルーチン内で行われる分析であり、そのプログラムのコンテキストとは関連付けられていない。

技術レベル

ユニットプログラム間の相互作用を考慮に入れた分析により、プログラム全体のより包括的かつ意味論的な視点を得て、問題点を発見し、明らかな誤検出を回避する。

システムレベル

ユニットプログラム間の相互作用を考慮した分析であり、特定の技術やプログラミング言語に限定されない。

ソフトウェア分析のさらなるレベルを定義することができる。

ミッション/ビジネスレベル

企業活動またはプログラム／ミッション活動の一環としてソフトウェアシステムが運用される際に、システム内部に実装されるビジネス／ミッション層の用語、ルール、プロセスを考慮した分析。これらの要素は、特定の技術やプログラミング言語に限定されずに実装され、多くの場合、複数の言語にまたがって実装されますが、ミッションの確実性を確保するためのシステム理解を目的として、静的に抽出・分析されます。

多くの静的解析ツールは、プログラムを実行せずにソースコードの構造を調べるために、プログラムの中間表現を使用します。この目的のために、プログラムの構文要素を構造的に表現できる抽象構文木（AST）が一般的に使用されます。

形式手法とは、厳密な数学的手法のみを用いて結果を得るソフトウェア（およびコンピュータハードウェア）の分析に用いられる用語である。用いられる数学的手法には、表示的意味論、公理的意味論、操作的意味論、および抽象解釈が含まれる。

停止問題への単純な還元により、任意のチューリング完全言語について、任意のプログラムにおけるあらゆる実行時エラー（あるいはより一般的には、プログラムの最終結果に関する仕様の違反）を見つけることは決定不能であることが証明できる。つまり、任意のプログラムが実行時エラーを起こすかどうかについて常に真実を答えることができる機械的な方法は存在しない。この結果は、 1930年代のチャーチ、ゲーデル、チューリングの研究に由来する（停止問題とライスの定理を参照）。多くの決定不能な問題と同様に、有用な近似解を与える試みは依然として可能である。

形式静的解析の実装手法には以下のようなものがある。^{[ 15 ]}

• 抽象解釈は、各ステートメントが抽象マシンの状態に及ぼす影響をモデル化します（つまり、各ステートメントと宣言の数学的特性に基づいてソフトウェアを「実行」します）。この抽象マシンはシステムの振る舞いを過度に近似します。そのため、抽象システムは分析が簡単になりますが、不完全性（元のシステムのすべての特性が抽象システムにも当てはまるわけではない）という代償を伴います。しかし、適切に行えば、抽象解釈は健全です（抽象システムのすべての特性は、元のシステムの真の特性にマッピングできます）。^{[ 16 ]}
• データフロー解析とは、可能な値の集合に関する情報を収集するための格子ベースの手法である。
• ホア論理は、コンピュータプログラムの正しさについて厳密に推論するための論理規則のセットを備えた形式体系です。一部のプログラミング言語（例えば、SPARKプログラミング言語（ Adaのサブセット）や、 ESC/JavaおよびESC/Java2を使用するJavaモデリング言語（JML）、ACSL（ ANSI/ISO C仕様言語）で拡張されたC言語用のFrama-C WP（最弱事前条件）プラグインなど）にはツールサポートがあります。
• モデル検査は、有限状態を持つシステム、または抽象化によって有限状態に縮小できるシステムを対象とする。
• 記号実行とは、コード内の特定の箇所における変更された変数の値を表す数式を導出するために使用される手法である。
• ヌル可能な参照分析

データ駆動型静的解析は、広範なコードベースを活用してコーディング規則を推論し、解析の精度を向上させます。^{[ 17 ] [ 18 ]}例えば、GitHubで入手可能なすべての Java オープンソース パッケージを使用して、優れた解析戦略を学ぶことができます。規則の推論には機械学習技術を使用できます。^{[ 19 ]}また、大量の過去の修正と警告から学習することも可能です。^{[ 17 ]}

静的アナライザーは警告を生成します。特定の種類の警告については、自動修復技術を設計および実装することが可能です。たとえば、LogozzoとBallはC# cccheckの自動修復を提案しています。^{[ 20 ]}

• Ayewah, Nathaniel; Hovemeyer, David; Morgenthaler, J. David; Penix, John; Pugh, William (2008). "静的解析を使用してバグを見つける". IEEE Software . 25 (5): 22–29 . CiteSeerX 10.1.1.187.8985 . doi : 10.1109/MS.2008.130 . S2CID 20646690 .  
• Brian Chess、Jacob West (Fortify Software) (2007).静的解析によるセキュアプログラミング. Addison-Wesley. ISBN 978-0-321-42477-8。
• フレミング・ニールソン、ハンネ・R・ニールソン、クリス・ハンキン（2004年12月10日）。プログラム分析の原理（1999年版（2004年改訂 版））。シュプリンガー。ISBN 978-3-540-65410-0。
• 「抽象解釈と静的解析」、 2003年国際意味論・応用冬季スクール、デビッド・A・シュミット著