Skip to main content
Springer Nature Link
Log in

Pattern-based environment modeling for static verification of Linux kernel modules

  • Computer Algebra, Applied Logic, Circuit Synthesis
  • Published:
Programming and Computer Software Aims and scope Submit manuscript

Abstract

Linux kernel modules operate in an event-driven environment. During static verification of such modules it is necessary to take into consideration all feasible scenarios of interaction between modules and their environment. The paper presents a new method which allows to automatically generate an environment model for a particular kernel module on the base of analysis of its source code and a set of specifications describing patterns of scenarios of interaction between modules and their environment. In specifications one can describe both generic patterns that are widespread in the Linux kernel and detailed specific patterns for a particular subsystem. It drastically reduces a specification size and thus helps to verify more modules with less efforts. Proposed method was implemented as a component of Linux Driver Verification Tools and was applied for static verification of modules from almost all Linux kernel subsystems.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

References

  1. Palix, N., Thomas, G., Saha, S., et al., Faults in Linux: ten years later, Proc. 16th Int. Conference on Architectural Support for Programming Languages and Operating Systems. ASPLOS XVI, ACM, 2011, pp. 305–318, URL: http://doi.acm.org/10.1145/1950365.1950401.

    Google Scholar 

  2. Mutilin, V.S., Novikov, E.M., and Khoroshilov, A.V., Analiz tipovykh oshibok v drajverakh operatsionnoj sistemy Linux [Analysis of typical faults in Linux operating system drivers], Trudy ISP RAN [Proc. ISP RAS], 2012, vol. 22, pp. 349–374.

    Google Scholar 

  3. Beyer, D. and Keremoglu M. Erkan, CPAchecker: A tool for configurable software verification, Computer Aided Verification, Springer Berlin Heidelberg, 2011, vol. 6806 of Lecture Notes in Computer Science, pp. 184–190, URL: http://dx.doi.org/10.1007/978-3-642-22110-1_16.

    Chapter  Google Scholar 

  4. Beyer, D., Henzinger, T.A., Jhala, R., and Majumdar, R., The software model checker Blast, International Journal on Software Tools for Technology Transfer, 2007, vol. 9, nos. 5–6, pp. 505–525, URL: http://dx.doi.org/10.1007/s10009-007-0044-z.

    Article  Google Scholar 

  5. Shved, P., Mandrykin, M., and Mutilin, V., Predicate analysis with BLAST 2.7, Tools and Algorithms for the Construction and Analysis of Systems, Springer Berlin Heidelberg, 2012, vol. 7214 of Lecture Notes in Computer Science, pp. 525–527, URL: http://dx.doi.org/10.1007/978-3-642-28756-5_39.

    Chapter  Google Scholar 

  6. Clarke, E., Kroening, D., and Lerda, F., A tool for checking ANSI-C programs, Tools and Algorithms for the Construction and Analysis of Systems, Springer Berlin Heidelberg, 2004, vol. 2988 of Lecture Notes in Computer Science, pp. 168–176, URL: http://dx.doi.org/10.1007/978-3-540-24730-2_15.

    Chapter  Google Scholar 

  7. Aws Albarghouthi, Arie Gurfinkel, Yi Li, et al., UFO: Verification with interpolants and abstract interpretation, Tools and Algorithms for the Construction and Analysis of Systems, Springer Berlin Heidelberg, 2013, vol. 7795 of Lecture Notes in Computer Science, pp. 637–640, URL: http://dx.doi.org/10.1007/978-3642-36742-7_52.

    Chapter  Google Scholar 

  8. Engler Dawson and Musuvathi Madanlal, Static analysis versus software model checking for bug finding, Verification, Model Checking, and Abstract Interpretation, Springer Berlin Heidelberg, 2004, vol. 2937 of Lecture Notes in Computer Science, pp. 191–210, URL: http://dx.doi.org/10.1007/978-3-540-24622-0_17.

    Chapter  Google Scholar 

  9. Milner, R., Parrow, J., and Walker, D., A calculus of mobile processes, I, Inf. Comput., 1992, vol. 100, no. 1, p. 140, URL: http://dx.doi.org/10.1016/08905401(92)90008-4.

    MathSciNet  Google Scholar 

  10. Milner, R., The Polyadic π-Calculus: a Tutorial, LFCS, Department of Computer Science, University of Edinburgh, 1991, p. 49.

    Google Scholar 

  11. Khoroshilov, A., Mutilin, V., Novikov, E., et al., Towards an open framework for C verification tools benchmarking, Perspectives of Systems Informatics, Springer Berlin Heidelberg, 2012, vol. 7162 of Lecture Notes in Computer Science, pp. 179–192, URL: http://dx.doi.org/10.1007/78-3-642-29709-0_17.

    Chapter  Google Scholar 

  12. Zakharov, I.S., Mandrykin, M.U., Mutilin, V.S., et al., Konfiguriruemaya sistema staticheskoj verifikatsii modulej yadra operatsionnykh sistem [Configurable toolset for static verification of operating systems Kernel modules], Trudy ISP RAN [Proc. ISP RAS], 2014, vol. 26, pp. 5–42.

    Google Scholar 

  13. Novikov, E.M., An approach to implementation of aspect-oriented programming for C, Programming and Computer Software, 2013, vol. 39, no. 4, pp. 194–206, URL: http: //dx.doi.org/10.1134/S0361768813040051.

    Article  MATH  Google Scholar 

  14. Novikov, E.M. and Khoroshilov, A.V., Ispol’zovanie aspektno-orientirovannogo programmirovaniya dlya vypolneniya zaprosov po iskhodnomu kodu programm [Using Aspect-Oriented Programming for Querying Source Code], Trudy ISP RAN [Proc. ISP RAS], 2012, vol. 23, pp. 371–386.

    Google Scholar 

  15. Zakharov, I.S., Mutilin, V.S., Novikov, E.M., and Khoroshilov, A.V., Modelirovanie okruzheniya drajverov ustrojstv operatsionnoj sistemy Linux [Environment modeling of Linux operating system device drivers], Trudy ISP RAN [Proc. ISP RAS], 2013, vol. 25, pp. 85–112.

    Google Scholar 

  16. Beyer Dirk, Second competition on software verification, Tools and Algorithms for the Construction and Analysis of Systems, Springer Berlin Heidelberg, 2013, vol. 7795 of Lecture Notes in Computer Science, pp. 594–609, URL: http://dx.doi.org/10.1007/978-3-642-36742-7_43.

    Chapter  Google Scholar 

  17. Witkowski, T., Blanc, N., Kroening, D., and Weissenbacher, G., Model checking concurrent Linux device drivers, Proc. 22nd IEEE/ACM Int. Conference on Automated Software Engineering, New York, NY, USA: ACM, 2007, pp. 501–504.

    Google Scholar 

  18. Post Hendrik and Küchlin Wolfgang, Integrated static analysis for Linux device driver verification, Integrated Formal Methods, Berlin, Heidelberg: Springer-Verlag, 2007, pp. 518–537, URL: http://portal.acm.org/citation.cfm?id=1770498.1770525.

    Google Scholar 

  19. Ball, T., Bounimova, E., Cook, B., et al., Thorough static analysis of device drivers, SIGOPS Oper. Syst. Rev., 2006, vol. 40, no. 4, pp. 73–85.

    Article  Google Scholar 

  20. Ivancic, F., Balakrishnan, G., Gupta, A., et al., DC2: A framework for scalable, scope-bounded software verification, Automated Software Engineering (ASE), Proc. 2011 26th IEEE/ACM International Conference on, 2011, pp. 133–142.

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute for System Programming of the Russian Academy of Sciences, ul. Alexandera Solzhenitsyna 25, Moscow, 109004, Russia

    I. S. Zakharov, V. S. Mutilin & A. V. Khoroshilov

Authors
  1. I. S. Zakharov
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. V. S. Mutilin
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. A. V. Khoroshilov
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to I. S. Zakharov.

Additional information

Original Russian Text © I.S. Zakharov, V.S. Mutilin, A.V. Khoroshilov, 2015, published in Programmirovanie, 2015, Vol. 41, No. 3.

The article was translated by the authors.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Zakharov, I.S., Mutilin, V.S. & Khoroshilov, A.V. Pattern-based environment modeling for static verification of Linux kernel modules. Program Comput Soft 41, 183–195 (2015). https://doi.org/10.1134/S036176881503007X

Download citation

  • Received:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1134/S036176881503007X

Keywords

Search

Navigation