Component-based verification of operating systems
https://doi.org/10.15514/ISPRAS-2018-30(6)-21
Abstract
The paper presents recent results on the way towards accurate and complete verification of industrial operating systems (OS). We consider here OSes, either of general purpose or actively used in some industrial domain, elaborated and maintained for a significant time, and not touching research-related OSes usually developed as a proof-of-concept. In spite of the fact that the stated goal of accurate and complete verification of industrial OS is still unreachable, we consider its decomposition into tasks of verification of various functional OS components and various their properties. The paper shows that many of these tasks can be solved with the help of various modern verification techniques and their combinations. Proposed methods can be lately integrated into an approach to the final goal. The paper summarizes the experience of various OS component and features verification from the projects conducted in ISP RAS in the last years.
About the Authors
V. V. Kuliamin
V.P.Ivannikov Institute for system programming, Russian Academy of Sciences; Lomonosov Moscow State University; FCS NRU Higher School of Economics
Russian Federation
Russian Federation
A. K. Petrenko
V.P.Ivannikov Institute for system programming, Russian Academy of Sciences; Lomonosov Moscow State University; FCS NRU Higher School of Economics
Russian Federation
Russian Federation
A. V. Khoroshilov
V.P.Ivannikov Institute for system programming, Russian Academy of Sciences; Lomonosov Moscow State University; FCS NRU Higher School of Economics; Moscow Institute of Physics and Technology
Russian Federation
Russian Federation
References
1. [32] Klein G. Operating system verification – An overview. Sadhana, vol. 34, no. 1, pp. 27-69.
2. [1] Why is the Linux kernel 15+ million lines of code? Available at:
3. [33] Devyanin P.N., Khoroshilov A.V., Kuliamin V.V., Petrenko A.K., Shchepetkov I.V. Formal Verification of OS Security Model with Alloy and Event-B. In Proc. of the International Conference on Abstract State Machines, 2014, pp. 309-313.
4. https://unix.stackexchange.com/questions/223746/why-is-the-linux-kernel-15-million-lines-ofcode/223770, accessed 10.12.2018.
5. [34] Devyanin P.N., Khoroshilov A.V., Kuliamin V.V., Petrenko A.K., Shchepetkov I.V. Comparison of specification decomposition methods in Event-B. Programming and Computer Software, vol. 42, no. 4, 2016, pp. 198-205.
6. [2] How Many Lines of Code in Windows XP? Available at:
7. [35] Wright C., Cowan C., Morris J., Smalley S., Kroah-Hartman G. Linux Security Module Framework. In Proc. of the Ottawa Linux Symposium, 2002, pp. 6-16.
8. https://www.facebook.com/windows/posts/155741344475532, accessed 10.12.2018.
9. [36] Marhé C., Moy Y. The Jessie Plugin for Deductive Verification in Frama-C. Available at: http://krakatoa.lri.fr/jessie.pdf, accessed 10.12.2018.
10. [3] Gerlits E.A., Kuliamin V.V., Maksimov A.V., Petrenko A.K., Khoroshilov A.V., Tsyvarev A.V. Testing of Operating Systems. Trudy ISP RAN/Proc. ISP RAS, vol. 26, issue 1, 2014, pp. 73-108 (in Russian). DOI: 10.15514/ISPRAS-2014-26(1)-3.
11. [37] Mandrykin M.U., Mutilin V.S. Survey of memory modeling methods in static verification tools. Trudy ISP RAN/Proc. ISP RAS, vol. 29, issue 1, 2017, pp. 195-230 (in Russian). DOI: 10.15514/ISPRAS-2017-29(1)-12.
12. [4] Bevier W.R. Kit: a Study in Operating System Verification. IEEE Transactions on Software Engineering, vol. 15, no. 11, 1989, pp. 1382-1396.
13. [5] Alkassar E., Paul W.J., Starostin A., Tsyban A. Pervasive Verification of an OS Microkernel. Lecture Notes in Computer Science, vol. 6217, 2010, pp. 71-85.
14. [6] Klein G., Andronick J., Elphinstone K., Murray T., Sewell T., Kolanski R., Heiser G. Comprehensive Formal Verification of an OS Microkernel. ACM Transactions on Computer Systems, vol. 32, no. 1, 2014.
15. [7] Burdonov I., Kossatchev A., Petrenko A., Galter D. KVEST: Automated Generation of Test Suites from Formal Specifications. Lecture Notes in Computer Science, vol. 1708, 1999, pp. 608-621.
16. [8] Bourdonov I.B., Kossatchev A.S., Kuliamin V.V., Petrenko A.K. UniTesK Test Suite Architecture. Lecture Notes in Computer Science, vol. 2391, 2002, pp. 77-88.
17. [9] Kuliamin V.V., Petrenko A.K., Pakoulin N.V., Kossatchev A.S., Bourdonov I.B. Integration of Functional and Timed Testing of Real-Time and Concurrent Systems. Lecture Notes in Computer Science, vol. 2890, 2003, pp. 450-461.
18. [10] Grinevich A., Khoroshilov A., Kuliamin V., Markovtsev D., Petrenko A., Rubanov V. Formal Methods in Industrial Software Standards Enforcement. Lecture Notes in Computer Science, vol. 4378, 2006, pp. 456-466.
19. [11] Maksimov A. Requirements-based conformance testing of ARINC 653 real-time operating systems. In Proc. of the International Conference on Data Systems in Aerospace (DASIA 2010), 2010.
20. [12] Kuliamin V. Standardization and Testing of Mathematical Functions. Lecture Notes in Computer Science, vol. 5947, 2009, pp. 257-268.
21. [13] Khoroshilov A., Rubanov V., Shatokhin E. Automated Formal Testing of C API Using T2C Framework. In Proc. of the International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2008), 2008, pp.56-70.
22. [14] Zybin R.S., Kuliamin V.V., Ponomarenko A.V., Rubanov V.V., Chernov E.S. Automation of broad sanity test generation. Programming and Computer Software, vol. 34, no. 6, 2008, pp. 351-363.
23. [15] Kuliamin V.V. Combinatoric generation of operating system software configurations. Trudy ISP RAN/Proc. ISP RAS, vol. 23, 2012, pp. 359-370 (in Russian). DOI: 10.15514/ISPRAS-2012-23-20.
24. [16] Shatokhin E. Using Dynamic Analysis to Hunt Down Problems in Kernel Modules. Presentation at LinuxCon Europe, 2011. Available at: http://linuxtesting.org/2011-LinuxConEurope-Shatokhin-KEDR.pdf, accessed 10.12.2018.
25. [17] kmemleak description. Available at: https://www.kernel.org/doc/Documentation/kmemleak.txt, accessed 10.12.2018.
26. [18] Kernel Strider. Available at: https://code.google.com/p/kernel-strider/, accessed 10.12.2018.
27. [19] Serebryany K., Iskhodzhanov T. ThreadSanitizer: data race detection in practice. In Proc. of the Workshop on Binary Instrumentation and Applications (WBIA 2009), 2009, pp. 62-71.
28. [20] Tsyvaerv A., Khoroshilov A. Using Fault Injection for Testing Linux Kernel Components. Trudy ISP RAN/Proc. ISP RAS, vol. 27, issue 5, 2015, pp. 157-174 (in Russian). DOI: 10.15514/ISPRAS-2015-27(5)-9.
29. [21] Race Hound tool. Available at: http://forge.ispras.ru/projects/race-hound/, accessed 10.12.2018.
30. [22] Erickson J., Musuvathi M., Burckhardt S., Olynyk K. Effective data-race detection for the kernel. Proc. of the USENIX Conference on Operating systems design and implementation, 2010, pp. 151-162.
31. [23] Mutilin V.S., Novikov E.M., Khoroshilov A.V. Analysis of typical faults in Linux operating system drivers. Trudy ISP RAN/Proc. ISP RAS, vol. 22, 2012, pp. 349-374 (in Russian). DOI: 10.15514/ISPRAS-2012-22-19.
32. [24] Ball T., Levin V., Rajamani S.K. A decade of software model checking with SLAM. Communications of the ACM, vol. 54, issue 7, 2011, pp. 68-76.
33. [25] Ball T., Bounimova E., Cook B., Levin V., Lichtenberg J., McGarvey C., Ondrusek B., Rajamani S.K., Ustuner A. Thorough static analysis of device drivers. In Proc. of the ACM SIGOPS/EuroSys European Conference on Computer Systems (EuroSys), 2006, pp. 73-85.
34. [26] Mutilin V.S., Novikov E.M., Strakh A.V., Khoroshilov A.V., Shved P.E. Architectire of Linux Driver Verification. Trudy ISP RAN/Proc. ISP RAS, vol. 20, 2011, pp. 163-187 (in Russian).
35. [27] Zakharov I.S., Mandrykin M.U., Mutilin V.S., Novikov E.M., Petrenko A.K., Khoroshilov A.V. Configurable Toolset for Static Verication 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.
36. [28] Beyer D., Henzinger T., Jhala R., Majumdar R. The software model checker BLAST: Applications to software engineering. International Journal on Software Tools for Technology Transfer (STTT), vol. 5, 2007, pp. 505-525.
37. [29] Beyer D., Keremoglu M.E. CPAchecker: A tool for configurable software verification. Lecture Notes in Computer Science, vol. 6806, 2011, pp. 184-190.
38. [30] Clarke E., Grumberg O, Jha S., Lu Y., Veith H. Counterexample-Guided Abstraction Refinement. Lecture Notes in Computer Science, vol. 1855, 2000, pp. 154-169.
39. [31] Andrianov P.S., Mutilin V.S., Khoroshilov A.V. Adjustable method with predicate abstraction for detection of race conditions in operating systems. Trudy ISP RAN/Proc. ISP RAS, vol. 28, issue 6, 2016, pp. 65-86 (in Russian). DOI: 10.15514/ISPRAS-2016-28(6)-5.
40. [32] Klein G. Operating system verification – An overview. Sadhana, vol. 34, no. 1, pp. 27-69.
41. [33] Devyanin P.N., Khoroshilov A.V., Kuliamin V.V., Petrenko A.K., Shchepetkov I.V. Formal Verification of OS Security Model with Alloy and Event-B. In Proc. of the International Conference on Abstract State Machines, 2014, pp. 309-313.
42. [34] Devyanin P.N., Khoroshilov A.V., Kuliamin V.V., Petrenko A.K., Shchepetkov I.V. Comparison of specification decomposition methods in Event-B. Programming and Computer Software, vol. 42, no. 4, 2016, pp. 198-205.
43. [35] Wright C., Cowan C., Morris J., Smalley S., Kroah-Hartman G. Linux Security Module Framework. In Proc. of the Ottawa Linux Symposium, 2002, pp. 6-16.
44. [36] Marhé C., Moy Y. The Jessie Plugin for Deductive Verification in Frama-C. Available at: http://krakatoa.lri.fr/jessie.pdf, accessed 10.12.2018.
45. [37] Mandrykin M.U., Mutilin V.S. Survey of memory modeling methods in static verification tools. Trudy ISP RAN/Proc. ISP RAS, vol. 29, issue 1, 2017, pp. 195-230 (in Russian). DOI: 10.15514/ISPRAS-2017-29(1)-12.
Review
For citations:
Kuliamin V.V., Petrenko A.K., Khoroshilov A.V. Component-based verification of operating systems. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2018;30(6):367-382. (In Russ.) https://doi.org/10.15514/ISPRAS-2018-30(6)-21
Email this article 