計算機科学において、プログラム解析(ぷろぐらむかいせき、)Nielson, F., Nielson, H. R., & Hankin, C. (2015). Principles of program analysis. Springer.とは、正当性、堅牢性、安全性、活性などの性質に関して、コンピュータプログラムの振る舞いを解析するプロセスである。 プログラム解析は、プログラム最適化とプログラム正当性という2つの主要な領域に焦点を当てている。前者はリソース使用量を削減しながらプログラムの性能を向上させることに焦点を当て、後者はプログラムが本来すべきことを行っていることを保証することに焦点を当てている。

プログラム解析は、プログラムを実行せずに(静的コード解析)、実行時に(動的プログラム解析)、またはその両方を組み合わせて行うことができる。

静的プログラム解析

プログラム正当性の文脈では、静的解析によってプログラムの開発フェーズ中に脆弱性を発見できるJovanovic, N., Kruegel, C., & Kirda, E. (2006, May). Pixy: A static analysis tool for detecting web application vulnerabilities. In Security and Privacy, 2006 IEEE Symposium on (pp. 6-pp). IEEE.。これらの脆弱性は、静的解析によって脆弱性の根本原因が特定されるため、テストフェーズで発見されるものよりも修正が容易である。

静的解析の多くの形式は計算上決定不能であるため、それを実行するメカニズムが常に正しい答えを返して終了するとは限らない。これにより、偽陰性(コードに実際に問題があるにもかかわらず「問題は見つかりません」)や偽陽性が生じる可能性があり、あるいは誤った答えを返すことはないが終了しない可能性もある。これらの制限にもかかわらず、静的解析は依然として価値がある。第1のタイプのメカニズムは脆弱性の数を減らす可能性があり、第2のタイプは特定のクラスの脆弱性の不在について強い保証を提供できる場合がある。

誤った最適化は非常に望ましくない。そのため、プログラム最適化の文脈では、計算上決定不能な解析を処理するための2つの主な戦略がある。

最適化コンパイラのオプティマイザなど、比較的短時間で完了することが期待されるオプティマイザは、有限時間内に完了することが保証され、かつ正しい最適化のみを見つけることが保証された、解析の省略版を使用することができる。 サードパーティの最適化ツールは、誤った最適化を生成しないが、場合によっては(最適化が見つかるまで、つまり永遠に見つからない可能性もある)無期限に実行し続けるように実装することができる。この場合、ツールを使用する開発者はツールを停止し、そのコードに対してツールを再実行することを避けなければならない(またはツールをつまずかせないようにコードを変更する必要がある)。

しかし、C言語のように完全には仕様が定められていない言語に対しては、適用可能な第3の戦略も存在する。最適化コンパイラは、使用している言語標準によってセマンティクスが規定されていないソースコードに遭遇した場合、実行時に何でもするコード、さらにはクラッシュを引き起こすコードを生成する自由がある。

制御フロー解析

制御フロー解析の目的は、プログラムの実行中のさまざまな時点でどの関数が呼び出されうるかについての情報を得ることである。収集された情報は、ノードがプログラムの命令であり、エッジが制御の流れを表す制御フローグラフ(CFG)によって表される。コードブロックとループを識別することで、CFGはコンパイラによる最適化の出発点となる。

データフロー解析

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

抽象解釈

抽象解釈は、プログラムを実際に実行することなく、プログラムの可能な実行に関する情報を抽出することを可能にする。 この情報は、コンパイラが最適化の可能性を探したり、特定のクラスのバグに対してプログラムを認定したりするために使用できる。

型システム

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

型検査 — 型システムによってプログラムが受け入れられるかどうかを検証する。

型検査は、プログラミングオブジェクトの使用方法と実行できることを制限するためにプログラミングで使用される。これはコンパイラまたはインタプリタによって行われる。型検査はまた、符号付き値が符号なし変数に代入されないことを保証することで脆弱性を防ぐのにも役立つ。 型検査は静的(コンパイル時)、動的(実行時)、またはその両方の組み合わせで行うことができる。

静的型情報(型推論によって推論されるか、ソースコードの型アノテーションによって明示的に提供される)は、ボックス化された配列を非ボックス化配列に置き換えるなど、最適化を行うためにも使用できる。

エフェクトシステム

エフェクトシステムは、関数またはメソッドを実行することで生じうるエフェクト(副作用)を表現するために設計された形式システムである。エフェクトは、何が行われているのかと何によって行われているのかを成文化する通常それぞれ「エフェクト種別」と「エフェクト領域」と呼ばれる。

モデル検査

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

動的プログラム解析

動的解析は、プログラムの実行時の知識を使用して解析の精度を高めることができ、実行時保護も提供するが、問題の単一実行のみを解析でき、実行時チェックによってプログラムの性能が低下する可能性がある。

テスト

ソフトウェアは、品質を確保し、信頼性のある方法で本来すべき動作を行い、並行して動作する可能性のある他のソフトウェアと競合しないようにテストする必要がある。テストは、入力を使用してプログラムを実行し、その動作と生成された出力を評価することで行われる。 セキュリティ要件が指定されていない場合でも、攻撃者がソフトウェアに干渉して情報を盗んだり、ソフトウェアの通常の動作を妨害したり、ユーザへの攻撃の踏み台として使用したりできないことを保証するために、追加のを実施する必要がある。

モニタリング プログラムモニタリングは、プログラムに関するリソース使用量、イベント、インタラクションなどさまざまな種類の情報を記録・ログに残し、異常な動作の原因を見つけたり特定したりするためにレビューできるようにする。さらに、セキュリティ監査を実施するために使用することもできる。プログラムの自動モニタリングは、実行時検証と呼ばれることがある。

プログラムスライシング

プログラムの振る舞いの特定のサブセットに対して、プログラムスライシングは、選択された振る舞いを依然として生成する最小の形式にプログラムを削減することからなる。削減されたプログラムは「スライス」と呼ばれ、指定された振る舞いサブセットのドメイン内における元のプログラムの忠実な表現である。 一般的に、スライスを見つけることは解くことのできない問題であるが、変数の集合の値によって目標とする振る舞いサブセットを指定することにより、データフローアルゴリズムを使用して近似スライスを得ることが可能である。これらのスライスは通常、デバッグ中にエラーの原因を特定するために開発者によって使用される。

関連項目

プロファイリング (コンピュータプログラミング) プログラム検証

脚注

参考文献

外部リンク