Incremental development of environment model and requirement specifications for subsystems of operating system monolithic kernels
https://doi.org/10.15514/ISPRAS-2017-29(6)-2
Abstract
Methods and tools for automated static verification aim at detecting all violations of checked requirements in target programs under certain assumptions even without complete models and formal specifications. The given feature form a basis of the suggested method for incremental development of environment model and requirement specifications for subsystems of operating system monolithic kernels. This method was implemented on top of static verification framework Klever. It was evaluated by checking the Linux kernel TTY subsystem. During this study some Klever components were improved. Besides, we fixed some existing and developed new environment model and requirement specifications. Almost all made changes also helps at static verification of loadable modules of the Linux kernel. Developers of automated static verification tool CPAchecker fixed several issues that we revealed and reported during the research. Overall developed specifications allowed to increase function coverage of the TTY subsystem from 5% to 83%. Moreover, we revealed 7 bugs in loadable modules verified together with the TTY subsystem.
About the Authors
I. S. Zakharov
Ivannikov Institute for System Programming of the Russian Academy of Sciences
Russian Federation
Russian Federation
E. M. Novikov
Ivannikov Institute for System Programming of the Russian Academy of Sciences
Russian Federation
Russian Federation
References
1. E.M. Novikov. Static verification of operating system monolithic kernels. Trudy ISP RAN/Proc. ISP RAS, vol, 29, issue 2, pp. 97-116, 2017 (in Russian). DOI: 10.15514/ISPRAS-2017-29(2)-4
2. E.M. Novikov. Evolution of the Linux kernel. Trudy ISP RAN/Proc. ISP RAS, vol. 29, issue 2, pp. 77-96, 2017 (in Russian). DOI: 10.15514/ISPRAS-2017-29(2)-3
3. D. Engler, M. Musuvathi. Static analysis versus model checking for bug finding. In Proceedings of the 5th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'04), LNCS, volume 2937, pp. 191-210, 2004.
4. T. Ball, S.K. Rajamani. SLIC: A specification language for interface checking of C. Technical Report MSR-TR-2001-21, Microsoft Research, 2001.
5. E.M. Novikov. Development of Contract Specifications Method for Verification of Linux Kernel Modules. PhD thesis, Institute for System Programming of the Russian Academy of Sciences, 2013 (in Russian).
6. A. Khoroshilov, V. Mutilin, E. Novikov, I. Zakharov. Modeling Environment for Static Verification of Linux Kernel Modules. In Proceedings of the 9th International Ershov Informatics Conference (PSI'14), LNCS, vol. 8974, pp. 400-414, 2014.
7. K.R.M. Leino. Developing verified programs with Dafny. In Proceedings of the 2013 International Conference on Software Engineering (ICSE '13), pp. 1488-1490, 2013.
8. P.N. Devyanin, V.V. Kulyamin, A.K. Petrenko, A.V. Khoroshilov, I.V. Shchepetkov. Comparison of Specification Decomposition Methods in Event-B. Programming and Computer Software, vol. 42, issue 4, pp. 17-26, 2016.
9. M.U. Mandrykin, V.S. Mutilin. Survey of memory modeling methods in static verification tools. Trudy ISP RAN/Proc. ISP RAS, vol. 29, issue 1, pp. 195-230, 2017. DOI: 10.15514/ISPRAS-2017-29(1)-12
10. M.U. Mandrykin, A.V. Khoroshilov. Towards Deductive Verification of C Programs with Shared Data. Trudy ISP RAN/Proc. ISP RAS, vol. 27, issue 4, pp. 49-68, 2015. DOI: 10.15514/ISPRAS-2015-27(4)-4
11. G. Klein, J. Andronick, K. Elphinstone, T. Murray, T. Sewell, R. Kolanski, G. Heiser. Comprehensive formal verification of an OS microkernel. ACM Transactions on Computer Systems (TOCS), vol. 32, issue 1, 70 p., 2014.
12. D. Bejer, A.K. Petrenko. Linux Driver Verification. Trudy ISP RAN/Proc. ISP RAS, vol. 23, pp. 405-412, 2012 (in Russian). DOI: 10.15514/ISPRAS-2012-23-23
13. I.S. Zakharov, 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. Programming and Computer Software, vol. 41, issue 1, pp. 49-64, 2015. DOI: 10.1134/S0361768815010065
14. E. Novikov, I. Zakharov. Towards Automated Static Verification of GNU C Programs. In Proceedings of the 11th International Ershov Informatics Conference (PSI'17), LNCS, volume 10742, 2018 (to appear).
15. D. Beyer, M.E. Keremoglu. CPAchecker: A tool for configurable software verification. In: Proceedings of the 23rd International Conference on Computer Aided Verification, Berlin, Heidelberg, Springer, pp. 184-190, 2011.
Review
For citations:
Zakharov I.S., Novikov E.M. Incremental development of environment model and requirement specifications for subsystems of operating system monolithic kernels. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2017;29(6):25-48. (In Russ.) https://doi.org/10.15514/ISPRAS-2017-29(6)-2
Email this article 