静的保証（1/2）

静的解析は混乱を招くことがあります。 あるプログラムをテストしたいとします。それを P と呼びましょう。 P を一度も実行しないなら、それが何をするのか、あるいは何をできるのかを、いったいどうやって知るのでしょうか？

静的解析ツールは、特定の問いに答えることを単純化する間接化の層を使うことがよくあります。 それらは P の構成要素を、解析固有の抽象ドメインに対応付けます¹。 この表現は、P の1つ以上の性質を反映するように設計されています。 それを解析することで、P について結論を導き出せます。

実行可能ファイルをビルドするためにコンパイラーを使ったことがある、あるいはスクリプトを実行する前にインタープリターに構文をチェックさせたことがあるなら、あなたは静的解析が実際に働いているところを目にしています。

解析それ自体がプログラム（あなたが選んだコンパイラーやインタープリターの内部にあるもの）であり、独自の特殊なアルゴリズムを実行します。それを「解析器」Q と呼びましょう。 私たちは Q を実行して結果を得るので、P（その結果が適用される対象）を実行する必要はありません。 これは静的解析を理解するための、[皮肉にも動的な] 1つの方法です。

具象 vs. 抽象:

動的解析がプログラムを実行することで一連の具象状態を観測するのに対し、静的解析は可能な抽象状態を要約します。 各抽象状態は、一連の具象状態を表します。

プレイヤーが1から10までの数（両端を含む）を選ぶ、単純な「数当てゲーム」プログラムを想像してください。 プレイヤーが 7 を入力すると、プログラムは you win! と出力します。 それ以外の場合は you lose と出力します。

プレイヤーが 3 を入力した実行に対する動的解析では、内部変数 x が 3 に設定され、分岐の片側が選ばれ、対応する you lose 出力が行われることを観測します。 これらはすべて具象イベントです。

ある種の静的解析²なら、このプログラムには2つの抽象状態があると結論づけるでしょう。すなわち、x == 7 の場合に you win! 出力へ至る状態と、x != 7 の場合に you lose へ至る状態です。

静的プログラム解析における課題

ここでは、未知のバグを見つけるための静的解析（前の図の左上の象限）について話していると仮定します。 このユースケースに適用すると、静的なアプローチにはトレードオフがあります。 一般的に言えば、次のとおりです。

• 長所: ドメインから導かれた結論は、プログラムのすべての可能な実行に適用できる場合があります。つまり、あらゆる可能な入力に対して成り立つ可能性があるということです！これは信頼度を最大化するのに役立ちます。

  • 静的解析は、最良の場合、特定のバグクラスが存在しないことを証明できます。

• 短所: 実物ではなく抽象表現を使っているため、静的解析の中には過大近似したり、さらに悪いことに停止しなかったりするものがあります^{3 4}。

  • 過大近似は偽陽性の結果を生みます。つまり、解析の限界により、見つかったバグの多くが本物のバグではないということです。誤った結果のバックログを抱えることは、忙しいエンジニアリングチームの足かせになります。

  • 停止しないことは、解析が決して結果を出力しないことを意味します。これは「状態爆発」、つまり解析が推論しようとしている問題の複雑さが組み合わせ的に増大することが原因で起こる場合があります。永遠に回り続けるのを避けるため、多くの商用ツールは近似によって複雑さを低減します。これもまた、偽陽性のリスクを伴います。

停止するほど実用的でありながら（状態爆発がなく）、偽陽性を一切生み出さないほど賢い（過大近似がない）静的解析アルゴリズムを設計することは、驚くほど多くの場合、不可能です。 「現在の知識と計算能力では不可能」という意味ではありません。 その問題が数学的に決定不能であるという意味で、証明可能に不可能なのです^{5 6}。

• 決定不能とは、任意のケースに対して正しい yes-or-no の判定を下せるアルゴリズムは、今後決して存在しないということです。

よい知らせがあります。アルゴリズム設計者は、賢明なトレードオフを選ぶことができます。 時には、許容できる程度の過大近似を受け入れることを意味します。 また別の時には、規則、制約、仮定、注釈を導入することを意味します。すべては、より精密な解析を実用的にするためです。

Rust も例外ではありません。 この言語はプログラマーに一定の制約を課します。 これらの制約は Rust の学習を難しくし、それによって可能になる解析はコンパイル時間の鈍化を引き起こすことがあります。 チームによっては、それらのトレードオフを受け入れられない場合があります。

すべての静的解析ツールにトレードオフが必要な理由について大まかな直感を身につけられれば、将来出会うどんな静的ツールや技術についても推論できるようになります。 高額なライセンス費用のかかるプロプライエタリな静的解析器も含めてです。 そこで、実践的な文脈で制限を探ってみましょう。ポインター解析です。

ケーススタディ: ポインター解析

ポインター解析（別名「points-to」解析または「may-alias」解析）について、非常に高いレベルで説明します。 そのため、big-step semantics⁷ を用いた Steensgaard のアルゴリズム⁸ の解説は行いません。 私たちの目的は、プログラミング言語（PL）形式論⁹ の「記号のスープ」に溺れることではなく、実践的な直感を築くことです。

なぜこの特定の種類の静的解析を見るのでしょうか？ ポインター解析は、実世界のメモリ安全でないシステムコードに対して性質を検証する際の課題を示す典型例です。 この議論は、Rust が静的に解決する深刻な問題を深く理解する助けになります。 また、この言語の厳格な規則の根拠を理解する助けにもなります。

ポインターとは何か？

C や C++ を書いたことがないなら、おそらく「生ポインター」の恐怖から守られてきたことでしょう。 しかし、Go や Java のような言語でさえ nil/NULL ポインターに対して例外を投げます（Rust はこの「10億ドルの過ち」¹⁰を修正します！）。C 系言語の場合を見てみましょう。

ポインターは、メモリ内の場所のアドレスです。 通常、ただし常にではありませんが、そのメモリは「仮想」です。つまり、マシン上の物理メモリ（CPU キャッシュ、RAM、HDD など）の上にある抽象化です。 機械的には、アドレスは符号なし整数として表現されます。

ポインターは一般に、データ（たとえば配列、構造体、オブジェクト）へ「参照によって」アクセスするために使われます。 これは、潜在的に大きなオブジェクトをコピーする必要がないことを意味します（別名「値渡し」）。 ポインターは従来のシステムプログラミングにとって重要な道具です。 メモリの効率的な利用を可能にします。

しかし、ポインターは諸刃の剣でもあります。 ポインターは、壊滅的な誤用が驚くほど簡単です。 ポインター演算における off-by-one エラーは、誤ったデータを読み取ってもそれに気づかないことを意味し得ます。無効なポインターにアクセスしようとすると、良くてもクラッシュです。攻撃者がポインターの値を設定できるなら、あなたのプログラムは悪用可能かもしれません。 「足を撃つ銃」だと考えてください。

ポインター解析には1つの目標があります:

• 各ポインターが実行時にどの変数やオブジェクトを指す可能性があるかを判定する。

その情報があれば、データがどこから読み取られる可能性があるか、どこに書き込まれる可能性があるかがわかります。 「可能性がある」とするのは、プログラムの実行ごとに異なる場合があるためです。 あらゆる潜在的な実行を代表する可能性の集合が必要です。 この情報により、プログラムについて強く、信頼感を与える主張を行えます。

すべてを欺く一行

その目標を念頭に置いて、次の1行のC関数を考えてみましょう¹¹:

void incr(int* a, int* b) {
    *a += *b;
}

この一見無害な小さな関数は、羊の皮をかぶった狼です。 この関数がより大きなプログラムの一部である場合、ポインター解析では a と b が同じ整数を指す（別名「エイリアス」）かどうかを判断できません。 解析結果は不確定になります。つまり、パラメーターは「エイリアスするかもしれないし、しないかもしれない」と結論づけます。 典型的な過大近似です。

Cを見るのはこれが初めてかもしれないので、ここで何が起きているのかを少し分解してみましょう。

• incr は関数名で、increment の略です。この関数は何かの値を増やすのだろうと推測できます。

• 関数パラメーターは括弧の中に現れます。この関数は a と b という2つの引数を取ります。どちらもメモリ内のどこかに格納された整数へのポインターです。

  • 関数シグネチャ内の * 演算子はポインターを表します。

  • したがって int* は「整数へのポインター」を意味します。

• 戻り値の型である void は、この関数が何も返さないことを示します。したがって、何らかの「副作用」（プログラム状態の更新）を持つのだろうと推測できます。

• 関数本体は、a と b が指す整数それぞれの現在値を（メモリから）読み取り、int b の値を int a に加算し（ポインター加算ではなく整数加算）、その合計で int a を更新します。

  • *a += *b; は *a = *a + *b; の省略形で、セミコロンで終わる文です。

  • ここでは、シグネチャ内とは異なり、* 演算子は「ポインターをデリファレンスする」、つまりその参照先の値を読み取ることを意味します。

  • * は + より優先順位が高く、読み取りが先に発生することを意味します。ポインター算術では優先順位の間違いが厄介になることがあります。

incr を呼び出す前に、int a の値が 40、int b の値が 2 だとします。 ポインター *a と *b は、それぞれメモリ内の対応する整数を次のように指します。

incr(a, b) を呼び出すと、int b が int a に加算されます。したがって呼び出し後は、次のようになります。

それは「慣用的な」Cコードですか？

いいえ。整数は通常、値渡しされます（整数へのポインターではなく、整数そのもの）。 整数はCPUのスクラッチ用メモリの小さな領域、つまり「レジスタ」にきれいに収まるため、そのほうが効率的です。 それでも、私たちの incr 関数は、参照されたデータを操作する日常的なCコードを代表しています。 これから導く結論は広く適用できます。

では何が問題なのでしょうか？

構文を理解してしまえば、incr 関数は非常に単純です。2つの数値を足し合わせるだけです。 なぜこれがポインター解析の実践にとってそれほど大きな課題なのでしょうか？

これらの「生の」（制約のない、という意味¹²）ポインターは、2つの自明でない複雑さをもたらします。

• 1. 決定不能なエイリアシング: 2つのポインターが同じメモリ位置を参照している（エイリアスしている）とします。その場合、a をインクリメントすると b もインクリメントされます。これはプログラマーが意図したことではない可能性が非常に高く、この関数が行うことを変えてしまうエッジケースです。しかし、これが起きないことを証明することはできません⁵。スケーラブルで正確なポインター解析は、依然として未解決の研究課題だからです。

  • 含意: 追加のコンテキスト（incr が呼び出されるすべての場所、別名「コールサイト」など）が与えられても、この関数が実行時に何をするかについて詳細な主張を行うことはできません。以下に示す望ましくないケースは、どのツールでも正確に検出できません。

  • 根本原因: 解析領域内での過大近似です。ポインター解析の設計者は、結果の精度について意識的なトレードオフ（「エイリアスするかもしれないし、しないかもしれない」という結論を許容するなど）を行う必要があります。

• 2. 複雑なメモリモデル: 生ポインターは無効なメモリ位置に設定される可能性があります。プログラマーがオフセットを計算するときにポインター算術のバグを混入させることもあります。あるいは単に、ポインターを「未初期化」のままにする（Cにおけるデフォルト状態）こともあります。

  • 含意: ポインターのデリファレンスはクラッシュにつながる可能性があります。あるいは任意のデータの読み取りや書き込みになる可能性もあります（クラッシュはしないが、プログラムの出力や挙動が不正になる）。

  • 根本原因: 解析領域外での過大近似です。これは抽象化境界の産物です。この場合は、ハードウェア/ソフトウェアインターフェイスにおけるセマンティクスの違いです。

まとめましょう。 エイリアスでしょうか？ プログラムが期待どおりに振る舞わないかもしれません。 私たちには判断できません。 無効なポインターでしょうか？ プログラムがクラッシュするかもしれませんし、別の値が上書きされて不正になるかもしれません。 やはり、これが起きないことを証明することはできません。

incr 関数は単純に見えますが、静的保証にとって克服できない課題を生み出します。 このプログラムが意図した加算を実行すると主張することはできません。 指し示せる証明がなければ、私たちの確信は低いままです。

現実世界におけるポインターエイリアシング問題

オープンソースのCコンパイラーである gcc は、効率的なコードを生成することを目指しています。 任意の2つのポインターがエイリアスするかどうかを確実に判断することは不可能なので⁵、gcc は少しずるをします。-O1 より大きい最適化レベルでは、2つのポインターが異なる型を指している場合、コンパイラーはそれらがエイリアスしないと仮定します。 この仮定により、影響の大きい特定の最適化が可能になります。

しかし実際には、Cプログラマーがこの仮定に違反することがあります（「型パンニング」と呼ばれるテクニックがあります）。 そのような場合、最適化によって厄介なバグや予期しない挙動が生じる可能性があります。 そのため、Linuxカーネルでは gcc フラグ -fno-strict-aliasing によって、この最適化が明示的に無効化されています^{13 14}。

ポインター問題のまとめ

静的解析には2つの失敗モード（相互排他的ではありません）のリスクがあります。過大近似、および/またはスケールしない/終了しないことです。 どちらも、静的解析ツールから引き出せる保証価値を制限します。 メモリ安全でない言語に対するポインター解析は、現実世界の問題を過大近似せざるを得ない古典的な例です。 ポインター（例: 自由に制御できるメモリアドレス）はシステムプログラミングにとって便利な抽象化ですが、実行時について自動的に推論する能力を著しく損ないます。 人間にとっても、それを正しく扱うのは困難です（ポインターは、C プログラムが「segmentation fault」¹⁵クラッシュで悪名高い理由の一部です）。

生ポインターは、既存の C/C++ コードからメモリ安全性の問題を排除することが現実的でない理由の 1 つにすぎません。 少なくとも、後方互換性を壊さずに行うことはできません。 覚えておいてください。メモリ安全性は、数十年にわたって困難であり続けている問題です。 多くの人が挑戦し、そのほとんどは失敗してきました。

Rust がポインターの問題をどのように扱うのか、少し見てみましょう。

不正確な解析でも有用であり得る！

ポインター解析には近い親戚があります。それが Value Set Analysis（VSA）です。 これはコンパイル済みバイナリに適用でき、ソースコードが利用できないユースケース（例: リバースエンジニアリング）を支援します。 ポインター解析とは異なり、VSA はポインター変数と整数変数を区別しません。 どちらの種類の数値変数についても、実行時に取り得る値の範囲を計算します。

上記の incr の例では、正しいプログラムに対する精密な VSA は、整数 a が [40, 42] という両端を含む値範囲を持つと判断するかもしれません。これはインクリメント前とインクリメント後の両方の値を捉えています。そしてポインター *a も同様に、有効なメモリアドレスの何らかの範囲内にあり、概念的には [0x7ffe455e5c40, 0x7ffe455e5bf0] のようなものになります。

ここが重要です。最近の査読付きヒューマンスタディ¹⁶では、不正確な（例: 過大近似の）VSA の結果であっても、プログラムが機密情報を出力するかどうか（例: 「情報漏えい」脆弱性を見つける）を判断するリバースエンジニアの能力を向上させることが示されました。 不正確な VSA の結果を利用することで、経験の浅いリバースエンジニアでも、特定の問題タイプについては、支援を受けない経験豊富なリバースエンジニアと同等の性能を発揮できました¹⁶。

近似的な静的解析は、多くの文脈において、実証的に有用であり得ます。

1. 抽象解釈: 不動点の構成または近似によるプログラムの静的解析のための統一束モデル. Patrick Cousot, Radhia Cousot (1977). ↩

2. プログラム変数に対する制約（x != 7 のようなもの）に従って結果を分解することは、「シンボリック実行」の特徴です。これは特に強力なプログラム解析です。理論上、シンボリック実行は純粋な静的解析です。しかし実際には、具体的な動的実行からのフィードバックを用いて実装されることが多くあります（別名「コンコリック実行」）。 ↩

3. 17-355/17-665/17-819 プログラム解析. Jonathan Aldrich et al, Carnegie Mellon University (2021). ↩

4. CIS 547 ソフトウェア解析. Mayur Naiak et al, University of Pennsylvania (2021). ↩

5. ポインターが引き起こすエイリアシング: 問題の分類. William Landi, Barbara Ryder (1990). ↩ ↩2 ↩3

6. 精密なフロー非依存 May-Alias 解析は NP 困難である. Susan Horowitz (1997). ↩

7. 講義 11: ポインター解析. Rohan Padhye, Jonathan Aldrich. Carnegie Mellon University (2021). ↩

8. ほぼ線形時間での Points-to 解析. Bjarne Steensgaard, Microsoft Research (1996). ↩

9. そうは言っても、形式的な記法には価値があります。それを学ぶことで、特定の問題についての考え方が変わることがありますし、少なくとも最先端の研究論文を読めるようになります。 ↩

10. Null References: 10 億ドルの過ち. Tony Hoare (2009). ↩

11. より安全な Rust: Creusot によるプログラム検証. Xavier Denis (2021). この講演から借用した関数は、Rust の型システムが検証をどのように支援するかを示すために使われました。次のセクションではこの考えを探りますが、異なる文脈で扱います。 ↩

12. ただし、ここでの「無制限」とは、現在の実行環境に対して相対的なものです。OS がプログラムに割り当てたプロセス空間のような「サンドボックス」（メモリセグメンテーションの強制）は存在します。このような制限により、あるプログラムのバグやエクスプロイトが他のプログラムや OS 自体に影響を及ぼす可能性が低減されます。 ↩

13. Re: gcc inlining heuristics was Re: [PATCH -v7][RFC]: mutex: implement adaptive spinning. Linus Torvalds (2009). ↩

14. 未定義動作: 私のコードに何が起きたのか？. Xi Wang, Haogang Chen, Alvin Cheung, Zhihao Jia, Nickolai Zeldovich, M. Frans Kaashoek (2012). ↩

15. 「segmentation fault」、略して「segfault」は、プログラムが自分に属さない（割り当てられた「セグメント」の外側の）メモリ領域にアクセスしようとしたときに、オペレーティングシステムによって送出されるエラーです。デバッグは苛立たしいものになり得ますが、OS が止めてくれなかったらどれほど大変になるか想像してみてください！ ↩

16. 精密および不精密な Value-Set Analysis（VSA）情報が手動コード解析に与える影響. Laura Matzen, Michelle Leger, Geoffrey Reedy (2021). ↩ ↩2