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).


Source Code Model Check Abstract Interpretation Device Driver Exit Node 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
  2. 2.
    Defrauding the WHQL driver certification process, March (2004),
  3. 3.
    C++ for kernel mode drivers: Pros and cons, WHDC web site (February 2007),
  4. 4.
    Balakrishnan, G.: WYSINWYX: What You See Is Not What You eXecute. PhD thesis, C.S. Dept. Univ. of Wisconsin, Madison, WI, August, TR-1603 (2007)Google Scholar
  5. 5.
    Balakrishnan, G., Reps, T.: Analyzing memory accesses in x86 executables. In: Duesterwald, E. (ed.) CC 2004. LNCS, vol. 2985, pp. 5–23. Springer, Heidelberg (2004)Google Scholar
  6. 6.
    Reps, T., Balakrishnan, G.: DIVINE: DIscovering Variables IN Executables. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 1–28. Springer, Heidelberg (2007)Google Scholar
  7. 7.
    Reps, T., Melski, D., Lal, A.K., Teitelbaum, T., Balakrishnan, G., Gruian, R., Kidd, N., Lim, J., Yong, S., Chen, C.-H.: Model checking x86 executables with CodeSurfer/x86 and WPDS++. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 158–163. Springer, Heidelberg (2005)Google Scholar
  8. 8.
    Balakrishnan, G., Reps, T., Melski, D., Teitelbaum, T.: WYSINWYX: What You See Is Not What You eXecute. In: IFIP Working Conf. on VSTTE (2005)Google Scholar
  9. 9.
    Ball, T.: Personal communication (February 2006)Google Scholar
  10. 10.
    Ball, T., Bounimova, E., Cook, B., Levin, V., Lichtenberg, J., McGarvey, C., Ondrusek, B., Rajamani, S.K., Ustuner, A.: Thorough static analysis of device drivers. In: EuroSys. (2006)Google Scholar
  11. 11.
    Ball, T., Rajamani, S.K.: Bebop: A symbolic model checker for Boolean programs. In: Spin Workshop (2000)Google Scholar
  12. 12.
    Rajamani, S.K., Ball, T.: The SLAM Toolkit. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, Springer, Heidelberg (2001)Google Scholar
  13. 13.
    Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: PLDI (2003)Google Scholar
  14. 14.
    Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Application to model checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, Springer, Heidelberg (1997)Google Scholar
  15. 15.
    Chou, A., Yang, J., Chelf, B., Hallem, S., Engler, D.: An empirical study of operating systems errors. In: SOSP (2001)Google Scholar
  16. 16.
    Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL (1979)Google Scholar
  17. 17.
    Das, M., Lerner, S., Seigle, M.: ESP: Path-sensitive program verification in polynomial time. In: PLDI (2002)Google Scholar
  18. 18.
    Das, M., Yang, Y., Dhurjati, D.: Path-Sensitive Dataflow Analysis with Iterative Refinement. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 425–442. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  19. 19.
    Finkel, A., Willems, B., Wolper, P.: A direct symbolic approach to model checking pushdown systems. Elec. Notes in Theor. Comp. Sci. 9 (1997)Google Scholar
  20. 20.
    Fischer, J., Jhala, R., Majumdar, R.: Joining dataflow with predicates. In: Gilbert, H., Handschuh, H. (eds.) FSE 2005. LNCS, vol. 3557, Springer, Heidelberg (2005)Google Scholar
  21. 21.
    Graf, S., Saïdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, Springer, Heidelberg (1997)Google Scholar
  22. 22.
    Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL (2002)Google Scholar
  23. 23.
    Holley, L.H., Rosen, B.K.: Qualified data flow problems. TSE 7(1), 60–78 (1981)MathSciNetGoogle Scholar
  24. 24.
  25. 25.
    Knoop, J., Steffen, B.: The interprocedural coincidence theorem. In: Pfahler, P., Kastens, U. (eds.) CC 1992. LNCS, vol. 641, Springer, Heidelberg (1992)Google Scholar
  26. 26.
    Mauborgne, L., Rival, X.: Trace Partitioning in Abstract Interpretation Based Static Analyzers. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 5–20. Springer, Heidelberg (2005)Google Scholar
  27. 27.
    Oney, W.: Programming the Microsoft Windows Driver Model. In: Microsoft (2003)Google Scholar
  28. 28.
    Ramalingam, G., Field, J., Tip, F.: Aggregate structure identification and its application to program analysis. In: POPL (1999)Google Scholar
  29. 29.
    Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. In: Program Flow Analysis: Theory and Applications, Prentice-Hall, Englewood Cliffs (1981)Google Scholar
  30. 30.
    Swift, M.M., Annamalai, M., Bershad, B.N., Levy, H.M.: Recovering device drivers. In: OSDI (2004)Google Scholar
  31. 31.
    Swift, M.M., Bershad, B.N., Levy, H.M.: Improving the reliability of commodity operating systems. ACM Trans. Comput. Syst. 23(1) (2005)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Gogul Balakrishnan
    • 1
  • Thomas Reps
    • 2
    • 3
  1. 1.NEC Laboratories America, Inc. 
  2. 2.University of Wisconsin 
  3. 3.GrammaTech, Inc. 

Personalised recommendations