sec9 - Splint翻訳 Wiki - Splint翻訳

Up: マニュアル

Prev: 8 Control Flow（制御フロー）

Next: 10 Extensible Checking（拡張可能なチェック）

Section：1　2　3　4　5　6　7　8　9　10　11　12　13　14　A　B　C　D　E

9 Buffer Sizes（バッファーサイズ）

バッファオーバーフローエラーは C言語のプログラムでは特に危険なバグの典型です。 それらは、全てのセキュリティ攻撃の約半分の、直接の原因です[Larochelle01]。 パフォーマンス上の理由のため、C言語では実行時に境界チェックは行われません。 割り当てられた領域外への記憶領域への参照は、 メモリ破壊を引き起こしたり、予想外の動作につながったりします。 その上、特にバッファオーバーフローバグは潜伏性があります。 なぜなら、それらは試験や通常の使用では検出されません、しかし、 通常セキュリティ上の重大なバグにつながります。 バッファの終わりを超えて読み出すと、プログラムに情報をリークさせます。 バッファの終わりを超えて書き込みをすると（バッファオーバーフロー）、通常、 プログラムに任意のコードを実行させて、悪用されます。 攻撃者はスタック上の戻りのアドレスを換えたり、メモリ上に任意のコードを 置いて、それによって、マシンへの全アクセス権を得たりするために これらのプログラミングのバグを悪用できます。 Splintは多くのメモリ境界エラーを検出することが出来ます。^*12

9.1 Checking Accesses（アクセスチェック）

Splintは2つのプロパティ（ maxSet と maxRead） を使用して連続するメモリのブロックをモデル化します。 バッファーbを考えると、 maxSet(b)は 左辺値として安全に使用できるbの最大アドレスを示します。 char buf[MAXSIZE]の宣言に対して、我々は、 maxSet(buf) = MAXSIZE - 1を持ちます。 同様に、maxReadは 右辺値として安全に使用できるバッファーのインデックスの最大値を示します。 これは初期化されていない要素やnull終端バッファのNUL終端を越える読み出しには不適切です。

バッファーが左辺値としてアクセスされるとき、 SplintはmaxSetプロパティに関連する 前提条件を生成します。 バッファーが右辺値としてアクセスされるとき、Splintは maxReadプロパティに関連する 前提条件を生成します。 式*ptrに対して、 Splintは、ptrが左辺値が右辺値の どちらで使用されるかによってmaxSet(ptr) >= 0 あるいは maxRead(ptr) >= 0の条件を生成します。 同様に、ptr[i]形式のアクセスに対しては、 SplintはmaxSet(ptr)>= i あるいは maxRead(ptr) >= iの条件を生成します。 +boundswriteフラグが設定されている場合、 maxSetに関係する条件を解決できなかったときに、 Splintは警告を発します。 +boundsreadフラグが設定されている場合もまた、 解決できなかったmaxReadの条件についてSplintは警告を発します。

Splintは前提条件の制約を解決するための文に対して 事後条件を生成します。 バッファーが書き込まれたとき、我々はバッファの要素が初期化され、 安全に読み出せることを知っています。 我々は、バッファが*ptrを使用して アクセスされるときには、maxRead(ptr) >= 0を、バッファがptr[i]を使用してアクセスされるときには maxRead(ptr) >= iの事後条件を生成します。 SplintはさまざまなC言語の構造体に対して付加的な事後条件を生成します。 代入文に対し、Splintは2つのオペランドを同等とする事後条件を生成します。 Splintはまた、固定サイズの配列のmaxSet値に対して 事後条件制約を生成します。

9.2 Annotating Buffer Sizes（バッファーサイズのアノテーション付け）

関数の宣言は、関数の前提条件に対するバッファーサイズについての仮定を規定する requires句とensures句を含んでもかまいません。それらは、単純なメモリ状態（Section 7.5参照）に対しての requires句とensures句の様に解釈されますが、しかし、より表現力があります。 requires句付きの関数が呼び出されたとき、呼び出し側はrequires句によって暗に含まれる制約を安全にチェックする必要があります。同様に、ensures句は関数の事後条件を指定するために使用されます。 +checkpostフラグが設定されている場合で、関数の実装が宣言されている事後条件を満たしていると確認できなかった場合、 Splintは警告を発します。

制約は、グローバル変数や整数制約と同じように関数の引数に含めることが出来ます。上記のプロパティに対応する単項演算子、maxSetとmaxReadもまた、サポートされています。複数の述部は/\を使用して連結されてもかまいません。

例えば、標準ライブラリは strcpyにアノテーションを付けます。

void /*@alt char * @*/strcpy

(/*@unique@*/ /*@out@*/ /*@returned@*/ char *s1, char *s2)
/*@modifies *s1@*/
/*@requires maxSet(s1) >= maxRead(s2) @*/
/*@ensures maxRead(s1) == maxRead (s2) @*/;

requires句は s1として渡されたバッファーはs2として渡された文字列を保持するのに十分な長さである必要があることを示します。 ensures句は呼出し後のs1の maxReadがs2の maxReadと等しいことを指定します。 s2のサイズが不明である場合は、プログラムは以下のようにアノテーション付けられた strncpyを使用すべきです。

void /*@alt char * @*/ strncpy

(/*@unique@*/ /*@out@*/ /*@returned@*/ char *s1, char *s2,

size_t n)

/*@modifies *s1@*/
/*@requires maxSet(s1) >= ( n - 1 ); @*/
/*@ensures maxRead (s2) >= maxRead(s1) /\ maxRead (s1) <= n;@*/;

バッファーサイズの制約句に対する構文は次の通りです。

constraint ⇒ (requires | ensures) consExpr relOp consExpr
relOp ⇒ == | > | >= | < | <=
consExpr ⇒ consExpression binOp consExpr | unaryOp (consExpr ) | term
binOp ⇒ + | -
unaryOp ⇒ maxSet | maxRead
term ⇒ identifier | literal | result

9.3 Less Stringent Checking（厳しさを減らしたチェック）

いくつかのプログラムに対して、Splintの標準の境界チェックは容認できないほどの多くの警告を生成します。このため、Splintは現在、単純な発見的方法を使用して警告を優先順位付けします。フラグ、likely-bounds、likely-bounds-writes、と、 likely-bounds-readは、 bounds、bounds-write、と、 bounds-readに似ていますが、それらのみ、Splintがそれが決定するものに対しての警告が境界エラーの可能性を生じさせる原因となります。 5 >= 10のような数値矛盾へ制約を減らすことが可能な場合、Splintは境界エラーの可能性として未解決の制約を分類します。これらの制約に対する警告が正当である可能性が高い -- 本当のバグあるいはアノテーションの不足を示しています。さらに、これらの警告が偽陽性の場合、それらを擬似であるとして認識しやすくなります。これらのフラグは有意に少なかったエラー（いくつかのケースでは大きさの順）を生成し、そして、生成されたエラーは理解しやすいものです。しかし、これはコスト無しではできません。チェックが大幅に少なく正確であり、実際のエラーを見逃す可能性があります。

9.4 Warnings（警告）

境界チェックはSplintにより行われた他のチェックよりも複雑なため、メモリ境界の警告は未解決の制約についての広範な情報を含みます。未解決の制約に対する警告メッセージは元の制約と解決できない制約の簡略された形式の両方を含みます。制約が関数の前提条件から派生された場合、元の前提条件はエラーメッセージに含まれています。 +showconstraintlocationフラグが設定されている場合、メッセージは制約が派生する表現を含みます。+showconstraintparensフラグはあいまいさを排除するため、Splintに警告の中で完全に括弧でくくられた制約を表示するよう指示します。

自明な境界外への書き込みを含んでいる以下のコードの抜粋を考えてみましょう：

int buf[10];
buf[10] = 3;

Splintは以下のように警告します：

setChar.c:5:4: Likely out-of-bounds store:

buf[10] = 3
Unable to resolve constraint: requires 9 >= 10
needed to satisfy precondition: requires maxSet(buf @ setChar.c:5:4) >= 10

9（安全に書き込みできるbufの最大インデックス番号）は10以上ではないため、 Splintは既知のmaxSet(buf)の値の代わりにすることによって 9 >= 10へのrequires句から制約を簡略化し、警告を生成しました。

より実際の例が図21に示さされています。関数updateEnvは環境変数をコピーする関数の単純な実装です。 getenvの戻り値の長さでの標準的な制約がありません、なので、これはバッファーオーバーフローを起こす可能性があります。 updateEnvの安全なバージョン（図21のupdateEnvSafeのような）は、コピー前にバッファーが環境変数の文字列を保持するための十分な長さがあることを保障します。

requires句は、 updateEnvSafeの呼び出しが strSize文字として渡された値を保持するのに十分な大きさではないstrとしてバッファーを渡したときに、 Splintが警告を報告することを意味します。

多くの場合、関数は類似している複数の未解決の制約を持ちます。例えば、続いて起こる文がバッファーの次の要素に書き込む場合です。通常、全てのこれらの制約は全て実際の問題を意味するか、全てまがい（偽）です。 +redundantconstraintsフラグが設定されている場合、 Splintは明白に余分な警告メッセージでさえも報告します。そうではなくても、もし、1つの未解決の制約を満足させることがもう一方を満足させることを含むであろう場合、Splintは強い制約に対する警告メッセージを出力のみします。

bounds.c

Running Splint

void updateEnv(char * str) {    char * tmp; 7   tmp = getenv("MYENV");    if (tmp != NULL) 9      strcpy (str, tmp); }   void updateEnvSafe (char * str,                 size_t strSize)   /*@requires maxSet(str)               >= strSize - 1@*/ {    char * tmp;    tmp = getenv("MYENV");    if (tmp != NULL)    {       strncpy (str, tmp,                strSize -1);       str[strSize -1] = ‘/0’;    } }

> splint bounds.c +bounds +showconstraintlocation   bounds.c:9: Possible out-of-bounds store:     strcpy(str, tmp)     Unable to resolve constraint:     requires maxSet(str @ bounds.c:9) >=     maxRead(getenv("MYENV") @ bounds.c:7)      needed to satisfy precondition:     requires maxSet(str @ bounds.c:9) >=     maxRead(tmp @ bounds.c:9)      derived from strcpy precondition: requires     maxSet(<parameter 1>) >=     maxRead(<parameter 2>)

図 21. メモリ境界

配列の境界の警告が偽のものであるかを決定するために、 +functionpostフラグが有効です。もし、このフラグが設定されている場合、Splintは関数の終わりで確立した制約を出力します。もし、警告が偽のものである場合、限定された制御コメントはそれらを抑制するために使用することができます。

このドキュメントはSplint(英)のサイトを元に作成しました

Up: マニュアル

Prev: 8 Control Flow（制御フロー）

Next: 10 Extensible Checking（拡張可能なチェック）