数十年にわたるC言語の脆弱性に関する理論

付録II: 意味論的イヌバリアントの理論 - C言語の脆弱性からメモリ安全な言語設計へ 欠けている概念 この本の中心的な主張は、単一のアイデアで表現できます。意味論的イヌバリアントとは、プログラムが意図したデータとメモリで操作を継続するために、プログラムの実行中に真であり続けなければならない値、オブジェクト、または関係性に関する性質のことです。 C言語にはこのようなイヌバリアントが満ちています。`length`という名前の変数は、バッファで利用可能なバイト数を示すことを意図しているかもしれません。`count`という名前の変数は、配列内の要素数を示すことを意図しているかもしれません。ポインタは、割り当てられたオブジェクトの開始位置を示すことを意図しているかもしれません。オフセットは、そのオブジェクト内に留まることを意図しているかもしれません。ポインタは、特定の操作が完了するまで有効であると想定されているかもしれません。2つのポインタは、メモリの異なる領域を参照していると想定されているかもしれません。 これらの仮定のどれも単なるプログラムに関するコメントではありません。それらは、後続の操作の正しさが依存する意味論的な事実です。 問題は、標準的なC言語が一般的にこれらの関係性を、それらを運ぶ値の型の一部にしていないことです。C言語は、値が`size_t`型であることを教えてくれます。通常の型システムでは、その値がバイト数、要素数、割り当てサイズ、バッファ容量、オフセット、または入力の長さを表すかどうかを教えてくれません。C言語は、値が`char *`型であることを教えてくれます。一般的に、そのポインタからアクセス可能なオブジェクトの範囲、そのオブジェクトの所有者、それがどれだけ長く生存するか、またはそのアドレスから安全にアクセスできるバイト数が特定されているかどうかを教えてくれません。 結果として、単にC言語に「安全でない操作」が含まれているだけではありません。より深い問題は、それらの操作を安全にするために必要な意味論的な関係性が、言語によって強制されるイヌバリアントではなく、プログラマーの推論における非公式な義務として維持されていることです。これは、驚くほど広範囲のセキュリティ脆弱性に対する一般的な理論的説明を提供します。 整数オーバーフロー、バッファオーバーフロー、境界外アクセス、use-after-free、double freeは同じバグではありません。それらはプログラムの異なる時点で発生し、異なる即時メカニズムを伴います。しかし、それらはしばしば、壊れた意味論的イヌバリアントの異なる失敗の現れとして理解できます。脆弱性とは、プログラムの現実の表現が現実と一致しなくなる時点のことです。 1. 意味論的イヌバリアントとは何か？ イヌバリアントとは、プログラム実行のある領域全体で真であると期待される命題です。以下を検討してください。 size_t count; size_t size; char *p; C言語の型システムは、これらの値間の関係性についてほとんど教えてくれません。しかし、プログラマーはより豊かな命題のセットに依存しているかもしれません。 count は要求された要素数を示す size は count 要素に必要なバイト数を示す p は少なくとも size バイトのストレージを指す p + offset へのアクセスはそのストレージ内に留まる length は残りの範囲を超えない p はアクセスが完了するまで有効である これらは意味論的イヌバリアントです。それらは宣言で見えるとは限りません。プログラムはそれらのすべてに依存している可能性があります。 この区別は基本的です。型は、言語によれば値が許可されるものを言います。意味論的イヌバリアントは、特定のプログラムでその値が何を意味し、後続の操作が有効であるためにどのような関係性が真であり続けなければならないかを言います。 例えば： size_t length; これは意味しません： length はバッファ p の有効な長さである それは単に `length` が C の `size_t` 型であるという意味だけです。より強い命題は、次のようなものです。 0 <= length <= extent(p) ここで `extent(p)` は `p` から始まるメモリの有効にアクセスできる量を表します。その命題は、次のようなことを安全にします。 memcpy(p, source, length); C言語は一般的に、`length` と `p` の値と共に命題 `length <= extent(p)` を運びません。プログラマーがそれを確立しなければなりません。 2. 意味論的な連鎖 多くのメモリ脆弱性は、依存する命題の連鎖として理解できます。単純化された例は次のとおりです。 size = count * element_size; p = malloc(size); q = p + offset; memcpy(q, source, length); 一見すると、これは単なる通常のC操作のシーケンスです。しかし、意味論的には、それは連鎖を表します。 count | v 要求されたサイズ | v 割り当てられた範囲 | v オブジェクトの識別 | v オフセット | v 残りの範囲 | v コピーの長さ | v 有効なメモリアクセス 各関係はイヌバリアントを表します。例えば： size = count * element_size は、`count` が実際に意図された要素数を示し、乗算がオーバーフローなしで意図されたサイズを生成するというイヌバリアントに依存します。次に： p = malloc(size) は、割り当てられたサイズがプログラマーが構築しようとしている論理オブジェクトに対応するというイヌバリアントに依存します。次に： q = p + offset は、`offset` がそのオブジェクト内の適切な位置にあることに依存します。最後に： memcpy(q, source, length) は、`length` が宛先の残りの範囲を超えず、ソースと宛先が操作の要件を満たすことに依存します。 連鎖の早い段階での失敗は、ずっと後になるまで明らかにならないことがあります。これが、脆弱性が `memcpy` で発生したように見えるのに、実際の意味論的な失敗はもっと前に起こった理由です。 3. 整数オーバーフロー：意味の最初の失敗 整数オーバーフローはしばしば算術的な問題として説明されます。セキュリティクリティカルなCコードでは、それを意味論的な意味の失敗として見る方がより有用です。仮に： size_t size = count * element_size; プログラマーの意図： size = count 要素を格納するために必要なバイト数 計算がその数学的な量を表さない場合、変数 `size` はもはやプログラマーが信じている意味を持ちません。意味論的イヌバリアントが失敗しました： 意図されたサイズ = 表されたサイズ 脆弱性はまだメモリ違反ではないかもしれません。プログラムはまだ正常に実行されるかもしれません。失敗は後で現れます： p = malloc(size); 今、割り当ては意図されたよりも小さくなっています。プログラムは意味論的な境界を越えました： 数学的な量 | v 表現された整数 | v 割り当てサイズ したがって、最初の不正確な値が後でメモリ安全違反を引き起こす可能性があります。 radare2 の CVE-2019-19590 は有用な例です。この脆弱性は、トークン割り当てサイズの計算における整数オーバーフローと、それに続くトークンバッファを含む use-after-free に関連していました。したがって、整数エラーは孤立した算術的欠陥に留まりませんでした。それはプログラムのメモリモデルに伝播しました。 CVE-2022-37454 は別の例を提供します。Keccak XKCP SHA-3 実装の脆弱性は、バッファオーバーフローを引き起こした整数オーバーフローを含んでいました。CVE カテゴリは異なるのは、それらが異なる観測可能な失敗を記述しているためです。しかし、意味論的には、それらは単一の連鎖を形成する可能性があります。 攻撃者が制御する量 | v 整数計算 | v 意図された割り当てサイズ | v 不正確な表現サイズ | v 不正確なメモリ関係 | v メモリ破損 整数オーバーフローは、壊れたイヌバリアントの一つの現れです。最終的なメモリ破損はもう一つの現れです。 4. バッファオーバーフロー：範囲イヌバリアントが失敗した 不正確なサイズが割り当てに到達すると、次のイヌバリアントは空間的なものです。アクセスされているメモリ領域は、操作が想定しているよりも少なくとも大きい必要があります。 プログラマーが信じていると仮定します。 p -> 100 バイト しかし、以前の計算が実際には次のような結果になったとします。 p -> 60 バイト ポインタ自体は完全に有効かもしれません。割り当ては成功したかもしれません。プログラムはこれまでのすべてのローカルテストに合格したかもしれません。失敗は、プログラムが後で誤った範囲を想定したときに発生します。例えば： memcpy(p, source, 100); 意味論的な主張は次のとおりです。 extent(p) >= 100 しかし現実は次のとおりです。 extent(p) = 60 したがって、コピーは単に「memcpy の悪い呼び出し」ではありません。それは、以前に壊れた範囲イヌバリアントが観測可能なメモリ破損になる時点です。