静的プログラム解析

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

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

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

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

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

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

VDC Researchが2012年に実施した調査では、調査対象となった組み込みソフトウェアエンジニアの28.7%が静的解析ツールを使用しており、39.7%が2年以内に使用したいと回答しています。^[9] 2010年の調査では、ヨーロッパの研究プロジェクトでインタビューを受けた開発者の60%が、基本的なIDEに組み込まれている静的解析ツールを少なくとも使用していました。しかし、その他の（おそらくより高度な）解析ツールを追加で使用していたのはわずか10%程度でした。^[10]

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

OMG ( Object Management Group ) は、ソフトウェア品質の測定と評価に必要なソフトウェア分析の種類に関する研究を発表しました。「CISQ の推奨事項に沿って、回復力があり、安全で、効率的で、変更が容易な IT システムを提供する方法」に関するこのドキュメントでは、ソフトウェア分析の 3 つのレベルについて説明しています。^[13]

ユニットレベル

特定のプログラムまたはサブルーチン内で、そのプログラムのコンテキストに接続せずに実行される分析。

技術レベル

ユニット プログラム間の相互作用を考慮した分析により、プログラム全体のより総合的かつ意味的なビューを取得し、問題を発見して明らかな誤検知を回避します。

システムレベル

特定のテクノロジーやプログラミング言語に限定されず、ユニット プログラム間の相互作用を考慮した分析。

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

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

エンタープライズまたはプログラム/ミッション レイヤーのアクティビティの一部としてソフトウェア システム内で運用するために実装されているビジネス/ミッション レイヤーの用語、ルール、プロセスを考慮した分析。これらの要素は、特定のテクノロジやプログラミング言語に限定されずに実装され、多くの場合、複数の言語に分散されていますが、静的に抽出され、システムを理解してミッションを保証するために分析されます。

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

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

形式的静的解析の実装技術には次のようなものがある: ^[14]

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

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

静的解析ツールは警告を生成します。特定の種類の警告に対しては、自動修復技術を設計して実装することが可能です。例えば、LogozzoとBallはC# cccheckの自動修復を提案しています。^[19]

• Ayewah, Nathaniel; Hovemeyer, David; Morgenthaler, J. David; Penix, John; Pugh, William (2008). 「静的解析を使用したバグの検出」. IEEE ソフトウェア. 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、David A. Schmidt 著