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.
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.References
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.
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.
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.
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.
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.
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.
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.
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.
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.
Milner, R., The Polyadic π-Calculus: a Tutorial, LFCS, Department of Computer Science, University of Edinburgh, 1991, p. 49.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
Author information
Authors and Affiliations
Corresponding author
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
About this article
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
Received:
Published:
Issue Date:
DOI: https://doi.org/10.1134/S036176881503007X