Static Driver
Giulia Satmary
Static Driver Verifier (also known as "StaticDV" or "SDV") is a static verification tool that systematically analyzes the source code of Windows kernel-mode drivers. SDV is a compile time tool that is capable of discovering defects and design issues in a driver. Based on a set of interface rules and a model of the operating system, SDV determines whether the driver correctly interacts with the Windows operating system kernel.
SDV is no longer supported and SDV is not available in Windows 24H2 WDK or EWDK releases. It is not available in WDKs newer than build 26017, and is not included in the Windows 24H2 RTM WDK.SDV can still be used by downloading the Windows 11, version 22H2 EWDK (released October 24, 2023) with Visual Studio build tools 17.1.5 from Download the Windows Driver Kit (WDK). Only the use of the Enterprise WDK to run SDV is recommended. Using older versions of the standard WDK in conjunction with recent releases of Visual Studio is not recommended, as this will likely result in analysis failures.
Going forward, CodeQL will be the primary static analysis tool for drivers. CodeQL provides a powerful query language that treats code as a database to be queried, making it simple to write queries for specific behaviors, patterns, and more.For more information about using CodeQL, see CodeQL and the Static Tools Logo Test.
Static Driver Verifier is available as part of the Windows Driver Kit (WDK) in both the full WDK experience and in the standalone Enterprise WDK. In addition, the Visual C++ Redistributable Packages for Visual Studio are required for SDV to run. See the following:
Static Driver Verifier is integrated into Visual Studio. You can run static analysis on your Visual Studio driver project. You can launch, configure, and control Static Driver Verifier from the Driver menu in Visual Studio.
Microsoft uses SDV to test the kernel-mode drivers that are included with the Microsoft Windows operating system and to test the sample drivers in the WDK. By using the DDI compliance rules for specific driver models, SDV can verify correct driver behavior. For example, SDV can verify that the driver:
Static Driver Verifier (SDV) is a static verification tool that runs at compile time. It explores paths in the driver code by symbolically executing the source code, making the fewest possible assumptions about the state of the operating system and the initial state of the driver. As a result, SDV can exercise code in paths that are missed in traditional testing.
SDV includes a set of rules that define proper interaction between a driver and the operating system kernel. During verification, SDV examines every applicable branch of the driver code and the library code that it uses, and tries to prove that the driver violates the rules. If SDV fails to prove a violation, it reports that the driver complies with the rules and passes the verification.
The build phase complains about failing even though I can build everything just fine either through the IDE or using MSBuild directly. The error messages are fairly opaque but dialing up the debug and looking at some logs has shown me the cause but not the solution.
If ebUniversalProForU3V is the project folder, where do you want the
binaries? The default project files will put the intermediate (.obj)
and final (.sys) files into:
ebUniversalProForU3V\Debug
ebUniversalProForU3V\Release
ebUniversalProForU3V\x64\Debug
ebUniversalProForU3V\x64\Release
Yeah. These are quasi generated files too. We build the drivers as part of a much larger cmake project and do some transforms on vcxproj templates to set them up relative to the source code in a throwaway build folder.
You can run Static Driver Verifier (SDV) in a Visual Studio Command Prompt window, either through installing the Windows Driver Kit (WDK) or by running the Enterprise Windows Driver Kit (EWDK). Navigate to the directory where the driver's project file or the library's project file is stored. The parameters can appear in any order on the command line.
Scans the driver's source code for function role type declarations. For information about how to declare the driver supplied callback functions and dispatch routines, see Using Function Role Type Declarations. During this scan, SDV tries to detect the driver entry points that it needs to verify the driver. It records the results of the scan in Sdv-map.h, a file that it creates in the driver's project directory.
Starts a verification with the specified rule(s). You can specify more than one rule by separating each rule with a comma. Run the /check: command and specify the driver's Visual Studio project file (*.vcxproj).
Starts a verification with the rules in the specified rule list file. You can list only one file with this parameter. In the rule list file, each line can be the name of one rule or it can be a wildcard character (*), which represents all SDV rules. Run /check:RuleList.sdv command and specify the driver's Visual Studio project file (*.vcxproj).
RuleList.sdv is the fully qualified path and file name of a rule list file. The file must have the .sdv file name extension. Unless the file is in the local directory, the path is required. If the path or file name includes spaces, you must enclose RuleList.sdv in quotation marks.
Processes the library in the current directory. SDV calls MSBuild.exe to compile and build the library for external use, and it generates the files that it needs to include the library in the driver verification.
Deletes SDV files from the directory. Because these files are used to generate the Static Driver Verifier Report display, the /clean command also deletes the report of the verification.
A /clean command deletes the files that SDV uses to create the Static Driver Verifier Report display for a verification. After running this command, the Static Driver Verifier Report display for the verification is no longer available.
Why is it that every function in most device drivers are static? As static functions are not visible outside of the file scope. Then, how do these driver function get called by user space applications?
Remember than in C everything is addresses. That means you can call a function if you have the address. The kernel has a macro named EXPORT_SYMBOL that does just that. It exports the address of a function so that driver functions can be called without having to place header declarations since those functions are sometimes not know at compile time. In cases like this the static qualifier is just made to ensure that they are only called through this method and not from other files that may include that driver code (in some cases it's not a good idea to include driver code headers and call them directly).
Driver functions are usually not called through userspace directly (except for x86 implementation of SYSCALL instruction which does some little tricks to save the context switch sometimes). So the static keyword here makes no difference. It only makes a difference in kernel space. As pointed out by @Cong Wang, functions are usually place into a structure of function pointers so that they may be called by simply having structures point to this structure (such as file_ops, schedulers, filesystems, network code, etc...).
Because these static function are not supposed to be used directly outside of the module. They are called by other functions in the module, among which can be the interface to an ioctl or whatever callbacks. This is why they can be called from user-space, they are just in the call path.
The kernel has thousands of modules and they are (or used to be) all object files, loaded dynamically via a process similar to linking --or are actually linked-- into the executable. Can you imagine how many name clashes there would be if they were all to export all their function names, as is the default C behavior unless static is specified?
64591212e2