静态驱动程序验证程序常规工具和技术限制

项目
06/15/2023

SDV 具有以下一般限制：

SDV 一次只验证一个驱动程序，驱动程序必须遵循以下驱动程序模型之一才能进行完全验证：WDM、KMDF、NDIS 或 Storport。有关支持的驱动程序的详细信息，请参阅确定静态驱动程序验证程序是否支持驱动程序或库。
不属于上述类别之一的驱动程序将在可验证的规则中受到严重限制，并且更有可能在分析过程中失败。
驱动程序项目文件和源代码必须驻留在本地计算机上。无法远程验证驱动程序。
SDV 随英语 (美国) 区域设置一起安装。因此，依赖区域设置的元素（如字符串格式）使用英语 (美国) 变体。即使 SDV 安装在非英语 (美国) 的本地化版本的 Windows 上，也存在此限制。

SDV 验证引擎存在技术限制，无法正确解释某些驱动程序代码。具体而言，验证引擎：

无法识别 32 位整数限制为 32 位。因此，它不会检测溢出或下溢错误。
确保正确处理使用静态关键字 (keyword) 声明其入口点的驱动程序。但是，为了确保识别静态入口点，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) 文件。若要避免此问题，请将驱动程序调度函数添加到 module-definition (.def) 文件的 EXPORTS 部分。
如果对此函数的以下引用不在同一 编译单元中，则无法成功检测函数的角色类型。
- 函数的声明。
- 函数的定义。
- 将函数分配给驱动程序入口点或回调函数。
编译单元在此处定义为此源代码文件包含的最小源代码文件和其他源文件集。

如果 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 个元素。对于其他数组类型，仅初始化第一个元素。
不会调用数组中初始化的对象的构造函数。例如，在以下代码片段中， x 未设置为 10，因为 SDV 不调用构造函数。
```
class A
{
public:
    A() {
      x = 10;
    }

    int x;
};

void main()
{
    A a[1];
}
```
SDV 不支持使用构造函数初始化数组。例如，在以下代码片段中，P 的构造函数将不会在 main 函数中正确调用，并且不会初始化数组 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 不会通过虚拟函数生成遵循代码路径的缺陷，这可能会导致丢失真正的缺陷。虚拟继承被视为常规继承，这可能会导致错误缺陷或丢失真实缺陷。

通过

静态驱动程序验证程序常规工具和技术限制

反馈

其他资源