はじめに

この連載では、C++ の整数型の奇妙な特性、そしてその中で整数オーバーフローを引き起こさないためのオーバーフローチェッカーをどう書くか、について主に解説します。

第2回では、割とすぐ役に立つはずの "符号無し整数型" のチェックをどう実装するかについて主に解説します。

連載インデックス

オーバーフローチェックの追加条件

第1回で書くのを忘れていた追加条件です。私の整数オーバーフローチェッカーは、次の条件をも満たしている必要があると考えました。

整数オーバーフローチェッカー自体に整数オーバーフローなどの未定義動作、実装定義の値の評価を含まないこと (割と細則)
整数オーバーフローチェッカーは、オーバーフロー "するか" "しないか" を正確に判定すること

2 番目の条件は地味ですが、強力で、実装上は面倒なものです。実のところ、整数型の中で使用する値の範囲を制限さえしてしまえば (つまり整数オーバーフローが発生しない場合でも "する可能性がある" と返すことができるものとすれば)、整数オーバーフローのチェックはより簡単に書くことができます。しかし、そうすると幾つかの問題が出てきます。

処理系の提供する整数型をフルに活用することができない
整数オーバーフローチェッカーを実装する上での積み木にするには不安定になる (その不安定さの結果、使用できる整数型の値域がさらに制限される)

後者は特に重要です。私が整数オーバーフローチェッカーを書けることを証明してしまった (してしまった、の意味は~~第3回~~第4回で解説) ときには、無条件に整数オーバーフローを発生させない演算を列挙し、そこから精緻な論理を積み重ねることで他の演算の整数オーバーフローチェッカーを書けることを証明していきました。ここで "余裕を持った" (整数オーバーフローが発生しなくとも発生すると返してしまう) オーバーフローチェッカーを積み木として利用してしまった場合、上段の論理も (下段以上に) 不安定なものになってしまうのです。

私が用いた Coq においては、これは "整数オーバーフローチェッカーが安全と判断する条件" と "整数オーバーフローが発生しない条件" が論理的に同値であること (言い換えれば、整数オーバーフローチェッカーが安全と判断する条件は実際に整数オーバーフローが発生しない必要十分条件であること) を証明すれば良いことを示します。

Coq においてどう定義、証明するか

Coq において、C++ の符号無し整数をどう定義するか、というのはやや問題でした。C++ 規格書の定義を見る限りでは、n ビットの符号無し整数型は 2^n の異なる値 (0～2^n-1) を表現することができます。しかし、2^n という値を証明の中に取り入れるのはやや面倒なところがありました。

そのため、私の Coq 証明においてはそれを一般化した (符号無しで最大値が存在するなら 2 進表現でさえなくとも良い) 条件の元で証明することにしました。C++ の符号無し整数型 (後述の nmax が特定の条件を満たす値に限られる) は、この定義の系として得られます。

符号無し整数型の整数は、

0 <= n <= nmax (0 < nmax) を満たす

符号付き整数 n

として定義する。

実際には符号を持たない C++ の符号無し整数を Coq 内では符号付き整数 (Z 型) として証明に写しこんだのは、証明を行う際には (自然数では満たされない) 整数の性質の良さが際立つからです。どのみち 0 <= n という条件があるので、n が負になることはできません。

また nmax を型の表現可能範囲内 (不等号に等号がついていることに注意) に入れたのは、nmax 自体を (std::numeric_limits<T>::max() のような) 同じ符号無し整数型の値として扱いたかったからです。

これを満たした上で、例えば符号無し整数型同士の加算 (a + b) のオーバーフローチェッカーが b <= nmax - a として書けることは、Coq において次の式で表現されます (ここでは具体的な証明は省略)。

Theorem overflow_safety_unsigned_add :
    forall (a b nmax : Z),
        0 < nmax ->
        0 <= a <= nmax ->
        0 <= b <= nmax -> (
            0 <= a + b <= nmax
            <->
            b <= nmax - a
        ).
(* 末尾 5 行の括弧は本来不要だが、読み間違えることがないようわざと囲っている。 *)

0 <= a + b <= nmax が、a + b がなお符号無し整数型の表現可能範囲内にあることを示す論理式、b <= nmax - a がそれに対応する整数オーバーフローチェッカーの式です。

ここで注意しておきたいのは、整数オーバーフローチェッカーの内部で使用されている nmax - a については、上記の定理内において自身が整数オーバーフローを起こさないことを証明していない、ということです。そのため、これが整数オーバーフローを引き起こさないということ (0 <= nmax - a <= nmax であること) を、別の補題として証明します。

Lemma overflow_safety_unsigned_add_expr :
    forall (a nmax : Z),
        0 < nmax ->
        0 <= a <= nmax ->
        0 <= nmax - a <= nmax.

このふたつが揃うことではじめて、C++ において、完全に規格準拠、移植性があり、かつ false positive / false negative の無い整数オーバーフローチェッカーが書けることを証明できたこととなります。具体的な Coq コードは後日 (この連載の最終回公開前に) 公開予定の ZSafeInt 証明部をご覧頂くとして、次の章から符号無し整数型に対する四則演算のオーバーフローチェッカーと証明の概略をご覧頂きましょう。

証明概略と C++ コード

減算 (`a - b`)

これは簡単ですね。b <= a です。a より大きい値を引こうとしたら負になるため、b は a と同値かそれより小さくなくてはなりません。

// Tu は符号無し整数型 (型チェックに必要な static_assert などは省略)
template <typename Tu>
static inline constexpr bool is_subtraction_safe(Tu a, Tu b)
{
    return b <= a;
}

加算 (`a + b`)

符号無し整数型における演算 a + b が整数オーバーフローを引き起こさない条件は、b <= nmax - a です。これは a + b <= nmax から a を移項させる (両辺から a を引く) ことによって容易に証明することができます¹。ここで nmax - a という式が出てきますが、a <= nmax を満たす (上記の減算のオーバーフローチェッカーを参照) ことから nmax - a が整数オーバーフローを引き起こすことはありません。

簡単な C++ コードに直すと、以下の通り。

#include <limits>

// Tu は最大値のある符号無し整数型 (型チェックに必要な static_assert などは省略)
template <typename Tu>
static inline constexpr bool is_addition_safe(Tu a, Tu b)
{
    return b <= std::numeric_limits<Tu>::max() - a;
}

除算 (`a / b`)

b != 0 という条件は当然ゼロ除算を避けるために必要ですが、それ以外に必要な条件はありません。a の正の整数 b による除算結果は a と同じ符号 (つまりこの場合は正) になり、絶対値は a の絶対値以下となるためです。

// Tu は符号無し整数型 (型チェックに必要な static_assert などは省略)
template <typename Tu>
static inline constexpr bool is_division_safe(Tu a, Tu b)
{
    return b != 0u;
}

乗算 (`a * b`)

四則演算の中で最も難しいのが乗算のオーバーフローチェッカーの証明です。これは a * b <= nmax を変形して b <= nmax / a とすることができますが、その中で起こりうるゼロ除算を排除する必要があります。

#include <limits>

// Tu は最大値のある符号無し整数型 (型チェックに必要な static_assert などは省略)
template <typename Tu>
static inline constexpr bool is_multiplication_safe(Tu a, Tu b)
{
    return !a || b <= std::numeric_limits<Tu>::max() / a;
}

剰余 (`a % b`)

剰余は四則演算と異なり、C/C++ 規格において移植性のある値が定義されるか否かが除法 a / b が定義されるか否かと完全にリンクしています。そのため証明戦略はやや異なり、a / b (ただし b != 0) が符号無し整数型の範囲内にあれば、a % b もまた符号無し整数型の範囲内にある、という一方向の定理を証明します。これが証明されれば、剰余の安全性は除算の安全性として記述することができます。

Theorem overflow_safety_unsigned_mod_from_div :
    forall (a b nmax : Z),
        0 < nmax ->
        0 <= a <= nmax ->
        0 <= b <= nmax ->
        0 <> b ->
        (* 0 <= a // b <= nmax -> *)
        0 <= a %% b <= nmax.

ここで // と %% という中置演算子は、C99/C++11 の規格の条件を満たす (Coq デフォルトの / および mod 演算子とは異なる) 除算と剰余を示すもので、私が証明ライブラリ内で定義したもの²です。この定理を証明してみると、a / b (Coq コードにおいて a // b) が範囲内にある、という条件は、実際には必要ありませんでした。そのため、その部分はコメント化されています。

対応する C++ コードは次の通り。

// Tu は符号無し整数型 (型チェックに必要な static_assert などは省略)
template <typename Tu>
static inline constexpr bool is_remainder_safe(Tu a, Tu b)
{
    return is_division_safe<Tu>(a, b); // b != 0u
}

その他の演算

ここまでで、符号無し整数型の四則演算、そして剰余を網羅しました。左右シフトについては乗除で表現できるので (実装する際の事前チェックがやや面倒な程度)、四則演算、剰余、そして左右シフトまでのオーバーフローチェッカーを書けることを証明したこととなります。ビット演算については符号無し整数型の範囲では表現に依存する処理系依存の問題を持つことはないので、これで符号無し整数型は攻略したといっても良いと思います。

あとがき / 次回予告

第2回では、簡単な話題を扱いました。符号がない場合には、各種の証明はかなり楽に扱えるものです。ここまでは頭の体操、ウォーミングアップといっても構いません。~~第3回~~第4回では、より複雑になっていく符号付き整数の話題について、そして、第1回で話した "動機" のさらに動機について、解説します。

解答 1 : ひとつ、もしくはふたつの整数オーバーフロー

第1回で出題した練習問題の答えです。ふたつの (潜在的な) 整数オーバーフローの答えは次の通り。

size に非常に大きな値が与えられると、size + 4 で整数オーバーフローを起こす
new 演算子の評価中、確保しなければならない配列のサイズ sizeof(int) * (size + 4) 計算の乗算中に整数オーバーフローを起こす可能性がある

大きな値の整数オーバーフロー

size に、例えば SIZE_MAX (size_t の最大値) が与えられたとしましょう。そうすると、size + 4 の計算の中で整数オーバーフローが発生し、(SIZE_MAX - 0) + 1 でモジュロを取った結果である 3 が配列確保に用いられることとなります。

Twitter での反応を見る限り、こちらに関しては即正しい答えを出せた方が多かったようです。

小さな値の整数オーバーフロー

さて、問題はこちらの方です。new で配列を確保する際、内部的には乗算を用いることで確保すべきメモリサイズが計算されます。実は、この中で整数オーバーフローが発生することがあるのです。

C++03 以前においては、練習問題に挙げたコードはおおむね次のようなコードに変換することができます (ネタバレになりますが、C++11 以降ではこのような内部的変換は許されません)。

size_t size;
/* ... (どこかで size を設定。ただし、攻撃者は size を任意の値に設定することができるものとする) */
int* buf = static_cast<int*>(malloc(sizeof(int) * (size + 4)));
if (!buf)
   /* std::bad_alloc を送出 */

この中に存在しうる乗算で整数オーバーフローが発生する場合、(おそらく³) 未定義の挙動が発生します。先述した単純なコードに置き換えた場合は、オーバーフローによって切り捨てられた値がそのままメモリ確保に用いられてしまい、誤ったサイズのバッファが返ることになります。これは、大きな値の整数オーバーフローより数段危険なことです。

最初に示した size + 4 のオーバーフローで異常な形で得ることができるのは、int 型 0～3 個分のバッファのみです。配列確保後すぐその大部分に対して初期化が行われるなら、非常に大きなサイズのバッファオーバーフローによってプログラムをほとんど瞬時にクラッシュさせます。これを用いて任意コードを実行するのは状況にもよりますが一般に不可能に近いです (一概にバッファオーバーフローといっても、攻撃者目線で見ると "使いやすいもの" と "使いにくいもの" が存在するのです)。

対して、sizeof(int) が 2 以上で、かつ前述のような単純なコード変形が成されるような処理系を対象とした攻撃では、攻撃者は (あくまで条件次第となりますが) バッファオーバーフローによって上書きするメモリのサイズをより自由に選択できます (クラッシュ⁴させずに任意コードを実行させるための誘導が困難とはいえ容易になる)。そのため、こちらの方が攻撃者にとっての利用価値が高くなります。

new による配列確保において整数オーバーフローが問題になるのは、次の両方の条件を満たした場合です。

sizeof(int) が 1 を上回る
C++03 以前の規格準拠で上記のような単純なコード変換を行う処理系である

驚くべきことに、C++11 ではこの問題に対して規格の修正によって対応しています。また、C++03 以前準拠の処理系でもコンパイラ独自機能によって対応を行うものがあります (未定義挙動に対しては、このような安全策を取ることも規格実装上可能です)。

小さな値の整数オーバーフロー ……への対策!

C++11 規格による対処

C++11 では、5.3.4 p7 に新しい明文化された規定があります。ISO/IEC 14882:2012 より引用、抄訳すると:

(前略) expression (訳注: 配列版 new を用いて確保する配列の要素数、多次元配列においては先頭の要素) にゼロより小さい値、もしくは確保されるオブジェクトのサイズが実装定義の制限を超えうるような値が指定された場合、あるいは (中略)、メモリ領域は確保されず、std::bad_array_new_length 型の例外ハンドラにマッチする例外を送出することによって new-expression は強制終了します。

つまり、整数オーバーフローないしはその他の要因によって正しいサイズのメモリ領域を確保できない (ないしはその可能性がある⁵) 場合、誤ったサイズのメモリは確保されないように規定されました。この規定に厳密に対応している場合、std::bad_array_new_length 例外は std::nothrow を使っていても発生するために追加で例外ハンドリングを行う必要はあるでしょう。しかしほとんどの場合、既存の C++ プログラムでも C++11 対応コンパイラ (の C++11 モード) でコンパイルし直すだけで追加の安全性を得ることができる可能性がある、ということは知っておいても良いかもしれません。

現状この規定に厳密に準拠する主要コンパイラは、残念ながら gcc 4.9 以降のみです (Clang は開発版にて一時規格準拠したのですが、何らかの理由により規格非準拠の状態に差し戻されました)。それでも、C++11 対応を謳うほとんどの主要コンパイラや C++03 以前にのみ準拠するコンパイラの一部は、明文化された規約がなくとも (あるいは規格に準拠した例外を出さずとも) この種のチェックだけは行います。

コンパイラ独自機能による対処

繰り返しになりますが、ここではコンパイラが未定義の動作をどのようにでも扱って良い、ということが重要になります。コンパイラは効率のためそのようなケースを事実上放置しても良いですし、逆にコード生成時に安全側に倒しても構わないわけです。

Visual C++ 2005、gcc 4.8、Clang 3.0 などでは、配列版 new において整数オーバーフローのチェックを行い、整数オーバーフローが発生する (gcc においてはその "可能性がある") 際には代わりに SIZE_MAX バイトのメモリを確保させようとします。SIZE_MAX バイトのメモリ確保は通常失敗するはずなので、これにより std::bad_alloc 型のハンドラにマッチする⁶ 例外が送出されたり、有効なメモリの代わりにヌルポインタが返されることとなります。

このように、コンパイラによっては上記の整数オーバーフローに起因する攻撃のうちひとつは成立しません。ただ移植性のあるプログラムを書く際には、当然このような処理系依存のものに頼るわけにはいきません。そのため、C++11 において規格によって対処されたことが重要になるわけです。

練習問題 2 : 誤った整数オーバーフローチェッカー

負の数同士の除算 a / b (nmin <= a && a <= 0、nmin <= b && b < 0) のオーバーフローチェッカー (nmin <= a / b && a / b <= nmax; 除数が負であるため何らかのチェックを行う必要がある) を作成するために a / b <= nmax という式を変形して、チェッカー内の整数オーバーフロー、そして b がゼロである場合を考えないとき nmax * b <= a という途中式 (負の数を両辺に掛け算したので不等号の左右が逆になっている) を得ました。……が、この式はその中で整数オーバーフローが起きず、b が常に 0 以外と仮定したときでさえ誤っています。何故、このような誤りが起きたのでしょうか?

これについては明確な答えを出す必要は特にありませんが、~~第3回~~第4回で解説する内容をより良く理解するために、あるいは、直感的な推論がいかに誤りやすいかを知るために考えておくと良いでしょう。

現況

符号付き整数型の証明 (第1回時点では未完成と報告): 完成 (証明のさらなる整理などを実施中)
C++ ライブラリ: 実装中

ここで Coq の符号無し整数型 (0 を含む自然数型) である N を使っていると、それだけで証明が膨れ上がります。 ↩
C++ 規格書においては各種演算の多くは統一された、型の精度とは関係ない形で記述され、加えて結果がそれを格納する型に入らない場合にどうなるかなどの個別ケースが記述されます。そのため、私は証明ライブラリにおいて整数型の精度とは無関係の cdiv / crem 関数 (後で Coq が提供する Z.quot および Z.rem 関数が同じ値を返すことに気づいてしまったが時既に遅し) を定義し、中置演算子にそれぞれマッピングを行いました。 ↩
おそらく、と書いたのは、実は C++03 規格書内に明確な定義が無いからです。未定義動作と推察はできますが、明確に禁止されていないのがなんとも薄気味悪い。 ↩
プログラムの敗北、ではあります。しかし、攻撃者の目的が破壊工作自体でない場合、クラッシュというのは攻撃者にとっての失敗にすぎない、という考え方も可能です。実際、OS やコンパイラに組み込まれたメモリ保護機能の多くは攻撃者によるコード実行を許すくらいならプログラムをクラッシュさせることを意図的に選択するでしょう。 ↩
例えば gcc においては、7 ビット精度の定数 (任意の定数を生成するのが大変な一部 RISC 系アーキテクチャへの配慮?) を用いて要素数が大きすぎるか否かをチェックします。つまりかなり大きな要素数を確保しようとすると、実際には整数オーバーフローを起こさない場合でも実装定義の制限を超えうるとしてエラーを発生させます。 ↩
std::bad_array_new_length は std::bad_alloc のサブクラスであるため、std::bad_alloc をキャッチする/しているなら std::bad_array_new_length の方を追加でキャッチする必要は通常ありません。 ↩

C++ における整数型の怪と "移植性のある" オーバーフローチェッカー (第2回 : 符号無し整数型のチェック)