静的ドライバー検証ツールの一般的なツールと技術的な制限

[アーティクル]
04/01/2024

SDV には、次の一般的な制限があります。

SDV は一度に 1 つのドライバーのみを検証し、完全に検証するには、ドライバーが WDM、KMDF、NDIS、Storport のドライバーモデルのいずれかに従っている必要があります。サポートされているドライバーの詳細については、「ドライバーまたはライブラリが静的ドライバー検証ツールでサポートされているかどうかの判定」を参照してください。
上記のカテゴリに該当しないドライバーは、検証可能なルールが厳しく制限され、分析中にエラーが発生する可能性が高くなります。
ドライバープロジェクトファイルとソースコードは、ローカルコンピューターに存在する必要があります。ドライバーをリモートで確認することはできません。
SDV では、ロケールは英語 (米国) でインストールされます。その結果、文字列の書式設定などのロケールに依存する要素は、英語 (米国) のバリアントを使用します。この制限は、英語 (米国) 以外でローカライズされたバージョンの Windows に SDV がインストールした場合でも発生します。

SDV 検証エンジンには技術的な制限があり、一部のドライバーコードを正常に解釈できません。具体的には、検証エンジンでは次のようになります。

32 ビット整数が 32 ビットに制限されていることを認識しません。そのため、オーバーフローエラーやアンダーフローエラーは検出されません。
static キーワードでエントリポイントを宣言したドライバーが正しく処理されていることを確認します。ただし、静的エントリポイントが確実に認識されるようにするため、SDV では静的関数の Sdv-map.h ファイルを変更する必要があります。たとえば、静的エントリポイントを宣言する場合は、次のようになります。
```
static DRIVER_UNLOAD Unload;
```
Sdv-map.h には、通常の fun_DriverUnload エントリは含まれません。
```
#define fun_DriverUnload Unload
```
代わりに、関数名が変更されているのがわかります。
```
  #define fun_DriverUnload sdv_static_function_Unload_1
```
これは、複数のモジュールに Unload という名前の静的関数がある場合に必要です。衝突の可能性を避けるため、名前は変更されています。
エクスポートドライバーに、ドライバーディスパッチ関数を非表示にするモジュール定義ファイル (.def) がある場合、エクスポートドライバーで定義されているドライバーディスパッチまたはドライバーコールバック関数を解釈できません。この問題を回避するには、モジュール定義ファイル (.def) の [エクスポート] セクションにドライバーディスパッチ関数を追加します。
この関数への次の参照が同じ コンパイル単位にない場合、関数のロール型を正常に検出できません。
- 関数の宣言。
- 関数の定義。
- ドライバーのエントリポイントまたはコールバック関数への関数の割り当て。
コンパイル単位とは、ソースコードファイルと、このソースコードファイルに含まれる他のソースファイルの最小セットと定義されています。

関数のロール型が SDV で検出されない場合、SDV は、この関数から発生したトレースを検証しません。

たとえば、ドライバーが mydriver.c ファイルで EvtDriverDeviceAdd 関数を定義 (または実装) しているとします。このコンパイル単位 (または mydriver.c が含まれる .h ファイル) には、EvtDriverDeviceAdd 関数のロール型宣言が含まれている必要があります。
構造化例外処理は解釈されません。 try/except 文の場合、SDV は例外がスローされなかったものとして、保護されたセクションを分析します。式や例外ハンドラーコードは分析しません。
```
// The try/except statement
__try 
{
   // guarded section
}
__except ( expression )
{
   // exception handler
} 
```
try/finally 文の場合、SDV は例外がスローされなかったものとして、保護されたセクションと終了ハンドラーを分析します。
```
// The try/finally statement
__try {
   // guarded section
}
__finally {
   // termination handler
}
```
try/except 文と try/finally 文の場合、SDV は、leave 文を無視します。

try/except 文と try/finally 文の場合、try ブロックからのジャンプは except 文や finally 文の分析を妨げます。 leave 文が使用できるように書き換える方法については、コンパイラ警告「C6242」のトピックを参照してください。
ポインター演算を無視します。たとえば、ポインターの増分や減少の状況を見落とされます。この制限により、偽陰性や偽陽性の結果が生じる可能性があります。
結合を無視します。ほとんどの場合、結合は 構造体 として扱われ、擬陽性や偽陰性が発生する可能性があります。
キャスト操作を無視するため、再キャストによって解決されたエラーとキャストによって発生するエラーの両方が見落とされます。たとえば、エンジンは、文字として再キャストされた整数の整数値が引き続き存在することを前提としています。
関数ポインター配列である配列のみを初期化します。 SDV は警告し、配列の初期化子を最初の 1000 の要素に圧縮します。他の配列型の場合、最初の要素のみが初期化されます。
配列で初期化されるオブジェクトのコンストラクターは呼び出されません。たとえば、次のコードスニペットでは、SDV がコンストラクターを呼び出していないため、x は 10 に設定されません。
```
class A
{
public:
    A() {
      x = 10;
    }

    int x;
};

void main()
{
    A a[1];
}
```
SDV は、コンストラクターを使用して配列を初期化することはサポートしていません。たとえば、次のコードスニペットでは、P のコンストラクターはメイン関数で正しく呼び出されず、配列 p2 の要素は初期化されません。
```
class P
{
public:
    P() : x(0) {}
    int x;
};

void main()
{
    P* p1 = new P[1];

    P p2[1] = {P()};
}
```
SDV はプリコンパイル済みのヘッダーを無視します。コンパイル速度を上げるためだけにプリコンパイル済みヘッダーを使用するドライバーは、SDV を使用するとコンパイル速度が遅くなります。コンパイルを成功させるためにプリコンパイル済みヘッダーを使用する必要があるドライバーは、SDV ではコンパイルされません。
RtlZeroMemory または NdisZeroMemory の呼び出しによって行われる一部の型の暗黙的な割り当てを推論できません。エンジンは、メモリをゼロに初期化するためのベストエフォート分析を実行しますが、その型を判別できる場合にのみ実行されます。その結果、メモリを初期化するためにこれらの関数に依存するコードでは、一部のコードパスで疑似欠陥が発生する可能性があります。
KMDF ドライバーへの I/O 要求の手動ディスパッチを追跡できるようにするメモリモデルはサポートされていません。エンジンは、I/O リクエストをドライバーに配信するフレームワークに依存するメソッドのみをサポートします (順次または並列ディスパッチの場合)。
比較に float データ型を使用することはできません。この技術的な制限により、偽陰性と偽陽性の結果が生じる可能性があります。
SDV は、仮想継承または仮想関数をサポートしていません。 SDV では、仮想関数を介してコードパスに従う欠陥は生成されないため、真欠陥が失われる可能性があります。仮想継承は通常の継承と同様に扱われ、疑似欠陥や真欠陥が失われる可能性があります。

Share via

静的ドライバー検証ツールの一般的なツールと技術的な制限

フィードバック

フィードバック

その他のリソース