Georgia Tech Summer 2024 振り返り

Georgia Tech OMSCSでの三学期目を完了したので、自身の備忘も兼ねて振り返りを記しておく。

概要

5月中旬頃から、7月末頃までの期間で実施された夏学期では Software Analysisというコースを履修した（夏学期は期間が短いため、特別な手続きをした場合を除き、1コースのみ履修可能）。タイトルの通り、ソフトウェアの品質を向上させるための、様々な解析手法やツールについて学んだ。

コースの構成としては、まずレクチャーで基本的な考え方を理解した後、その内容に関連する小テスト・定期テスト・プロジェクトを通じて、より理解を深めていくような構成であった。定期テストは一度のみで、プロジェクトでカバーされていない範囲から出題される。また、グループワークは存在しなかった。

履修の狙い

主な狙いとしては、純粋にソフトウェア品質を向上させるための手法を学びたいという好奇心である。所属している会社のCIに組み込まれている様々な静的解析から日々恩恵を受けているが、内部の仕組みを理解することで、更なる品質向上へのヒントを得たいと感じていた。

また、別の狙いとして、今後履修予定の低レイヤのコースではC++を求められることが多く、C++をメインで使うコースの中でも比較的言語理解に対する要件が緩いコースで、それらに備えたいという思いもあった。

学んだ内容

このコースのプロジェクトの多くは、LLVMというコンパイラ基盤を活用して進めるため、具体的な解析手法に加えて、コンパイル時のエラーチェックの裏側の仕組みや、独自パスを追加する方法など、LLVMに対する理解を深めることができた。

また、解析手法を評価する際に重要な、SoundnessとCompletenessという考え方についても理解を深めることができた。

簡単に言うと、下記のような内容である。
Soundness: 解析がプログラムを正しいと判断した場合、そのプログラムは確実に正しいが、正しいプログラムを誤って正しくないと判断する可能性がある。例えば、あらゆるプログラムを正しくないと判断する解析はsoundである。
Completeness: 解析がプログラムを正しくないと判断した場合、そのプログラムは確実に正しくないが、正しくないプログラムを誤って正しいと判断する可能性がある。例えば、あらゆるプログラムを正しいと判断する解析はcompleteである。

コースは大きく以下9つのトピックをカバーしており、そのうち7つについては併せて関連するプロジェクトも実施し、様々な解析手法やツールに対する理解を深めることができた。

Random Testing

ランダムにテストインプットを生成し、テストを実行する手法。Androidのモバイルアプリのユーザーイベントをランダムに生成するMonkeyツールや、プログラムの並行性バグを見つけるためのCuzzというツールについても学んだ。

関連するプロジェクトでは、プログラムがクラッシュするケースを特定するインプットを自動で生成するMutation StrategyをC++で実装した。

Automated Test Generation

Random Testingと似た内容だが、過去のテストの振る舞いを観察し、将来のテスト生成に活かすことで、効率的にテストを実施する方法を学んだ。具体的なツールとして、プログラムに対するテスト生成ツールであるKoratやRandoopの仕組みについて学んだ。これらはRandom Testingで学んだ手法と比べて、不正や冗長なテストの生成を防ぐことで、より効率的にテストインプットの生成ができる。

Dataflow Analysis

制御フローグラフと呼ばれるグラフの各ノードに対してアルゴリズムを適用し、変数の値がどのように伝播するかなどの情報を集め、バグ検出やコンパイラの最適化などに活かす静的解析の手法の一つ。Reaching Definition Analysis, Very Busy Expressions Analysis, Available Expressions Analysis, Live Variables Analysisという4つの解析手法について学んだ。

関連するプロジェクトでは、Reaching Definition と Liveness Analysesのアルゴリズムの実装をC++で行った。

Pointer Analysis

こちらも静的解析の一種である、ポインタ解析について学んだ。ポインタやヒープへの参照がどの変数や記憶領域を指し示す可能性があるかを明らかにし、メモリ管理や最適化、バグ特定などに役立てることができる静的解析の手法の一つ。また、flow-sensitive・context-sensitive・ヒープの抽象化・aggregate modelingなど、ポインタ解析の様々な分類方法と、それぞれのコストや利点について理解した。

Constraints Based Analysis

「どのように計算するか」ではなく「何を計算するか」に焦点を当てて、解析を行う手法で、制約として解析の仕様を定義し、ソルバーを使用してこれらの制約を解決する。ライブラリやモジュールとして提供される既存のソルバーを利用し「どのように計算するか」の部分を自動化することで、効率的な解析が可能になる。Datalogと呼ばれる制約言語を用いた解析の手法について学んだ。

関連するプロジェクトでは、Dataflow Analysisで取り組んだReaching Definition と Liveness Analysesと同様の問題を、C++とZ3というソルバーを利用して解析を行なった。

Type Systems

型を利用してロジックのエラーを見つけることで、バグの可能性を減らすための、代表的な静的解析手法。型規則からプログラムの型を計算する方法を学んだ。また、Type systemsにおける、flow-sensitive・context-sensitive・path-sensitiveの分類についても学んだ。

関連するプロジェクトでは、バグを含むJavascriptコードをTypescriptに変換した後、Typescriptの型アノテーションを活用してバグを特定・修正した。Typescriptのような強い型付け言語のメリットをより理解することができた。

Statistical Debugging

ユーザーの実行中のプログラムの挙動に関するデータを収集し、分析することで、プログラムのクラッシュを予測する挙動を特定し、問題特定に役立てる動的解析の手法。収集した膨大なデータの中から重要なメトリクスを導出し、そのメトリクスをアルゴリズムに適用することで、バグを分離する手法を学んだ。アプリがクラッシュした際に、しばしばクラッシュレポートを求められるが、その裏側でそのレポートがどのように活用しているのかについて理解できる内容であった。

関連するプロジェクトでは、LLVMパスを追加し、Cプログラムの実行時にデータを取得し、バグを発見するのに役立つスコアを計算するプログラムをC++で実装した。

Delta Debugging

プログラムが失敗するインプットがわかっているが、その「どの部分がエラーを引き起こしているか」が不明な場合に有用なテクニック。アルゴリズムによって自動的にエラーに無関係なインプット部分を取り除き最小限のエラーを引き起こすインプットを特定する方法を学んだ。

関連するプロジェクトでは、Delta Debugging Algorithmを適用し、エラーを引き起こす最小限のインプットを特定するためのプログラムをJavaで実装した。

Dynamic Symbolic Execution

シンボリック実行と具体的実行の両方の利点を活用してプログラムのパスカバレッジを最大化し、潜在的なバグを発見するための解析手法。シンボリック実行はすべての可能な入力値を一般化して処理し、プログラムのすべてのパスを理論的に探索することで、幅広いテストカバレッジを提供する一方、具体的実行は実際の入力値に基づいてプログラムを実行し、その結果を基に解析プロセスを単純化する。このハイブリッドなアプローチによって、与えられたプログラム内の様々なパスに沿って実行を促す入力を系統的に生成することができる。

関連するプロジェクトでは、KLEEというDynamic Symbolic Executionを活用した自動テストケース生成ツールを利用して、提供されたCプログラムの特定の挙動が発生するインプットを特定した。

成績

プロジェクト: 60/60
クイズや出席点など: 19.05/20
テスト: 16.30/20
計: 95.35/100
最終成績: A

感想

今まで経験したことのない視点からソフトウェアの分析やテストについて考える機会が多く、常に好奇心を持って学ぶことができた。今後、このコースで学習した手法が使えないかという視点を持って業務に取り組み、ソフトウェアの品質の改善に繋げていきたい。

課題の指示や質問への運営からの回答が明確で、安心して快適に受講できた。総じて満足度の高いコースであった。

これまで受講してきたコースと比較して、難しいとされているコースであっても、余裕を持ってAを取得することができ自信に繋がった。おかげで、これまで難易度が高いとされているコースを履修することに不安があったが、臆せずチャレンジしていこうと思えた。