This paper sketches the design and implementation of Device- Driver Analyzer for x86 (DDA/x86), a prototype analysis tool for finding bugs in stripped Windows device-driver executables (i.e., when neither source code nor symbol-table/debugging information is available), and presents a case study. DDA/x86 was able to find known bugs (previously discovered by source-code-based analysis tools) along with useful error traces, while having a reasonably low false-positive rate.

This work represents the first known application of automatic program verification/analysis to stripped industrial executables, and allows one to check that an executable does not violate known API usage rules (rather than simply trusting that the implementation is correct).