research-article

Static analysis of device drivers: we can do better!

Authors:

Sidney Amani,

Leonid Ryzhyk,

Alastair F. Donaldson,

Gernot Heiser,

Alexander Legg,

Yanjin ZhuAuthors Info & Claims

APSys '11: Proceedings of the Second Asia-Pacific Workshop on Systems

Article No.: 8, Pages 1 - 5

https://doi.org/10.1145/2103799.2103809

Published: 11 July 2011 Publication History

Get Access

Abstract

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 correctly interacts with the rest of the kernel. This limitation cannot be addressed solely via better verification tools. We maintain that qualitative improvement in the effectiveness of static driver verification must rely on an improved driver architecture, leading to drivers that are easier to write, understand, and verify.

To support our claims, we present a device driver architecture, called active drivers, that satisfies these requirements. We outline our methodology for specifying and verifying active driver protocols using existing model checking tools and describe initial experimental results.

References

[1]

T. Ball, E. Bounimova, B. Cook, V. Levin, J. Lichtenberg, C. McGarvey, B. Ondrusek, S. K. Rajamani, and A. Ustuner. Thorough static analysis of device drivers. In 1st EuroSys Conf., pages 73--85, Leuven, Belgium, Apr 2006.

Digital Library

Google Scholar

[2]

F. Barnes and C. Ritson. Checking process-oriented operating system behaviour using CSP and refinement. Operat. Syst. Rev., 43(4):45--49, Oct 2009.

Digital Library

Google Scholar

[3]

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

Digital Library

Google Scholar

[4]

M. Fähndrich, M. Aiken, C. Hawblitzel, O. Hodson, G. C. Hunt, J. R. Larus, and S. Levi. Language support for fast and reliable message-based communication in Singularity OS. In 1st EuroSys Conf., pages 177--190, Leuven, Belgium, Apr 2006.

Digital Library

Google Scholar

[5]

A. Fehnker, R. Huuck, P. Jayet, M. Lussenburg, and F. Rauch. Goanna --- A Static Model Checker. In 11th FMICS, pages 297--300, Bonn, Germany, Aug 2006.

Digital Library

Google Scholar

[6]

D. Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8(3):231--274, Jun 1987.

Digital Library

Google Scholar

[7]

T. A. Henzinger, R. Jhala, R. Majumdar, G. C. Necula, G. Sutre, and W. Weimer. Temporal-safety proofs for systems code. In 14th Int. Conf. Comp. Aided Verification, pages 526--538, Copenhagen, Denmark, 2002.

Digital Library

Google Scholar

[8]

N. Palix, G. Thomas, S. Saha, C. Calvès, J. Lawall, and G. Muller. Faults in linux: ten years later. In 16th ASPLOS, pages 305--318, Newport Beach, CA, USA, 2011.

Digital Library

Google Scholar

[9]

L. Ryzhyk, P. Chubb, I. Kuz, and G. Heiser. Dingo: Taming device drivers. In 4th EuroSys Conf., Nuremberg, Germany, Apr 2009.

Digital Library

Google Scholar

[10]

L. Ryzhyk, Y. Zhu, and G. Heiser. The case for active device drivers. In 1st APSys, pages 25--30, New Delhi, India, Aug 2010.

Digital Library

Google Scholar

[11]

T. Witkowski, N. Blanc, D. Kroening, and G. Weissenbacher. Model checking concurrent Linux device drivers. In 22nd ASE, pages 501--504, Atlanta, Georgia, USA, 2007.

Digital Library

Google Scholar

Cited By

View all

Bai JWang YHu SKnoop JSchordan MJohnson TO'Boyle M(2018)AutoPA: automatically generating active driver from original passive driver codeProceedings of the 2018 International Symposium on Code Generation and Optimization10.1145/3168809(288-299)Online publication date: 24-Feb-2018
https://dl.acm.org/doi/10.1145/3168809
Misono MOgino MFukai TShinagawa T(2018)FaultVisor2: Testing Hypervisor Device Drivers Against Real Hardware Failures2018 IEEE International Conference on Cloud Computing Technology and Science (CloudCom)10.1109/CloudCom2018.2018.00048(204-211)Online publication date: Dec-2018
https://doi.org/10.1109/CloudCom2018.2018.00048
Jindal APathak AHu YMidkiff SHanzálek ZHärtig HCastro MKaashoek M(2013)HypnosProceedings of the 8th ACM European Conference on Computer Systems10.1145/2465351.2465377(253-266)Online publication date: 15-Apr-2013
https://dl.acm.org/doi/10.1145/2465351.2465377
Show More Cited By

Index Terms

Static analysis of device drivers: we can do better!
1. Software and its engineering
2. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning
      1. Program analysis
    2. Program semantics

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 ...
Thorough static analysis of device drivers
Proceedings of the 2006 EuroSys conference

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 ...
Understanding modern device drivers
ASPLOS XVII: Proceedings of the seventeenth international conference on Architectural Support for Programming Languages and Operating Systems

Device drivers are the single largest contributor to operating-system kernel code with over 5 million lines of code in the Linux kernel, and cause significant complexity, bugs and development costs. Recent years have seen a flurry of research aimed at ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

APSys '11: Proceedings of the Second Asia-Pacific Workshop on Systems

July 2011

97 pages

ISBN:9781450311793

DOI:10.1145/2103799

General Chairs:
Haibo Chen
Fudan University, China
,
Zheng Zhang
Microsoft Research Asia, China
,
Program Chairs:
Sue Moon
KAIST, Korea
,
Yuanyuan Zhou
University of California, San Diego, USA

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

In-Cooperation

SIGOPS: ACM Special Interest Group on Operating Systems

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 July 2011

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Research-article

Funding Sources

Engineering and Physical Sciences Research Council

Conference

APSys '11

Sponsor:

USENIX Assoc

APSys '11: Asia Pacific Workshop on Systems

July 11 - 12, 2011

Shanghai, China

Acceptance Rates

Overall Acceptance Rate 169 of 430 submissions, 39%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
167
Total Downloads

Downloads (Last 12 months)6
Downloads (Last 6 weeks)0

Reflects downloads up to 29 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Bai JWang YHu SKnoop JSchordan MJohnson TO'Boyle M(2018)AutoPA: automatically generating active driver from original passive driver codeProceedings of the 2018 International Symposium on Code Generation and Optimization10.1145/3168809(288-299)Online publication date: 24-Feb-2018
https://dl.acm.org/doi/10.1145/3168809
Misono MOgino MFukai TShinagawa T(2018)FaultVisor2: Testing Hypervisor Device Drivers Against Real Hardware Failures2018 IEEE International Conference on Cloud Computing Technology and Science (CloudCom)10.1109/CloudCom2018.2018.00048(204-211)Online publication date: Dec-2018
https://doi.org/10.1109/CloudCom2018.2018.00048
Jindal APathak AHu YMidkiff SHanzálek ZHärtig HCastro MKaashoek M(2013)HypnosProceedings of the 8th ACM European Conference on Computer Systems10.1145/2465351.2465377(253-266)Online publication date: 15-Apr-2013
https://dl.acm.org/doi/10.1145/2465351.2465377
Renzelmann MKadav ASwift MVahdat AThekkath C(2012)SymDriveProceedings of the 10th USENIX conference on Operating Systems Design and Implementation10.5555/2387880.2387908(279-292)Online publication date: 8-Oct-2012
https://dl.acm.org/doi/10.5555/2387880.2387908

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.

PDF

eReader

View online with eReader.

eReader

Abstract

References

Cited By

Index Terms

Recommendations

Thorough static analysis of device drivers

Thorough static analysis of device drivers

Understanding modern device drivers

Comments

Information

Published In

Sponsors

In-Cooperation

Publisher

Publication History

Permissions

Check for updates

Qualifiers

Funding Sources

Conference

Acceptance Rates

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

Login options

Full Access

View options

PDF

eReader

Share

Share this Publication link

Share on social media

Affiliations