1. エグゼクティブサマリー
時空間リソース使用（STRU）の脆弱性は、ループを含み、外部から制御される実行パスの空間計算量と時間計算量に根ざしている。STAC プログラムは、STRU 脆弱性として、アルゴリズム計算量（AC）の脆弱性とサイドチャネル（SC）の脆弱性の 2 種類を扱う。AC 脆弱性は、比較的小さな入力によって引き起こされる、空間計算量または時間計算量の高い実行パスに関わる。SC 脆弱性は、秘密情報に関連する実行パスの集合に関わり、それらのパスに沿った空間計算量または時間計算量の変動からその秘密情報が推測されうる。
極端な場合、STRU 脆弱性を完全に自動で検出することは、停止問題 [1] を解くことに等しい。停止問題は解決不可能な問題であり、その起源は 1878 年の Cantor による連続体仮説 [2] にさかのぼる。連続体仮説は、のちに Gödel [3] と Cohen [4] による公理的数学の決定不能性と不完全性の証明につながった。幸いなことに、攻撃者もまた停止問題を解くことはできない。したがって、STRU 脆弱性の検出は困難ではあるが不可能ではないプログラム分析の取り組みであり、攻撃者の能力を上回ることを実際的な目標とする場合には特にそうである。我々の新しいソリューションである RULER（Resource Usage vuLnerability identifiER）は、機械と人間の革新的な統合を切り開くものであり、これにより、高度な STRU 脆弱性を正確に検出しながら、大規模なソフトウェアにスケールする。
第 6.1 節では、STAC エンゲージメントにおける我々の結果をまとめる。STAC における我々の成功は、次の研究課題を特定し、それぞれに新しい解決策を見いだしたことに直接起因する。
- 新規で高度な、ドメイン固有の STRU 脆弱性の時空間計算量を、どのように数学的にモデル化するか。
- パス爆発の問題に対処するために、プログラムの関連する振る舞いをどのように静的に計算するか。
- ソフトウェアの異常を検証し、その妥当性を確認するために、静的プログラム分析と動的プログラム分析の両方の強みをどのように効果的に活用するか。
- 新規で高度な、ドメイン固有の STRU 脆弱性を検出するために、機械と人間による分析システムは、プログラム分析における手に負えない問題にどのように対処できるか。
上記の研究課題に取り組むため、高度なリソース使用の脆弱性を検出するための我々の研究と技術的アプローチは、次の分類にわたる、プログラム分析に固有の課題に取り組むことに焦点を当てた。
- AC/SC 脆弱性のためのループのモデル化
- 実行パスに依存する解析
- 組み合わせ可能で、精度の境界を考慮した解析
- 対話とプログラム可能な what-if 推論
- 脆弱性のメカニズムをモデル化するための高水準の抽象化
第 2 節では、プロジェクトの概要を述べる。第 3 節では、我々の技術的アプローチを挙げる。第 4 節では、STAC の問題を解くために我々が RULER で達成した技術的進歩を列挙する。第 5 節では、それらの技術的進歩を STAC エンゲージメントの問題の解決にどのように適用するかを詳しく述べる。第 6 節では、エンゲージメントの結果をまとめる。続いて、第 7 節で結びの所見を、第 8 節で我々の論文と発表の一覧を示す。