プログラム分析

制御フロー解析の目的は、プログラム実行中の様々な時点でどの関数が呼び出されるかに関する情報を取得することです。収集された情報は制御フローグラフ（CFG）で表され、ノードはプログラムの命令、エッジは制御の流れを表します。CFGはコードブロックとループを特定することで、コンパイラによる最適化の出発点となります。

データフロー解析は、プログラムの各ポイントにおける値とその時間経過に伴う変化に関する情報を収集するために設計された手法です。この手法は、コンパイラがコードを最適化する際によく使用されます。データフロー解析の最もよく知られた例の1つは、汚染チェックです。これは、ユーザーが提供したデータを含むすべての変数（「汚染されている」、つまり安全でないとみなされる）を考慮し、それらの変数がサニタイズされるまで使用できないようにするものです。この手法は、 SQLインジェクション攻撃を防ぐためによく使用されます。汚染チェックは、静的または動的に実行できます。  

抽象解釈を用いることで、プログラムを実際に実行することなく、プログラムの実行結果に関する情報を抽出することが可能になります。この情報は、コンパイラが最適化の可能性を探したり、特定の種類のバグに対するプログラムの安全性を検証したりするために利用できます。

型システムは、特定の要件を満たすプログラムに型を関連付けます。その目的は、ある特性に基づいて正しいとみなされる言語のプログラム群を選択することです。

• 型チェック– プログラムが型システムによって受け入れられるかどうかを検証します。

型チェックは、プログラミングオブジェクトの使用方法や実行可能な動作を制限するためにプログラミングで使用されます。これはコンパイラまたはインタプリタによって行われます。型チェックは、符号付き値が符号なし変数に割り当てられないようにすることで、脆弱性の防止にも役立ちます。型チェックは、静的（コンパイル時）、動的（実行時）、またはその両方の組み合わせで行うことができます。

静的な型情報（推論されたもの、またはソースコード内の型注釈によって明示的に提供されたもの）は、ボックス化された配列をボックス化されていない配列に置き換えるなどの最適化を行うためにも使用できます。

効果システムとは、関数やメソッドの実行によって生じる効果を表現するために設計された形式システムです。効果は、何が実行され、何を用いて実行されるかをコード化します。これらは通常、それぞれ効果の種類と効果領域と呼ばれます。 

モデル検査とは、モデル（この文脈ではコードの形式モデルを指しますが、他の文脈ではハードウェアのモデルを指す場合もあります）が与えられた仕様に準拠しているかどうかを、厳密かつ形式的で自動化された方法でチェックする手法です。コードは本質的に有限状態であり、仕様とコードの両方が論理式に変換可能であるため、効率的なアルゴリズム的手法を用いてシステムが仕様に違反していないかどうかをチェックすることが可能です。

ソフトウェアは、その品質と、期待どおりに確実に動作すること、そして他のソフトウェアと競合しないことを保証するためにテストされるべきです。テストは、入力を与えてプログラムを実行し、その動作と出力を評価することによって行われます。セキュリティ要件が指定されていない場合でも、攻撃者がソフトウェアを改ざんして情報を盗み出したり、ソフトウェアの正常な動作を妨害したり、ソフトウェアを足がかりとしてユーザーを攻撃したりできないように、追加のセキュリティテストを実施する必要があります。

プログラム監視は、リソース使用量、イベント、相互作用など、プログラムに関するさまざまな情報を記録・ログ化し、異常動作の原因を特定するためにレビューできるようにします。さらに、セキュリティ監査にも利用できます。プログラムの自動監視は、ランタイム検証と呼ばれることもあります。

プログラムの動作の特定部分集合に対して、プログラムスライシングとは、選択した動作を依然として生成する最小限の形式にプログラムを縮小することです。縮小されたプログラムは「スライス」と呼ばれ、指定された動作部分集合の範囲内で元のプログラムを忠実に表現したものです。一般的に、スライスを見つけることは解決不可能な問題ですが、一連の変数の値によって対象となる動作部分集合を指定することで、データフローアルゴリズムを使用して近似スライスを取得することが可能です。これらのスライスは通常、開発者がデバッグ中にエラーの原因を特定するために使用します。