Partager via

Présentation du vérificateur de pilote statique

  • Article

Static Driver Verificationr (SDV) est un outil de vérification statique qui s’exécute au moment de la compilation. Il explore les chemins dans le code du pilote en exécutant symboliquement le code source, ce qui rend les hypothèses les plus rares possibles sur l’état du système d’exploitation et l’état initial du pilote. Par conséquent, SDV peut exercer du code dans des chemins qui sont manqués dans les tests traditionnels.

SDV inclut un ensemble de règles qui définissent une interaction appropriée entre un pilote et le noyau du système d’exploitation. Lors de la vérification, SDV examine chaque branche applicable du code de pilote et le code de bibliothèque qu’il utilise, et tente de prouver que le pilote enfreint les règles. Si SDV ne parvient pas à prouver une violation, il signale que le conducteur est conforme aux règles et passe la vérification.

Cette section inclut les éléments suivants :

Présentation du vérificateur de pilote statique

Concepts du vérificateur de pilote statique

Pilotes pris en charge

Limitations du vérificateur de pilotes statiques

Important

SDV n’est plus pris en charge et SDV n’est plus disponible dans les versions wdK ou EWDK de Windows 24H2. Il n’est pas disponible dans les kits WDK plus récents que la build 26017 et n’est pas inclus dans windows 24H2 RTM WDK. SDV peut toujours être utilisé en téléchargeant windows 11, version 22H2 EWDK (publiée le 24 octobre 2023) avec Visual Studio Build Tools 17.1.5 à partir du téléchargement du Kit de pilotes Windows (WDK). Seule l’utilisation du kit WDK Entreprise pour exécuter SDV est recommandée. L’utilisation de versions antérieures de WDK standard conjointement avec les versions récentes de Visual Studio n’est pas recommandée, car cela entraînera probablement des échecs d’analyse.
À l’avenir, CodeQL sera l’outil d’analyse statique principal pour les pilotes. CodeQL fournit un langage de requête puissant qui traite le code comme une base de données à interroger, ce qui facilite l’écriture de requêtes pour des comportements, des modèles spécifiques, etc. Pour plus d’informations sur l’utilisation de CodeQL, consultez CodeQL et le test du logo Static Tools.