Static verification of operating system monolithic kernels
https://doi.org/10.15514/ISPRAS-2017-29(2)-4
Abstract
The most of modern widely used operating systems have monolithic kernels since this architecture aims at reaching maximum performance. Usually monolithic kernels without various extensions like device drivers consist of several million lines of code in the programming language C/C++ and in the assembly language. With time, their source code evolves quite intensively: a new functionality is supported, various operations are optimized, bugs are fixed. The high practical value of operating system monolithic kernels defines strict requirements for their functionality, security, reliability and performance. Approaches for software quality assurance which are currently used in practice help to identify and to fix quite a number of bugs, but none of them allows to detect all possible bugs of kinds sought for. This article shows that different approaches to static verification, which are aimed at solving this task, have significant restrictions if applied to monolithic kernels as a whole, primarily due to a large size and complexity of source code that is constantly evolving. As a first step towards static verification of operating system monolithic kernels a method is proposed for decomposition of kernels into subsystems.
About the Author
E. M. Novikov
Institute for System Programming of the Russian Academy of Sciences
Russian Federation
Russian Federation
References
1. V.E. Karpov, K.A. Kon'kov. Fundamentals of operating systems. Kurs lekcij. Uchebnoe posobie [Lectures. Study material]. M.: Internet-universitet informacionnyh tehnologij, 536 p., 2005 (in Russian).
2. E.M. Novikov. Evolution of the Linux kernel. Trudy ISP RAN/Proc. ISP RAS, volume 29, issue 2, 2017, pp. xx-xx (in Russian). DOI: 10.15514/ISPRAS-2017-29(2)-3
3. R.L. Glass. Facts and fallacies of software engineering. Addison-Wesley Professional, 2002.
4. J. Corbet, G. Kroah-Hartman. Linux kernel development. How Fast It is Going, Who is Doing It, What They Are Doing and Who is Sponsoring the Work. http://go.linuxfoundation.org/linux-kernel-development-report-2016, 2016.
5. A.V. Cyvarev, V.A. Martirosjan. Testing of Linux File System Drivers. Trudy ISP RAN/Proc. ISP RAS, volume 23, pp. 413-426, 2012 (in Russian). DOI: 10.15514/ISPRAS-2012-23-24
6. J.-P. Lozi, B. Lepers, J. Funston, F. Gaud, V. Quéma, A. Fedorova. The Linux scheduler: a decade of wasted cores. In Proceedings of the Eleventh European Conference on Computer Systems (EuroSys '16), article 1, 16 pages, 2016.
7. A. Chou, J. Yang, B. Chelf, S. Hallem, D. Engler. An empirical study of operating systems errors. In Proceedings of the eighteenth ACM symposium on Operating systems principles (SOSP'01), pp. 73-88, 2001.
8. J.L. Lawall, J. Brunel, N. Palix, H.R. Rydhof, H. Stuart, G. Muller. WYSIWIB: A declarative approach to finding API protocols and bugs in Linux code. Proceedings of the 39th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN), pp. 43-52, 2009.
9. A. Avetisjan, A. Belevancev, A. Borodin, V. Nesov. Using static analysis for finding security vulnerabilities and critical errors in source code. Trudy ISP RAN/Proc. ISP RAS, volume 21, pp. 23-38, 2011 (in Russian).
10. N. Palix, G. Thomas, S. Saha, C. Calves, J. Lawall, G. Muller. Faults in Linux: ten years later. In Proceedings of the 15th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS'11), pp. 305-318, 2011.
11. G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, S. Winwood. seL4: formal verification of an OS kernel. In Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles (SOSP'09), pp. 207-220, 2009.
12. J. Andronick, D. Greenaway, K. Elphinstone. Towards proving security in the presence of large untrusted components. In Proceedings of the 5th international conference on Systems software verification (SSV'10), pp. 9-9, 2010.
13. G. Klein. From a verified kernel towards verified systems. In Proceedings of the 8th Asian conference on Programming languages and systems (APLAS'10), pp. 21-33, 2010.
14. I. Kuz, G. Klein, C. Lewis, A. Walker. capDL: a language for describing capability-based systems. In Proceedings of the first ACM asia-pacific workshop on Workshop on systems (APSys'10), pp. 31-36, 2010.
15. T. Sewell, S. Winwood, P. Gammie, T. Murray, J. Andronick, G. Klein. seL4 enforces integrity. In Proceedings of the Second international conference on Interactive theorem proving (ITP'11), pp. 325-340, 2011.
16. T. Murray, D. Matichuk, M. Brassil, P. Gammie, G. Klein. Noninterference for operating system kernels. In Proceedings of the Second international conference on Certified Programs and Proofs (CPP'12), pp. 126-142, 2012.
17. M. Daum, N. Billing, G. Klein. Concerned with the unprivileged: user programs in kernel refinement. Formal Aspects of Computing, vol. 26, issue 6, pp. 1205-1229, 2014.
18. 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 pages, 2014.
19. C. Baumann, B. Beckert, H. Blasum, T. Bormer. Formal Verification of a Microkernel Used in Dependable Software Systems. In Proceedings of the 28th International Conference on Computer Safety, Reliability, and Security (SAFECOMP'09), pp. 187-200, 2009.
20. E. Alkassar, W. J. Paul, A. Starostin, A. Tsyban. Pervasive verification of an OS microkernel: inline assembly, memory consumption, concurrent devices. In Proceedings of the Third international conference on Verified software: theories, tools, experiments (VSTTE'10), pp. 71-85, 2010.
21. C. Baumann, T. Bormer, H. Blasum, S. Tverdyshev. Proving Memory Separation in a Microkernel by Code Level Verification. In Proceedings of the 14th IEEE International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing Workshops (ISORCW '11), pp. 25-32, 2011.
22. S. Schmaltz, A. Shadrin. Integrated semantics of intermediate-language c and macro-assembler for pervasive formal verification of operating systems and hypervisors from VerisoftXT. In Proceedings of the 4th international conference on Verified Software: theories, tools, experiments (VSTTE'12), pp. 18-33, 2012.
23. R. Gu, J. Koenig, T. Ramananandro, Z. Shao, X. Wu, S.-C. Weng, H. Zhang, Y. Guo. Deep Specifications and Certified Abstraction Layers. SIGPLAN Not. 50, 1, pp. 595-608, 2015.
24. M. Děcký. A road to a formally verified general-purpose operating system. In Proceedings of the First international conference on Architecting Critical Systems (ISARCS'10), pp. 72-88, 2010.
25. H. Mai, E. Pek, H. Xue, S. T. King, P. Madhusudan. Verifying security invariants in ExpressOS. In Proceedings of the eighteenth international conference on Architectural support for programming languages and operating systems (ASPLOS '13), pp. 293-304, 2013.
26. J.F. Ferreira, C. Gherghina, G. He, S. Qin, W.-N. Chin. Automated verification of the FreeRTOS scheduler in Hip/Sleek. Int. J. Softw. Tools Technol. Transf. 16, 4, pp. 381-397, 2014.
27. A. Gotsman, H. Yang. Modular verification of preemptive OS kernels. In Proceedings of the 16th ACM SIGPLAN international conference on Functional programming (ICFP '11), pp. 404-417, 2011.
28. J. Yang, Chris Hawblitzel. Safe to the last instruction: automated verification of a type-safe operating system. In Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '10), pp. 99-110, 2010.
29. M. Danish, H. Xi. Operating system development with ATS: work in progress. In Proceedings of the 4th ACM SIGPLAN workshop on Programming languages meets program verification (PLPV'10), pp. 9-14, 2010.
30. M. Danish, H. Xi. Using Lightweight Theorem Proving in an Asynchronous Systems Context. In Proceedings of the 6th International Symposium on NASA Formal Methods, vol. 8430, pp. 158-172. 2014.
31. B.W. Cronkite-Ratcliff. Development of automatically verifiable systems using data representation synthesis. In Proceedings of the 2013 companion publication for conference on Systems, programming, & applications: software for humanity (SPLASH '13), pp. 109-110, 2013.
32. 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.
33. A. DeHon, B. Karel, T. F. Knight, Jr., G. Malecha, B. Montagu, R. Morisset, G. Morrisett, B. C. Pierce, R. Pollack, S. Ray, O. Shivers, J. M. Smith, G. Sullivan. Preliminary design of the SAFE platform. In Proceedings of the 6th Workshop on Programming Languages and Operating Systems (PLOS '11), article 4, 5 pages, 2011.
34. A. Azevedo de Amorim, N. Collins, A. DeHon, D. Demange, C. Hriţcu, D. Pichardie, B. C. Pierce, R. Pollack, A. Tolmach. A verified information-flow architecture. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'14), pp. 165-178, 2014.
35. T. Ball, E. Bounimova, R. Kumar, V. Levin. SLAM2: Static driver verification with under 4% false alarms. In Proceedings of the 10th International Conference on Conference on Formal Methods in Computer-Aided Design (FMCAD'10), pp. 35-42, 2010.
36. D. Beyer. Status Report on Software Verification (Competition Summary SV-COMP 2014). In Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and of Analysis Systems (TACAS'14), LNCS 8413, pp. 373-388, 2014.
37. D. Beyer. Software Verification and Verifiable Witnesses (Report on SV-COMP 2015). In Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and of Analysis Systems (TACAS'15), LNCS 9035, pp. 401-416, 2015.
38. T. Ball, V. Levin, S.K. Rajamani. A decade of software model checking with SLAM. Communications of the ACM, vol. 54, issue 7, pp. 68-76, 2011.
39. T. Witkowski, N. Blanc, D. Kroening, G. Weissenbacher. Model checking concurrent Linux device drivers. In Proceedings of the 22nd IEEE/ACM international conference on Automated Software Engineering (ASE'07), pp. 501-504, 2007.
40. H. Post, W. Küchlin. Integrated static analysis for Linux device driver verification. In Proceedings of the 6th International Conference on Integrated Formal Methods (IFM'07), LNCS, vol. 4591, pp. 518-537, 2007.
41. D. Bejer, A.K. Petrenko. Linux Driver Verification. Trudy ISP RAN/Proc. ISP RAS, volume 23, pp. 405-412, 2012 (in Russian). DOI: 10.15514/ISPRAS-2012-23-23
42. 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, volume 41, issue 1, pp 49-64, 2015. DOI: 10.1134/S0361768815010065
43. T. Ströder, C. Aschermann, F. Frohn, J. Hensel, J. Giesl. AProVE: Termination and Memory Safety of C Programs (Competition Contribution). In Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'15), LNCS 9035, pp. 417-419, 2015.
44. M. Kotoun, P. Peringer, V. Šoková, T. Vojnar. Optimized PredatorHP and the SV-COMP Heap and Memory Safety Benchmark. In Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'16), vol. 9636, pp. 942-945, 2016.
45. 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, vol. 2937, pp. 191-210, 2004.
46. T. Ball, S.K. Rajamani. SLIC: A specification language for interface checking of C. Technical Report MSR-TR-2001-21, Microsoft Research, 2001.
47. 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.
48. 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 8974, pages 400-414, 2014. DOI: 10.1007/978-3-662-46823-4_32
Review
For citations:
Novikov E.M. Static verification of operating system monolithic kernels. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2017;29(2):97-116. (In Russ.) https://doi.org/10.15514/ISPRAS-2017-29(2)-4
Email this article 