Skip to main content
SpringerLink
Log in

Linux Driver Verification

(Position Paper)

  • Conference paper
Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies (ISoLA 2012)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 7610))

Abstract

Linux driver verification is a large application area for software verification methods, in particular, for functional, safety, and security verification. Linux driver software is industrial production code — IT infrastructures rely on its stability, and thus, there are strong requirements for correctness and reliability. This implies that if a verification engineer has identified a bug in a driver, the engineer can expect quick response from the development community in terms of bug confirmation and correction. Linux driver software is complex, low-level systems code, and its characteristics make it necessary to bring to bear techniques from program analysis, SMT solvers, model checking, and other areas of software verification. These areas have recently made a significant progress in terms of precision and performance, and the complex task of verifying Linux driver software can be successful if the conceptual state-of-the-art becomes available in tool implementations.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Ball, T., Rajamani, S.K.: The Slam Project: Debugging System Software via Static Analysis. In: Proc. POPL, pp. 1–3. ACM (2002)

    Google Scholar 

  2. Basler, G., Donaldson, A., Kaiser, A., Kröning, D., Tautschnig, M., Wahl, T.: SatAbs: A Bit-Precise Verifier for C Programs. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 552–555. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  3. Beyer, D.: Competition on Software Verification. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 504–524. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  4. Beyer, D., Cimatti, A., Griggio, A., Keremoglu, M.E., Sebastiani, R.: Software Model Checking via Large-block Encoding. In: Proc. FMCAD, pp. 25–32. IEEE (2009)

    Google Scholar 

  5. Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The Software Model Checker Blast. Int. J. Softw. Tools Technol. Transfer 9(5-6), 505–525 (2007)

    Article  Google Scholar 

  6. Beyer, D., Henzinger, T.A., Keremoglu, M.E., Wendler, P.: Conditional Model Checking: A Technique to Pass Information Between Verifiers. In: Proc. FSE. ACM (2012)

    Google Scholar 

  7. Beyer, D., Henzinger, T.A., Théoduloz, G.: Program Analysis with Dynamic Precision Adjustment. In: Proc. ASE, pp. 29–38. IEEE (2008)

    Google Scholar 

  8. Beyer, D., Keremoglu, M.E.: CPAchecker: A Tool for Configurable Software Verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184–190. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  9. Beyer, D., Keremoglu, M.E., Wendler, P.: Predicate Abstraction with Adjustable-block Encoding. In: Proc. FMCAD, pp. 189–197. FMCAD (2010)

    Google Scholar 

  10. Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic Model Checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  11. Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided Abstraction Refinement for Symbolic Model Checking. J. ACM 50(5), 752–794 (2003)

    Article  MathSciNet  Google Scholar 

  12. Clarke, E., Kroning, D., Sharygina, N., Yorav, K.: SatAbs: SAT-Based Predicate Abstraction for ANSI-C. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 570–574. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  13. Cook, B., Podelski, A., Rybalchenko, A.: Terminator: Beyond Safety. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 415–418. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  14. Cordeiro, L., Morse, J., Nicole, D., Fischer, B.: Context-Bounded Model Checking with ESBMC 1.17. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 534–537. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  15. Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: Combination of Abstractions in the ASTRÉE Static Analyzer. In: Okada, M., Satoh, I. (eds.) ASIAN 2006. LNCS, vol. 4435, pp. 272–300. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  16. Dudka, K., Müller, P., Peringer, P., Vojnar, T.: Predator: A Verification Tool for Programs with Dynamic Linked Data Structures. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 545–548. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  17. Galloway, A., Lüttgen, G., Mühlberg, J.T., Siminiceanu, R.I.: Model-Checking the Linux Virtual File System. In: Jones, N.D., Müller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 74–88. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  18. Grebenshchikov, S., Gupta, A., Lopes, N.P., Popeea, C., Rybalchenko, A.: HSF(C): A Software Verifier Based on Horn Clauses. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 549–551. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  19. Gupta, A., Popeea, C., Rybalchenko, A.: Threader: A Constraint-Based Verifier for Multi-threaded Programs. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 412–417. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  20. Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from Proofs. In: Proc. POPL, pp. 232–244. ACM (2004)

    Google Scholar 

  21. Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy Abstraction. In: Proc. POPL, pp. 58–70. ACM (2002)

    Google Scholar 

  22. Khoroshilov, A., Mutilin, V., Novikov, E., Shved, P., Strakh, A.: Towards an Open Framework for C Verification Tools Benchmarking. In: Clarke, E., Virbitskaite, I., Voronkov, A. (eds.) PSI 2011. LNCS, vol. 7162, pp. 179–192. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  23. Khoroshilov, A., Mutilin, V., Petrenko, A., Zakharov, V.: Establishing Linux Driver Verification Process. In: Pnueli, A., Virbitskaite, I., Voronkov, A. (eds.) PSI 2009. LNCS, vol. 5947, pp. 165–176. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  24. Mühlberg, J.T., Lüttgen, G.: Blasting Linux Code. In: Brim, L., Haverkort, B.R., Leucker, M., van de Pol, J. (eds.) FMICS 2006 and PDMC 2006. LNCS, vol. 4346, pp. 211–226. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  25. Penninckx, W., Mühlberg, J.T., Smans, J., Jacobs, B., Piessens, F.: Sound Formal Verification of Linux’s USB BP Keyboard Driver. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 210–215. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  26. Podelski, A., Rybalchenko, A.: Transition Predicate Abstraction and Fair Termination. In: Proc. POPL, pp. 132–144. ACM (2005)

    Google Scholar 

  27. Post, H., Sinz, C., Küchlin, W.: Towards Automatic Software Model Checking of Thousands of Linux Modules — A Case Study with Avinux. Softw. Test., Verif. Reliab. 19(2), 155–172 (2009)

    Article  Google Scholar 

  28. Shved, P., Mandrykin, M., Mutilin, V.: Predicate Analysis with BLAST 2.7. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 525–527. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  29. Shved, P., Mutilin, V., Mandrykin, M.: Experience of Improving the Blast Static Verification Tool. Programming and Computer Software 38(3), 134–142 (2012)

    Article  Google Scholar 

  30. Sinz, C., Merz, F., Falke, S.: LLBMC: A Bounded Model Checker for LLVM’s Intermediate Representation. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 542–544. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  31. von Rhein, A., Apel, S., Raimondi, F.: Introducing Binary Decision Diagrams in the Explicit-state Verification of Java Code. In: Proc. Java Pathfinder Workshop (2011)

    Google Scholar 

  32. Witkowski, T., Blanc, N., Kröning, D., Weissenbacher, G.: Model Checking Concurrent Linux Device Drivers. In: Proc. ASE, pp. 501–504. ACM (2007)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Passau, Germany

    Dirk Beyer

  2. ISPRAS, Moscow, Russia

    Alexander K. Petrenko

Authors
  1. Dirk Beyer
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Alexander K. Petrenko
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institut für Informatik, Universität Potsdam, August-Bebel-Straße 89, 14482, Potsdam, Germany

    Tiziana Margaria

  2. Fakultät für Informatik, Technische Universität Dortmund, Otto-Hahn-Straße 14, 44227, Dortmund, Germany

    Bernhard Steffen

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Beyer, D., Petrenko, A.K. (2012). Linux Driver Verification. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies. ISoLA 2012. Lecture Notes in Computer Science, vol 7610. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-34032-1_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-34032-1_1

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-34031-4

  • Online ISBN: 978-3-642-34032-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation