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

静态驱动程序验证程序 (SDV) 是一种在编译时运行的静态验证工具。 它通过以符号方式执行源代码来探索驱动程序代码中的路径，对操作系统状态和驱动程序的初始状态做出尽可能少的假设。 因此，SDV 可以在传统测试中遗漏的路径中执行代码。

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

本节包括：

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

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

支持的驱动程序

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