プログラム解析入門
もしくはC/C++を安全に書くのが難しすぎる話
Last updated: Jul 30, 2022
Kinuko Yasuda <@kinu>
前置き
気になりますね 👀
この資料で説明すること・しないこと
その難しさと戦うために日々改良が行われているプログラム解析� (動的解析、静的解析) とプログラミング言語の安全性について、�基礎的な工学・数学的背景も含めてざっくり説明します。
（明日からすぐに自分のプログラムに適用して安全にしたり…�はできるようになりません😊、他の資料をあたってください）
なお、内容は個人の意見・理解に基づくものです
問題点の共有：C / C++ などの難しさ
C++ (や類似の古めの言語) では安全なコードを書くのがとにかく難しい！
ptr
???
適当なアドレスを�セットすれば
その中を見られる
でも中を見ちゃダメなところだったら�クラッシュする 😨
例えば… (1)
void func(char* p) {
*p = 'c';
}
p に nullptr や適当な値 (0xff) が来たらクラッシュ�null-deref, invalid access
opt に値がセットされていなかったら例外�bad_optional_access
例えば… (2)
int func(std::vector<int>& vec) {
auto& v0 = vec[0];
vec.emplace_back(1);
return v0;
}
void func(const std::vector<int>& vec) {
return vi[idx];
}
idx に vec.len() や -1 が来たら不正アクセス (すぐクラッシュするとは限らない)�vector overflow / underflow
emplace_back によって元の vec[0]�はもう free されているかも知れない use-after-free
疑問
どうすればより安全なコードを書ける？
安全なプログラムを書くための戦略
安全なプログラムを書くための戦略
規模が大きくなると、
間違いを「絶対に」�起こさないのはムリです…
安全なプログラムを書くための戦略
安全なプログラムを書くための戦略
テストは素晴らしい！でも限界がある：
1. プログラムに入力を与える
2. プログラムの出力と正解を比べる
安全なプログラムを書くための戦略
そこで動的解析
動的解析とは、プログラムを実行しながらプログラムの解析を行う手法の総称
ものすごくざっくり説明するならば、例えば�
このようなチェック文をコンパイラやライブラリ越しに挿入することで、プログラム実行中に起きてはいけないことが起こってないか常にチェックする方法。応用範囲が広く強力
if (起きてはいけない条件があるか？) {� 報告してクラッシュする();�} |
動的解析の例
多くの手法やライブラリが発表されており、大量のバグを見つけてきた。例：
動的解析の例：Address Sanitizer (ASan)
メモリアクセスをトラックする Shadow memory と呼ばれる特別な領域を使って、許されていないメモリへのアクセスがないか実行時に(= 動的に)チェックする
Process Memory
Shadow Memory
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
if (IsPoisoned(p))
Crash();
*p = 0xb00;
*p = 0xb00;
コンパイル時にチェックを埋め込む
p
0xb00
p >> 3 + offset
Poisoned
アクセスしては�いけない領域
８バイトのメモリを１バイトの shadow 領域で管理
動的解析の例：Address Sanitizer (ASan)
メモリアクセスをトラックする Shadow memory と呼ばれる特別な領域を使って、許されていないメモリへのアクセスがないか実行時に(= 動的に)チェックする
Process Memory
Shadow Memory
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
*p = 0xb00;
コンパイル時にチェックを埋め込む
p
0xb00
p >> 3 + offset
Poisoned
アクセスしては�いけない領域
* チェックを入れる箇所をサンプリングしてオーバヘッドを抑え、リリースバイナリに入れる方法もあります
if (IsPoisoned(p))
Crash();
*p = 0xb00;
2〜5倍遅くなる程度で動的チェックしながらプログラムを実行できる* ��なにが嬉しい？ あらゆるテストやリリース前バイナリで ASAN を有効化することで、メモリエラーを探せる範囲が格段に増える!
* チェックを入れる箇所をサンプリングすることでオーバヘッドを抑える方法 (GWP-Asan) もあります
動的解析の例：Fuzzing (ファジング)
プログラムの入力として、自動的に生成されるランダムなデータを（変異させながら）与え続けることで、プログラムのエラーを見つける方法。
単なるランダムな入力を与えるだけではなく、プログラムのいろいろな実行パスをなるべく効率よくテストできるように入力を変異させるアルゴリズムがいろいろ研究されている
テスト対象の
プログラム
新しい入力
フィードバック情報
動的解析の例：Fuzzing (ファジング)
プログラムの入力として、自動的に生成されるランダムなデータを（変異させながら）与え続けることで、プログラムのエラーを見つける方法。
単なるランダムな入力を与えるだけではなく、プログラムのいろいろな実行パスをなるべく効率よくテストできるように入力を変異させるアルゴリズムがいろいろ研究されている
テスト対象の
プログラム
新しい入力
フィードバック情報
安全なプログラムを書くための戦略
動的解析と静的解析
動的解析 → プログラムを実行しながらエラーを見つける���
静的解析 → プログラムを実行せずに(実行する前に)エラーを見つける
if (check_error(...)) {� report_error_and_crash();�} |
(補足) Shifting left: 早く問題を見つけるとコストも低い
動的解析
静的解析
なるべく早く（左側で）見つけたい
(ただし、右側のほうが一般的にはより多くの問題を正確に見つけられる)
プログラムを実行せずに解析するとは？
プログラムのソースコードや仕様を元に、パターンマッチや数学的な手法でプログラムの挙動や性質を検証する方法のこと。
プログラムの仕様を別の言語で書いてモデル検証する方法や、バイナリを解析して検証する方法もありますが、ここではソースコードをそのまま解析する手法を説明します
CPU上でプログラムの命令を実行する代わりに…
プログラムを解析して、
形をチェックしたり�モデル化した問題を解く
静的解析は古くて新しい問題
静的解析の考え方自体は 1950 年代頃からある古くて新しい問題
コンパイラの進歩などとともに（地味に）発達してきたが、
2005年頃からプログラム解析での応用が急速に発展した。
理由はいくつかあるが…
奥深い分野ですが、こちらもものすごくざっくり説明します
解析の材料: Abstract Syntax Tree (AST, 抽象構文木)
AST とはプログラムを構文解析して、意味に関係ある部分を木構造で表したもの
コンパイラがプログラムの意味解析や最適化をするために作るものとして知られる�AST ベースのプログラム解析は IDE をはじめ多くのツールで使われています
x = a + b;
while (y > a) {
a = a + 1;
}
Program
=
while
>
Block
=
a
+
a
1
x
+
a
b
y
a
古典的な静的解析：Lint, よくあるエラーの指摘
プログラムの AST をパターンマッチして、危険なパターンを指摘・修正してくれる
void function() {
int x;
…� foo(&x);
}
void function() {
int x = 0;
…� foo(&x);
}
変数 x が初期化されていない
1) 初期値が与えられていないコードパターンを探す AST クエリを書く
2) クエリにマッチしたコードパターンを元に、警告を報告する
before
after
varDecl(� unless(hasInitializer(anything())),� unless(isInstantiated()),� isDefinition())
ASTクエリの例
古典的な静的解析：Lint, よくあるエラーの指摘
プログラムの AST をパターンマッチして、危険なパターンを指摘・修正してくれる
void function() {
int x;
…� foo(&x);
}
void function() {
int x = 0;
…� foo(&x);
}
変数 x が初期化されていない
before
after
1) 初期値が与えられていないコードパターンを探す AST クエリを書く
2) クエリにマッチしたコードパターンを元に、警告を報告する
varDecl(� unless(hasInitializer(anything())),� unless(isInstantiated()),� isDefinition())
ASTクエリの例
同じようにして、パターンをうまく書けばいろんなチェックを作れます！
でもこれだけだとパターンマッチ�による解析しか作れませんね…
一方、解析で見つけたいバグとは…
C++ や Java で断然危険なのはメモリエラー
これらがあると：
int x[4];
アクセスし�てはいけない
void func(std::optional<int> opt) {
if (opt.has_value()) {
...
}
use(*opt); // これは危険😣
}
一方、解析で見つけたいバグとは…
C++ や Java で断然危険なのはメモリエラー
これらがあると：
int x[4];
アクセスし�てはいけない
void func(std::optional<int> opt) {
if (opt.has_value()) {
...
}
use(*opt); // これは危険😣
}
危ないメモリアクセスをする�可能性のあるプログラムを�警告したい
一方、解析で見つけたいバグとは…
C++ や Java で断然危険なのはメモリエラー
これらがあると：
int x[4];
アクセスし�てはいけない
void func(std::optional<int> opt) {
if (opt.has_value()) {
...
}
use(*opt); // これは危険😣
}
危ないメモリアクセスをする�可能性のあるプログラムを�警告したい
どうやって？？��各値の状態がフロー制御によってどう変わるか追っていかないとチェックできない
パターンマッチングでは限界がある
解析に使える便利な道具：CFG(制御フローグラフ)
AST をもとに CFG (制御フローグラフ) というグラフを構築することで、プログラムの流れに沿った解析や最適化が可能になる
void func(std::optional<int> opt) {
if (opt.has_value()) {
use1(*opt);
}
…� use2(*opt);
}
if (opt.has_value())
use1(*opt)
use2(*opt)
T
F
CFG の例
CFG: 分岐やループなどのフローの流れをつないでグラフにしたもの。ノードはプログラムの基本ブロック。
データフロー解析 : 単純な例
void Example(int n) {
int x = 0;
// x の取り得る値は {0}
if (n > 0) {
x = 5;
// x の取り得る値は {5}
} else {
x = 42;
// x の取り得る値は {42}
}
// x の取り得る値は {5, 42}
print(x);
}
“x” が各場所でどの値を取り得るかを解析する
→ x の取り得る値をセットで表すことにする�
このように CFG の沿ってモデルの値を更新することを繰り返し、すべての場所で値が変わらなくなったら (=fixpoint に到達したら) 解析終了とする
データフロー解析 : 単純な例
void Example(int n) {
int x = 0;
// x の取り得る値は {0}
if (n > 0) {
x = 5;
// x の取り得る値は {5}
} else {
x = 42;
// x の取り得る値は {42}
}
// x の取り得る値は {5, 42}
print(x);
}
“x” が各場所でどの値を取り得るかを解析する
→ x の取り得る値をセットで表すことにする�
値の更新をよく見ると…
このように CFG の沿ってモデルの値を更新することを繰り返し、すべての場所で値が変わらなくなったら (=fixpoint に到達したら) 解析終了とする
データフロー解析 : 単純な例
void Example(int n) {
int x = 0;
// x の取り得る値は {0}
if (n > 0) {
x = 5;
// x の取り得る値は {5}
} else {
x = 42;
// x の取り得る値は {42}
}
// x の取り得る値は {5, 42}
print(x);
}
“x” が各場所でどの値を取り得るかを解析する
→ x の取り得る値をセットで表すことにする�
値の更新をよく見ると…
このように CFG の沿ってモデルの値を更新することを繰り返し、すべての場所で値が変わらなくなったら (=fixpoint に到達したら) 解析終了とする
順序集合的にはこれは Lattice (束) � として見ることができる！
データフロー解析と束
このケースでは join(a, b) = a ∪ b であり
join(a, b) ⩾ a, join(a, b) ⩾ b
void Example(int n) {
int x = 0;
// x の取り得る値は {0}
if (n > 0) {
x = 5;
// x の取り得る値は {5}
} else {
x = 42;
// x の取り得る値は {42}
}
// x の取り得る値は {5, 42}
print(x);
}
何も情報がない状態 (初期化前) が ⊥ (bottom)
データフロー解析と束
void ExampleOfTopWithALoop() {
int x = 0; // x is {0}
while (condition()) {
x += 1; // x is {0, 1, 2...}
}
print(x); // x is {0, 1, 2...}
}
解析が終了しなそうな例
例えばこのようなループがあったら束の高さは無限になり、解析は終了しない😣
上界がない (Join-semilattice)
何も情報がない状態 (初期化前) が ⊥ (bottom)
データフロー解析と束
void ExampleOfTopWithALoop() {
int x = 0; // x is {0}
while (condition()) {
x += 1; // x is ⊤
}
print(x); // x is ⊤
}
情報が多すぎる、衝突がある場合を ⊤ (top) とする
→ 有限時間で fixpoint に到達する (= 解析終了)
現実的な落とし所：モデルの精度を落として上限を定め、そこを ⊤ (top) とする
例えば値の集合は 3 つまでしか追わないなど
解析が終了するには昇鎖条件が成り立つ必要がある = 上限が必要
何も情報がない状態 (初期化前) が ⊥ (bottom)
データフロー解析と束
void ExampleOfTopWithALoop() {
int x = 0; // x is {0}
while (condition()) {
x += 1; // x is ⊤
}
print(x); // x is ⊤
}
情報が多すぎる、衝突がある場合を ⊤ (top) とする
→ 有限時間で fixpoint に到達する (= 解析終了)
現実的な落とし所：モデルの精度を落として上限を定め、そこを ⊤ (top) とする
例えば値の集合は 3 つまでしか追わないなど
解析が終了するには昇鎖条件が成り立つ必要がある = 上限が必要
何も情報がない状態 (初期化前) が ⊥ (bottom)
Complete Lattice (完備束)として解析を� 作ることで、fixpoint (不動点) に到達 ＝� 最小解が求まると同意になる
データフロー解析：定式化
束の値 はプログラムの文 (statement) と制御フローによって変更される
// 入力: x is {42, 44} x = x + 100; // 出力: x is {142, 144} |
if (...) { ... // 入力: x is {42} } else { ... // 入力: x is {44} } // 出力: x is {42; 44} |
データフロー解析：定式化
束の値 はプログラムの文 (statement) と制御フローによって変更される
// 入力: x is {42, 44} x = x + 100; // 出力: x is {142, 144} |
if (...) { ... // 入力: x is {42} } else { ... // 入力: x is {44} } // 出力: x is {42; 44} |
この条件を満たす
transfer, join と束の定義を
設計することで、様々な解析を�作ることができます
余談：データフロー解析の典型的な応用例
コンパイラの (少し古典的な) 最適化の話で良く出てきます
とはいっても…
実際のプログラムでは、この例のように変数に 0 や 42 のような具体的な値 (concrete value) を代入することは少ない
�
具体的な値を取らない値を「プログラムを実行することなく」�どのように解析するのか？
x = 42; // {42} |
x = x + y; |
シンボリック実行
具体的な値がないときは「シンボリックな値」を使ってプログラムを実行する
実際のハードウェアでの実行と同様に、�シンボリック値を記録する仮想的な「ストレージ」の上で、モデルに従って束と値を更新しながら実行を進める
void func(int x, int y) { int z = x + y; if (z > 0) { x = -x; } if (y > 0) { if (x == y) x = 5; y = 3; } } |
未知の値はシンボル値 x0, y0 として扱う
x のシンボリックな状態は x = -x0
パス条件 (Path Condition)
実行は分岐していくので、どの条件のときの値かの情報 (= パス条件) が必要
パス条件 == そこまでの分岐状態をすべてエンコードしたシンボリックな論理値
void func(int x, int y) { int z = x + y; if (z > 0) { x = -x; } if (y > 0) { if (x == y) x = 5; y = 3; } } |
未知の値はシンボル値 x0, y0 として扱う
パス条件: x0 + y0 > 0�のとき、x のシンボリックな状態は x = -x0
x0 + y0 > 0
x = -x0;
T
F
パス条件 (Path Condition): すべて辿ると
すべての可能な分岐を見ると、実行は二分木状になる
void func(int x, int y) { int z = x + y; if (z > 0) { x = -x; } if (y > 0) { if (x == y) x = 5; y = 3; } } |
z > 0
y > 0
y > 0
x == y
x == y
x = -x;
x = 5;
y = 3;
T
T
T
F
F
F
T
F
パス条件 | (x0 + y0 > 0) ∧ (y0 > 0) ∧�¬(-x0 == y0) |
値 | x= -x0, y = 3 |
実際には通らないパスもある
どんな入力を与えても通らない分岐の組み合わせは解析から外してよい
z > 0
y > 0
y > 0
x == y
x == y
x = -x;
x = 5;
y = 3;
T
T
T
F
F
F
T
F
パス条件 | (x0 + y0 > 0) ∧ (y0 > 0) ∧�(-x0 == y0) |
値 | x= 5, y = 3 |
void func(int x, int y) { int z = x + y; if (z > 0) { x = -x; } if (y > 0) { if (x == y) x = 5; y = 3; } } |
これを満たす解は存在しない! Unsatisfiable
あり得ないパスはどう判定する?
あるパスがあり得るかは、SAT (充足可能性判定) 問題として解ける
SAT問題は古典的な NP 完全問題だが、近年ソルバが著しく発展したこともあって幅広く応用されるようになった (== 大規模解析もかなり現実的になった)
寄り道: SAT / SMT ソルバの進化
扱える変数規模の変遷
1962年 DPLL 10変数� 1986年 BDDs 100変数� 1996年 GRASP 1K変数� 2001年 CDCL 10K変数� 2013年 1M変数� 2020年 100M変数〜
2020年のSATベンチマークで優勝したもの
速いSATとして応用を一気に広めた MiniSAT 2006 の性能
過去20年で著しく高速化
寄り道: Knuth先生の本を読んで自分で書いてみよう！
TeX、チューリング賞などで知られるクヌース先生のSAT本
単純なもの（= 遅い）であれば比較的簡単に書けます
寄り道: SMT ソルバで身近な問題を解く
ソルバを自作して遊ぶわけではないなら、公開されている SMT ソルバ（cvc5 [1] やマイクロソフトのz3 [2]やなど）を使って問題を解いて見るのも楽しいですね�[1] https://cvc5.github.io/ �[2] https://github.com/Z3Prover/z3
機械学習の影に隠れていますが、実はソルバで解けてしまう�問題もかなりたくさんあります（問題設定さえうまくすれば）
そして… すべてを組み合わせる！
LLVM/Clang でいろいろなデータフロー解析を開発できるフレームワークを作ってます
そして… すべてを組み合わせる！
LLVM/Clang でいろいろなデータフロー解析を開発できるフレームワークを作ってます
「バグがあるコード」とは�意味合いが少し異なります
いろいろな静的解析の設計例
注：ある問題をモデル化する方法はいろいろ�あり得ます、ここであげてるのは全て一例です
解析の例：未初期化変数
void Init() { int x; // x is uninitialized if (cond()) { x = 10; // x is initialized } else { x = 20; // x is initialized } print(x); // x is initialized } |
void Uninit() { int x; // x is uninitialized if (cond()) { x = 10; // x is initialized } print(x); // x is maybe uninitialized } |
安全
ダメ
Initialized
Uninitialized
Maybe Uninitialized
例えば、各変数について、初期化状態を示す {Initialized, Uninitialized} を記録する�
join:
transfer:
decl: 新しく Uninitialized を作る� assign: Uninitialized → Initialized
解析の例：危険な std::optional の使い方を警告する
void Safe(std::optional<int> &x) { if (x.has_value()) { Use(x.value()); } } |
void Unsafe1(std::optional<int> &x) { if (x.has_value()) { ... } Use(x.value()); } |
安全
危険
例えば、シンボリックな論理値 has_value を子に持つ複合値として optional を定義
束の値: violation のあるソース箇所
join(a, b): a ∪ b�
transfer:
ctor(e), assign(x, e): eが値を持っていれば� x.has_value をパス条件に足す
unwrap(x): x.has_value がパス条件によっ� て Imply されているかを調べる� (パス条件 ∧ ¬has_value を満たす解が� 存在しない == Unsat であるかを調べる)
危険
void Unsafe2(std::optional<int> &x, � std::optional<int> &y) { bool b = x.has_value();� if (b || y.has_value()) { Use(x.value()); } } |
危険
解析の例：Null ポインタか参照される可能性を警告する
void foo(int *x, bool b) { if (b) { x = nullptr; } if (!b) { *x; // 安全 { NonNull } } *x; // 危険 { Null? } } |
安全
危険
例えば、ポインタの状態は Null, NonNull, Unknown (状態がわからない) の3値論理値で決まるとする*
パス条件やシンボリック状態がより複雑になるため、どういう論理値モデルにするか、どれくらいの状態を保持するかなどが論点になる
* “Gradual Program Analysis for Null Pointers”, ECOOP 2021, Sam Estep et al より
そうはいっても…
本当にそれでちゃんと問題は見つかるの？�
→ 静的解析にももちろん限界があります
よく問題になるのが誤検知 (False Postivie)
静的解析の Soundness と Precision の話
静的解析を設計する上で必ず出てくる概念：
ほとんどの解析は Precise でも Sound でもないが、多くの解析はなるべく Sound な（＝見落としはない）解析を目指して、その中で誤検知をできるだけ低くする
問題
問題
問題
Sound, Imprecise
(見落としがない)
Precise, Unsound�(誤検知がない)
Unsound�Imprecise
実際の問題の形
解析のモデル化が�検知できる形
どう運用すると使われるのか？複数文献に見られるメタ知見
「すぐに報告されなかったものは人間は重要だと思わない」
「やり終わったものへの報告は対処されにくい」(コンテキストスイッチが大変)
「同じ問題でもコンパイルエラーとして出るとびびって直す人が多い…」
ちなみに: 静的解析と動的解析の組み合わせ
質問：静的解析と動的解析の両要素を組みわせた方法はないの？
もちろんあります。例えば：似た要素技術（シンボリック実行とSMTソルバ）と動的テスト実行を組み合わせたテスト手法として、Concolic Testing などが有名
Symbolic Execution + Testing with Concrete Values = Concolic Testing
1. 適当な入力値を選んでテストを実行� 2. 実行パス中に通る条件の１つを反転 (Negate)し、それを満たす入力をSMTソルバを使って得る� 3. それを次の入力としてテストを実行 (繰り返し)
�静的解析だけでは分からないフロー構造や実行環境を動的実行の結果から取り入れる…みたいな解析方法は他にもたくさんやられています
シンボリック実行
具体値を使ったテスト
コンコリックテスト
安全なプログラムを書くための戦略
安全なメモリの世界：GC と Borrow Checker
GC (Garbage Collection)
Borrow Checker
安全なメモリの世界：GC と Borrow Checker
GC (Garbage Collection)
Borrow Checker
Garbage Collection は� 動的解析ベースの
アプローチ
Borrow Checker は
静的解析ベースの� アプローチ
C++ はライフタイムの夢を見るか
C++ に Rust のライフタイムという概念を持ち込む提案があります (してます)
ライフタイムとは
[RFC] Lifetime annotations for C++�https://discourse.llvm.org/t/rfc-lifetime-annotations-for-c/61377
ptr
😈？
ptr
invalid
✗
安全なプログラムを書くための戦略
自動化アプローチ例
自動コード提案：CodeX / Github Copilot (OpenAI / MS), AlphaCode (Google)
プログラムを自動で修正する：DeepDelta (Google)
ML と動的解析・静的解析を組み合わせるアイディアも多く研究されています
おしまい