sec10 - Splint翻訳 Wiki - Splint翻訳

Up: マニュアル

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

Next: 11 Macros（マクロ）

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

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

Splintはメタ状態定義を使用して新しいチェックとアノテーションを定義するためのメカニズムを提供します。ユーザ定義のチェックは、チェックするためと、提供されたチェックではサポートサポートされないプロパティをドキュメント化するために使用されます。 ^*13

便利なチェックの大きなクラスは、プログラムオブジェクトあるいはグローバル実行状態に関連付けられた属性に制約として記述されます。型とは異なり、しかし、これらの属性の値は実行パスに沿って変わります。 Splintは、両方がインタフェースの点で属性値を制約し、どの属性値を変更するかを指定するルールと同じようにプログラムオブジェクトの異なる種類に関連した属性をユーザが定義するのを許す一般的な言語を提供します。

ユーザ定義の属性のチェックは通常のチェックと統合されているため、Splintのユーザユーザ定義の属性の解析は、別名化やnullかどうかの解析などのような、他の解析を利用するかもしれません。

10.1 Defining Attributes（属性の定義）

属性を定義するためには、 使用可能な値と属性の遷移ルールを定義したメタ状態ファイル（.mts）を作成して下さい。 属性は、プログラムオブジェクト（例えば、全てのchar *のもの）の特定の種類、あるいは、 グローバル状態（ネットワークが初期化されているかどうか）に 関連付けられます。 -mts<file>フラグはSplintがメタ状態ファイル （デフォルトの拡張子.mtsを持つ、LARCH_PATHパス上で見つけられる ）を読むように指示するために使用されます。

属性定義の例を図22に示します。 char *が信頼できない可能性のあるソースから来ているかどうか を記録するためのtaintedness属性 を定義しています。 値が敵意のある可能性があるかどうかを知ることは、 書式文字列バグを含むいくつかのセキュリティ脆弱性を防ぐために役立ちます。 ^*14 (書式の脆弱性を検知するための簡単な方法は、コンパイル時には不明な どの書式文字列に対しても警告をすることです。 Splintは+formatconstフラグが設定されている場合に このチェックを行い、警告を出し、そして、コンパイル時に不明などんな書式文字列 も検索します。 これは、しかし、敵意のある入力に対して弱くはない不明な書式文字列があるかもしれない ため、誤ったメッセージを生成することがあります。)

属性定義の最初の3行は、char *オブジェクトに関連付けられたtaintedness属性を定義しています。 そして、これは、untainted あるいは tainted の2つの状態のどちらかになります。 context句はオブジェクトが属性を持っている コンテキストセレクター（context selector：文脈選択者）を与えます。 このケースでは、reference char *はchar *である全ての参照が関連付けられた taintedness 属性を持っていることを意味しています。 他のcontextはparameter（引数定義のみ） 、literal（文字列か数値のリテラルのみ） 、そして、null（既知のNULLのみ）を含みます。 属性は、どの特定のオブジェクトとも関連付かず、しかし、その代わりに プログラムの実行のグローバルな状態と関連付くようにも定義できます。 globalキーワードは、グローバル属性を定義するためにattributeの前に使用されます。

oneof句はtaintednessの 値に対応する2つの識別子（ 信頼できない入力から派生していない参照に対するuntaintedと、 敵意のあるデータを含む可能性のある参照に対するtainted ） を導入します。

annotations句は taintednessの仮定 を記述するために使用される可能性のある2つの新しいアノテーションを定義します。 このケースでは、アノテーションは値の選択肢の名前に一致しますが、 それらは、どんな識別子でもかまいません。 句tainted reference ==> taintedは、 tainted状態を持つ ことを示すための参照に使用される可能性のあるtaintedアノテーションを定義します。

attribute taintedness    context reference char *    oneof untainted, tainted    annotations      tainted reference ==> tainted      untainted reference ==> untainted    transfers      tainted as untainted ==> error "Possibly tainted storage used where untainted required."    merge       tainted + untainted ==> tainted    defaults       reference ==> tainted       literal ==> untainted       null ==> untainted end 図 22.  Taintedness属性

transfers句は、オブジェクトが 引数として渡されるか、戻されるか、外部から見える参照へ 割り当てられるときの状態遷移と警告に対するルールを定義します。 ルール、tainted as untainted ==> error "Possibly tainted storage used where untainted required."、は、 untaintedのtaintedness を持つ引数としてtainted値を渡すことは エラーであることを意味します。 他のすべての遷移は暗黙的に許可されており、遷移前と同じ 状態の記憶を残します。 参照が遷移後に状態に変わることを示すために transfers句を使用することも出来ます。 losereference句 （taintednessの中では使用されていない）は、 transfers句と似ていますが、 その代わり、宣言されたスコープを残すか 関数から戻るか、新しい値を割り当てるかによって、 記憶への参照がなくなったときに対するルールを提供するために 使用されることを除きます。

merge句は経路に沿った 状態を結合するためのルールを定義します。 句、merge tainted + untainted ==> tainted、は、 taintedと untaintedのオブジェクトを 結合させることはtaintedオブジェクトを作る ことを示しています。 従って、もし、参照が1制御経路に沿ったtaintedと もう１つの制御経路に沿ったuntaintedである場合、 チェックはそれが2つのブランチのマージ後にtaintedであると 想定します。 関数の仕様にtaintedness状態をマージするためにも使用されます （次のsectionのstrcatの例を参照）。 異なる経路上の状態が矛盾している場合、 警告が報告されるよう、エラーの組み合わせを定義することも出来ます。

defaults句は 明示的な属性アノテーションが無い宣言に対して使用されるデフォルト値 を指定します。 アノテーション付けされていないプログラムのチェックの開始を容易にするために デフォルト値を選択します。 ここでは、アノテーション付けされていない参照が taintedであるとし、 アノテーション付けされていない参照が untainted引数を要求する関数へ渡された場所をSplintが警告すると仮定します。 警告は、コード内の書式バグか、あるいは、 untainted アノテーションが追加されるべき場所を示します。 アノテーションを追加した後、再度Splintを実行すると、 プログラムを介してドキュメント化された仮定を新たに伝達させます。

メタ状態に対する完全な文法はAppendix Cに記載されています。

10.2 Annotations（アノテーション）

メタ状態の定義によって定義されたアノテーションは 通常のアノテーションと同様に使用可能です。 アノテーションに対するコンテキスト指定子は、 それが使用される可能性のある場所を示します。 taintednessの例では、onlyが使用できる場所ではどこでも、 アノテーションとしてtainted と untaintedが使用できます。 これはensures と requires 句（メタ状態定義にて関連付けられた状態を変更する関数を指定することが出来る）を含みます。 構文、<expr>:<attribute>、は 式、<expr>、 に対してのユーザ定義の属性の値を参照するために使用されます。

メタ状態のアノテーションによって ライブラリの使用を拡張する必要がしばしばあります。 異なるメタ状態のアノテーションに対してライブラリの異なるバージョンを 持ちたくないので、代わりに、Splintは.xhファイル を使用してアノテーションを別に追加するメカニズムを提供しています。 taintednessの例では、tainted.xhファイル の中でアノテーション付けした宣言を提供することでこれを行っています。 このファイルの例の仕様は次の通りです：

int printf (/*@untainted@*/ char *fmt, ...);

char *fgets (char *s, int n, FILE *stream) /*@ensures tainted s@*/ ;

char *strcat (/*@returned@*/ char *s1, char *s2)
　/*@ensures s1:taintedness = s1:taintedness | s2:taintedness @*/

strcatの仕様には、 strcatが戻った後の s1の taintednessが呼び出し前のs1 と s2 のtaintednessをマージした結果であることを示すために、 /*@ensures s1:taintedness = s1:taintedness | s2:taintedness @*/ が使用されています。 引数はアノテーションが欠落しているため、暗黙的にデフォルトルールに従って taintedになり、untaintedかtaintedのどちらかの参照が strcatへの引数として 渡されます。 ensures句は、 strcatが戻った後の 第一引数（と戻り値。なぜなら、s1にreturnedアノテーションがあるため） は渡されたオブジェクトどちらか一方でもtaintedのときにtaintedとなる ことを意味しています。 Splintは属性の定義ルールを使用して2つのtaintedness状態をマージします。 -- 従って、s1引数がuntaintedで、 かつ、s2引数がtaintedの場合、 strcatが戻った後の 戻り値と第一引数はtaintedになります。

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

Up: マニュアル

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

Next: 11 Macros（マクロ）