静态驱动程序验证程序简介

静态驱动程序验证程序(SDV)是在编译时运行的静态验证工具。 它通过以符号方式执行源代码来探索驱动程序代码中的路径,从而尽可能少地假设操作系统的状态和驱动程序的初始状态。 因此,SDV 可以在传统测试中错过的路径中练习代码。

SDV 包含一组规则,用于定义驱动程序和操作系统内核之间的正确交互。 在验证期间,SDV 检查驱动程序代码的每个适用分支及其使用的库代码,并尝试证明驱动程序违反了规则。 如果 SDV 无法证明违规,则会报告驱动程序符合规则并通过验证。

本部分包括:

了解静态驱动程序验证程序

静态驱动程序验证程序概念

支持的驱动程序

静态驱动程序验证程序限制

重要

不再支持 SDV,并且 Windows 24H2 WDK 或 EWDK 版本中不提供 SDV。 它在版本 26017 之前的 WDK 中不可用,并且不包括在 Windows 24H2 RTM WDK 中。 通过从 下载 Windows 驱动程序工具包(WDK)下载 Windows 11 版本 22H2 EWDK(2023 年 10 月 24 日发布)和 Visual Studio 生成工具 17.1.5,仍可使用 SDV。 建议仅使用企业 WDK 运行 SDV。 不建议将旧版标准 WDK 与 Visual Studio 的最新版本结合使用,因为这可能会导致分析失败。
今后,CodeQL 将成为驱动程序的主要静态分析工具。 CodeQL 提供了一种功能强大的查询语言,可将代码视为要查询的数据库,使编写特定行为、模式等查询变得简单。 有关使用 CodeQL 的详细信息,请参阅 CodeQL 和静态工具徽标测试