More Web Proxy on the site http://driver.im/

article

Thorough static analysis of device drivers

Authors:

Ella Bounimova,

Vladimir Levin,

Jakob Lichtenberg,

Bohus Ondrusek,

Sriram K. Rajamani,

Abdullah UstunerAuthors Info & Claims

ACM SIGOPS Operating Systems Review, Volume 40, Issue 4

Pages 73 - 85

https://doi.org/10.1145/1218063.1217943

Published: 18 April 2006 Publication History

Abstract

Bugs in kernel-level device drivers cause 85% of the system crashes in the Windows XP operating system [44]. One of the sources of these errors is the complexity of the Windows driver API itself: programmers must master a complex set of rules about how to use the driver API in order to create drivers that are good clients of the kernel. We have built a static analysis engine that finds API usage errors in C programs. The Static Driver Verifier tool (SDV) uses this engine to find kernel API usage errors in a driver. SDV includes models of the OS and the environment of the device driver, and over sixty API usage rules. SDV is intended to be used by driver developers "out of the box." Thus, it has stringent requirements: (1) complete automation with no input from the user; (2) a low rate of false errors. We discuss the techniques used in SDV to meet these requirements, and empirical results from running SDV on over one hundred Windows device drivers.

References

[1]

T. Ball, B. Cook, S. Das, and S. K. Rajamani. Refining approximations in software predicate abstraction. In TACAS 04: Tools and Algorithms for the Construction and Analysis of Systems, pages 388--403, 2004.

[2]

T. Ball, B. Cook, S. K. Lahiri, and L. Zhang. Zapato: Automatic theorem proving for predicate abstraction refinement. In CAV 04: Computer-Aided Verification, pages 457--461, 2004.

[3]

T. Ball, R. Majumdar, T. Millstein, and S. K. Rajamani. Automatic predicate abstraction of C programs. In PLDI 01: Programming Language Design and Implementation, pages 203--213, 2001.

Digital Library

[4]

T. Ball, M. Naik, and S. K. Rajamani. From symptom to cause: Localizing errors in counterexample traces. In POPL 03: Principles of programming languages, pages 97--105, 2003.

Digital Library

[5]

T. Ball, A. Podelski, and S. K. Rajamani. Boolean and cartesian abstractions for model checking C programs. In TACAS 01: Tools and Algorithms for Construction and Analysis of Systems, pages 268--283, 2001.

Digital Library

[6]

T. Ball, A. Podelski, and S. K. Rajamani. On the relative completeness of abstraction refinement. In TACAS 02: Tools and Algorithms for Construction and Analysis of Systems, pages 158--172, April 2002.

Digital Library

[7]

T. Ball and S. K. Rajamani. Bebop: A symbolic model checker for Boolean programs. In SPIN 00: SPIN Workshop, pages 113--130, 2000.

Digital Library

[8]

T. Ball and S. K. Rajamani. Automatically validating temporal safety properties of interfaces. In SPIN 01: SPIN Workshop, pages 103--122, 2001.

Digital Library

[9]

T. Ball and S. K. Rajamani. Bebop: A path-sensitive interprocedural dataflow engine. In PASTE 01: Workshop on Program Analysis for Software Tools and Engineering, pages 97--103, 2001.

Digital Library

[10]

A. Bradley, Z. Manna, and H. Sipma. Linear ranking with reachability. In CAV 05: Computer-Aided Verification, pages 491--504, 2005.

Digital Library

[11]

R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677--691, 1986.

Digital Library

[12]

W. R. Bush, J. D. Pincus, and D. J. Sielaff. A static analyzer for finding dynamic programming errors. Software-Practice and Experience, 30(7):775--802, June 2000.

Digital Library

[13]

S. Chaki, E. Clarke, A. Groce, S. Jha, and H. Veith. Modular verification of software components in c. In ICSE 03: International Conference on Software Engineering, pages 385--395, 2003.

Digital Library

[14]

H. Chen, D. Dean, and D. Wagner. Model checking one million lines of c code. In NDSS 04: Network and Distributed System Security Symposium, 2004.

[15]

A. Chou, J. Yang, B. Chelf, S. Hallem, and D. Engler. An empirical study of operating systems errors. In SOSP 01: Symposium on Operating System Principles, pages 73--88, 2001.

Digital Library

[16]

E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In CAV 00: Computer Aided Verification, pages 154--169, 2000.

Digital Library

[17]

E. Clarke, D. Kroening, N. Sharygina, and K. Yorav. Predicate abstraction of ANSI-C programs using SAT. Formal Methods in System Design (FMSD), 25:105--127, September-November 2004.

Digital Library

[18]

B. Cook and G. Gonthier. Using Stalmårck's algorithm to prove inequalities. In ICFEM 05: Conference on Formal Engineering Methods, pages 330--344, 2005.

Digital Library

[19]

B. Cook, D. Kroening, and N. Sharygina. Cogent: Accurate theorem proving for program verification. In CAV 05: Computer-Aided Verification, pages 296--300, 2005.

Digital Library

[20]

B. Cook, D. Kroening, and N. Sharygina. Symbolic model checking for asynchronous boolean programs. In SPIN 01: SPIN Workshop, pages 75--90, 2005.

Digital Library

[21]

B. Cook, A. Podelski, and A. Rybalchenko. Abstraction refinement for termination. In SAS 05: Static Analysis Symposium, pages 87--101, 2005.

Digital Library

[22]

B. Cook, A. Podelski, and A. Rybalchenko. Termination proofs for systems code. In PLDI 06: Programming Language Design and Implementation, 2006.

Digital Library

[23]

P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for the static analysis of programs by construction or approximation of fixpoints. In POPL 77: Principles of Programming Languages, pages 238--252, 1977.

Digital Library

[24]

P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, and X. Rival. The ASTREÉ analyzer. In ESOP 05: European Symposium on Programming, pages 21--30, 2005.

Digital Library

[25]

M. Das. Unification-based pointer analysis with directional assignments. In PLDI 00: Programming Language Design and Implementation, pages 35--46, 2000.

Digital Library

[26]

M. Das, S. Lerner, and M. Seigle. ESP: Path-sensitive program verification in polynomial time. In PLDI 02: Programming Language Design and Implementation, pages 57--68, June 2002.

Digital Library

[27]

R. DeLine and M. Fähndrich. Enforcing high-level protocols in low-level software. In PLDI 01: Programming Language Design and Implementation, pages 59--69, 2001.

Digital Library

[28]

D. Detlefs, G. Nelson, and J. B. Saxe. Simplify: A theorem prover for program checking. Technical Report HPL-2003-148, HP Labs, 2003.

[29]

D. Engler, B. Chelf, A. Chou, and S. Hallem. Checking system rules using system-specific, programmer-written compiler extensions. In OSDI 00: Operating System Design and Implementation, pages 1--16. Usenix Association, 2000.

Digital Library

[30]

G. Balakrishnan et al. Model checking x86 executables with CodeSurfer/x86 and WPDS++. In CAV 05: Computer-Aided Verification, 2005.

Digital Library

[31]

C. Flanagan, K. R. M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe, and R. Stata. Extended static checking for java. In PLDI 02: Programming Language Design and Implementation", pages 234--245, 2002.

Digital Library

[32]

K. Fraser, S. Hand, R. Neugebauer, I. Pratt, A. Warfield, and M. Williams. Safe hardware access with the Xen virtual machine monitor. In OASIS'04: Workshop on Operating System and Architectural Support for the on demand IT InfraStructure, June 2004.

[33]

S. Hallem, B. Chelf, Y. Xie, and D. Engler. A system and language for building system-specific, static analyses. In PLDI 02: Programming Language Design and Implementation, pages 69--82, 2002.

Digital Library

[34]

T. A. Henzinger, R. Jhala, R. Majumdar, and K. L. McMillan. Abstractions from proofs. In POPL 04: Principles of Programming Languages, pages 232--244, 2004.

Digital Library

[35]

T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In POPL 02: Principles of Programming Languages, pages 58--70, January 2002.

Digital Library

[36]

R. P. Kurshan. Computer-aided Verification of Coordinating Processes. Princeton University Press, 1994.

Digital Library

[37]

S. Lahiri, T. Ball, and B. Cook. Predicate abstraction via symbolic decision procedures. In CAV 05: Computer-Aided Verification, pages 24--38, 2005.

Digital Library

[38]

L. Lamport. Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering, SE-3(2): 125--143, 1977.

Digital Library

[39]

J. R. Larus, T. Ball, M. Das, Rob DeLine, M. Fähndrich, J. Pincus, S. K. Rajamani, and R. Venkatapathy. Righting software. IEEE Software, 21(3):92--100, May/June 2004.

Digital Library

[40]

K. R. M. Leino and G. Nelson. An extended static checker for Modula-3. In CC 98: Compiler Construction, pages 302--305, 1998.

Digital Library

[41]

G. Necula, S. McPeak, and W. Weimer. CCured: Type-safe retrofitting of legacy code. In POPL 02: Principles of Programming Languages, pages 128--139, January 2002.

Digital Library

[42]

S. Qadeer and D. Wu. KISS: keep it simple and sequential. In PLDI 04: Programming Language Design and Implementation, pages 14--24, 2004.

Digital Library

[43]

F. B. Schneider. Enforceable security policies. ACM Transactions on Information and System Security, 3(1):30--50, February 2000.

Digital Library

[44]

M. M. Swift, B. N. Bershad, and H. M. Levy. Improving the reliability of commodity operating systems. In SOSP 03: Symposium on Operating System Principles, pages 207--222, June 2003.

Digital Library

[45]

M. Y. Vardi and P. Wolper. An automata theoretic apporach to automatic program verification. In LICS 86: Logic in Computer Science, pages 332--344. IEEE Computer Society Press, 1996.

Cited By

Meng RDuck GRoychoudhury ALuo BLiao XXu JKirda ELie D(2024)Program Environment FuzzingProceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security10.1145/3658644.3690229(720-734)Online publication date: 2-Dec-2024
https://dl.acm.org/doi/10.1145/3658644.3690229
Ferles KStephens JDillig I(2021)Verifying correct usage of context-free API protocolsProceedings of the ACM on Programming Languages10.1145/34342985:POPL(1-30)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434298
Li ZMachiry AChen BNaik MWang KSong L(2021)ARBITRAR: User-Guided API Misuse Detection2021 IEEE Symposium on Security and Privacy (SP)10.1109/SP40001.2021.00090(1400-1415)Online publication date: May-2021
https://doi.org/10.1109/SP40001.2021.00090
Show More Cited By

Index Terms

Thorough static analysis of device drivers

Recommendations

Thorough static analysis of device drivers
EuroSys '06: Proceedings of the 1st ACM SIGOPS/EuroSys European Conference on Computer Systems 2006

Bugs in kernel-level device drivers cause 85% of the system crashes in the Windows XP operating system [44]. One of the sources of these errors is the complexity of the Windows driver API itself: programmers must master a complex set of rules about how ...
Proving that programs eventually do something good
POPL '07: Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

In recent years we have seen great progress made in the area of automatic source-level static analysis tools. However, most of today's program verification tools are limited to properties that guarantee the absence of bad events (safety properties). ...
Static analysis of device drivers: we can do better!
APSys '11: Proceedings of the Second Asia-Pacific Workshop on Systems

We argue that the device driver architecture enforced by current operating systems complicates both manual and automatic reasoning about driver behaviour. In particular, it makes it hard and in some cases impossible to statically verify that the driver ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGOPS Operating Systems Review

ACM SIGOPS Operating Systems Review Volume 40, Issue 4

Proceedings of the 2006 EuroSys conference

October 2006

383 pages

ISSN:0163-5980

DOI:10.1145/1218063

Issue’s Table of Contents

EuroSys '06: Proceedings of the 1st ACM SIGOPS/EuroSys European Conference on Computer Systems 2006
April 2006
420 pages
ISBN:1595933220
DOI:10.1145/1217935
Conference Chair:
Yolande Berbers
K. U. Leuven, Belgium
,
Program Chair:
Willy Zwaenepoel
EPFL

Copyright © 2006 Authors.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 18 April 2006

Published in SIGOPS Volume 40, Issue 4

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

326
Total Citations
View Citations
2,008
Total Downloads

Downloads (Last 12 months)57
Downloads (Last 6 weeks)8

Reflects downloads up to 29 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Meng RDuck GRoychoudhury ALuo BLiao XXu JKirda ELie D(2024)Program Environment FuzzingProceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security10.1145/3658644.3690229(720-734)Online publication date: 2-Dec-2024
https://dl.acm.org/doi/10.1145/3658644.3690229
Ferles KStephens JDillig I(2021)Verifying correct usage of context-free API protocolsProceedings of the ACM on Programming Languages10.1145/34342985:POPL(1-30)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434298
Li ZMachiry AChen BNaik MWang KSong L(2021)ARBITRAR: User-Guided API Misuse Detection2021 IEEE Symposium on Security and Privacy (SP)10.1109/SP40001.2021.00090(1400-1415)Online publication date: May-2021
https://doi.org/10.1109/SP40001.2021.00090
Ali SSun HZhao Y(2021)Model learning: a survey of foundations, tools and applicationsFrontiers of Computer Science: Selected Publications from Chinese Universities10.1007/s11704-019-9212-z15:5Online publication date: 1-Oct-2021
https://dl.acm.org/doi/10.1007/s11704-019-9212-z
Bai XXing LZheng MQu FLigatti JOu XKatz JVigna G(2020)iDEA: Static Analysis on the Security of Apple Kernel DriversProceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security10.1145/3372297.3423357(1185-1202)Online publication date: 30-Oct-2020
https://dl.acm.org/doi/10.1145/3372297.3423357
Sachidananda VBhairav SElovici YHung CCerny TShin DBechini A(2020)OVERProceedings of the 35th Annual ACM Symposium on Applied Computing10.1145/3341105.3373930(729-738)Online publication date: 30-Mar-2020
https://dl.acm.org/doi/10.1145/3341105.3373930
Feng HGrundy JLe Goues CLo D(2020)A program verification based approach to find data race vulnerabilities in interrupt-driven programProceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering10.1145/3324884.3418925(1361-1363)Online publication date: 21-Dec-2020
https://dl.acm.org/doi/10.1145/3324884.3418925
Feng HYin LLin WZhao XDong W(2020)Rchecker: A CBMC-based Data Race Detector for Interrupt-driven Programs2020 IEEE 20th International Conference on Software Quality, Reliability and Security Companion (QRS-C)10.1109/QRS-C51114.2020.00084(465-471)Online publication date: Dec-2020
https://doi.org/10.1109/QRS-C51114.2020.00084
Lee SHong SYi JKim TKim CYoo S(2019)Classifying False Positive Static Checker Alarms in Continuous Integration Using Convolutional Neural Networks2019 12th IEEE Conference on Software Testing, Validation and Verification (ICST)10.1109/ICST.2019.00048(391-401)Online publication date: Apr-2019
https://doi.org/10.1109/ICST.2019.00048
Ali SSun HZhao YAkram N(2019)Testing-based Model Learning Approach for Legacy Components2019 16th International Bhurban Conference on Applied Sciences and Technology (IBCAST)10.1109/IBCAST.2019.8667149(597-603)Online publication date: Jan-2019
https://doi.org/10.1109/IBCAST.2019.8667149
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Issue’s Table of Contents