Static Verification of Linux Kernel Configurations
https://doi.org/10.15514/ISPRAS-2017-29(4)-14
Abstract
The Linux kernel is often used as a real world case study to demonstrate novel software product line engineering research methods. It is one of the most sophisticated programs nowadays. To provide the most safe experience of building of Linux product line variants it is necessary to analyse Kconfig file as well as source code. Ten of thousands of variable statements and options even by the standards of modern software development. Verification researchers offered lots of solutions for this problem. Standard procedures of code verification are not acceptable here due to time of execution and coverage of all configurations. We offer to check the operating system with special wrapper for tools analyzing built code and configuration file connected with coverage metric. Such a bundle is able to provide efficient tool for calculating all valid configurations for predetermined set of code and Kconfig. Metric can be used for improving existing analysis tools as well as decision of choice the right configuration. Our main goal is to contribute to a better understanding of possible defects and offer fast and safe solution to improve the validity of evaluations based on Linux. This solution will be described as a program with instruction for inner architecture implementation.
About the Authors
S. V. Kozin
National Research University Higher School of Economics
Russian Federation
Russian Federation
V. S. Mutilin
Institute for System Programming of the Russian Academy of Sciences
Russian Federation
Russian Federation
References
1. Jacobson I., Griss M., Jonsson P. Software Reuse, Architecture, Process and Organization for Business Success. Addison-Wesley, 1997.
2. Bosch J. Design and Use of Software Architectures: Adopting and Evolving a Product Line Approach. Pearson Education, 2000.
3. Clements P., Northrop L. Software Product Lines: Practices and Patterns. SEI Series in Software Engineering, Addison-Wesley, 2001.
4. Pohl K., Böckle G., van der Linden F. J. Software Product Line Engineering: Foundations, Principles and Techniques. Springer-Verlag, 2005. DOI: 10.1007/3-540-28901-1.
5. Kuliamin V.V., Lavrischeva E.M., Mutilin V.S., Petrenko A.K. Verification and analysis of variable operating systems. Trudy ISP RAN/Proc. ISP RAS, vol. 28, issue 3, 2016, pp. 189-208 (in Russian). DOI: 10.15514/ISPRAS-2016-28(3)-12
6. Lotufo R., She S., Berger T., Czarnecki K., Wąsowski A. Evolution of the Linux kernel variability model. Proc. of SPLC’10, LNCS 6287:136-150, Springer, 2010. DOI: 10.1007/978-3-642-15579-6_10.
7. Lavrischeva Е. М., Koval G.I., Slabospickaya О.O., Kolesnik A.L. Features of management processes when creating families of software systems [Osobennosti processov upravleniya pri sozdanii semejstv programmnyh system]. Problems of programming [Problemy programmirovaniya], 3:40-49, 2009 (in Russian).
8. Lavrischeva Е.М., Koval G.I., Slabospickaya О.O., Kolesnik A.L. Teoreticheskie aspekty upravleniya variabel'nost'yu v semejstvah programmnyh sistem. Bulletin of KSU, a series of physics and mathematics [Vesnik KNU, seriya fiz.–mat. nauk], 1:151-158, 2011 (in Russian).
9. Al Bessey, Ken Block, Ben Chelf, Andy Chou, Bryan Fulton, Seth Hallem, Charles Henri-Gros, Asya Kamsky, Scott McPeak, Dawson Engler, A “Few Billion Lines of Code Later: Using Static Analysis to Find Bugs in the Real World”, Communications of the ACM, Vol. 53 No. 2, pp. 66-75
10. Borodin A.E., Belevancev A.A, A Static Analysis Tool Svace as a Collection of Analyzers with Various Complexity Levels, Trudy ISP RAN/Proc. ISP RAS, vol 27, issue. 6, 2015, pp. 111-134. DOI: 10.15514/ISPRAS-2015-27(6)-8 (in Russian).
11. Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, “The software model checker BLAST”, Int J Softw Tools Technol Transfer (2007) 9:505–525, Springer-Verlag 2007
12. Andy Kenner, Christian Kastner, SteffenHaase, Thomas Leich, “TypeChef: toward type checking #ifdef variability in C”. Proceeding FOSD ’10 Proceedings of the 2nd Internationsal Workchop on Feature-Oriented Software Development, pp. 25-32, Eindhoven, The Netherlands, Oct. 10, 2010.
13. Stephan Henglein. Vampyr configurability aware compile testing of source files. Linux Plumber Conference, Oct 15-17, 2014, Dusseldorf, Germany. Available at: http://www.linuxplumbersconf.net/2014/ocw//system/presentations/2313/original/hengelein.pdf, accessed 12.01.2017.
14. Kulyamin V., Model-based testing [Testirovanie na osnove modeley]. (online publication). Available at: http://mbt-course.narod.ru/Lecture03.pdf, accessed 12.02.2017 (in Russian).
15. Alber Zever. Pycparcer wiki. (Onine publication). Available at: https://pypi.python.org/pypi/pycparser/2.14. accessed 7.05.2017.
16. I.S. Zaharov, M.U. Mandrykin, V.S. Mutilin, E.M. Novikov, A.K. Petrenko, A.V. Khoroshilov. Configurable Toolset for Static Verification of Operating Systems Kernel Modules. Trudy ISP RAN/Proc. ISP RAS, vol 26, issue 2, 2014, pp. 5-42 (in Russian). DOI: 10.15514/ISPRAS-2014-26(2)-1.
Review
For citations:
Kozin S.V., Mutilin V.S. Static Verification of Linux Kernel Configurations. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2017;29(4):217-230. https://doi.org/10.15514/ISPRAS-2017-29(4)-14
Email this article 