Компонентная верификация операционных систем

В работе рассматриваются полученные недавно результаты на пути к полномасштабной верификации промышленно используемых операционных систем (ОС). Таковыми считаются не системы, разработанные в целях демонстрации определенной исследовательской идеи, а ОС, активно используемые в каких-то областях экономики и управленческой деятельности и развиваемые на протяжении значительного времени. Предлагается декомпозиция заявленной цели верификации промышленной ОС в целом на задачи верификации различных компонентов ОС и их различных свойств, методы решения которых в дальнейшем можно интегрировать в метод достижения общей цели. На данном этапе пока рассматриваются различные подходы к решению выделенных отдельных задач. Статья является экспликацией опыта верификации различных компонентов нескольких ОС и интеграции используемых для этого технологий, полученного в рамках проектов, проводимых в ИСП РАН.

операционная система, верификация, тестирование, статический анализ, дедуктивная верификация, мониторинг

1. . Why is the Linux kernel 15+ million lines of code? Режим доступа:

2. https://unix.stackexchange.com/questions/223746/why-is-the-linux-kernel-15-million-lines-ofcode/223770, дата обращения 10.12.2018.

3. . How Many Lines of Code in Windows XP? Режим доступа:

4. https://www.facebook.com/windows/posts/155741344475532, дата обращения 10.12.2018.

5. . Герлиц Е.А., Кулямин В.В., Максимов А.В., Петренко А.К., Хорошилов А.В., Цыварев А.В. Тестирование операционных систем. Труды ИСП РАН, том 26, вып. 1, 2014 г., стр. 73-108. DOI: 10.15514/ISPRAS-2014-26(1)-3.

6. . Bevier W.R. Kit: a Study in Operating System Verification. IEEE Transactions on Software Engineering, vol. 15, no. 11, 1989, pp. 1382-1396.

7. . 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.

8. . 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.

9. . 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.

10. . 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.

11. . 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.

12. . 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.

13. . 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.

14. . Kuliamin V. Standardization and Testing of Mathematical Functions. Lecture Notes in Computer Science, vol. 5947, 2009, pp. 257-268.

15. . 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.

16. . 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.

17. . Кулямин В.В. Комбинаторная генерация программных конфигураций ОС. Труды ИСП РАН, том 23, 2012 г., стр. 359-370. DOI: 10.15514/ISPRAS-2012-23-20.

18. . Shatokhin E. Using Dynamic Analysis to Hunt Down Problems in Kernel Modules. Presentation at LinuxCon Europe, 2011. Режим доступа: http://linuxtesting.org/2011-LinuxConEurope-Shatokhin-KEDR.pdf, дата обращения 10.12.2018.

19. . kmemleak description. Режим доступа: https://www.kernel.org/doc/Documentation/kmemleak.txt, дата обращения 10.12.2018.

20. . Kernel Strider. Режим доступа: https://code.google.com/p/kernel-strider/, дата обращения 10.12.2018.

21. . 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.

22. . Цыварев А.В., Хорошилов А.В. Использование симуляции сбоев при тестировании компонентов ядра ОС Linux. Труды ИСП РАН, том 27, вып. 5, 2015 г., стр. 157-174. DOI: 10.15514/ISPRAS-2015-27(5)-9.

23. . Race Hound tool. Режим доступа: http://forge.ispras.ru/projects/race-hound/, дата обращения 10.12.2018.

24. . 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.

25. . Мутилин В.С., Новиков Е.М., Хорошилов А.В. Анализ типовых ошибок в драйверах операционной системы Linux. Труды ИСП РАН, том 22, 2012 г., стр. 349-374. DOI: 10.15514/ISPRAS-2012-22-19.

26. . 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.

27. . 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.

28. . Мутилин В.С., Новиков Е.М., Страх А.В., Хорошилов А.В., Швед П.Е. Архитектура Linux Driver Verification. Труды ИСП РАН, том 20, 2011 г., стр. 163-187.

29. . Захаров И.С., Мандрыкин М.У., Мутилин В.С., Новиков Е.М., Петренко А.К., Хорошилов А.В. Конфигурируемая система статической верификации модулей ядра операционных систем. Труды ИСП РАН, том 26, вып. 2, 2014 г., стр. 5-42. DOI: 10.15514/ISPRAS-2014-26(2)-1.

30. . 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.

31. . Beyer D., Keremoglu M.E. CPAchecker: A tool for configurable software verification. Lecture Notes in Computer Science, vol. 6806, 2011, pp. 184-190.

32. . 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.

33. . Андрианов П.С., Мутилин В.С., Хорошилов А.В. Конфигурируемый метод поиска состояний гонок в операционных системах с использованием предикатных абстракций. Труды ИСП РАН, том 28, вып. 6, 2016 г., стр. 65-86. DOI: 10.15514/ISPRAS-2016-28(6)-5.

34. . Klein G. Operating system verification – An overview. Sadhana, vol. 34, no. 1, pp. 27-69.

35. . 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.

36. . 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.

37. . 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.

38. . Marhé C., Moy Y. The Jessie Plugin for Deductive Verification in Frama-C. Режим доступа: http://krakatoa.lri.fr/jessie.pdf, дата обращения 10.12.2018.

39. . Мандрыкин М.У., Мутилин В.С. Обзор подходов к моделированию памяти в инструментах статической верификации. Труды ИСП РАН, том 29, вып. 1, 2017 г., стр. 195-230. DOI: 10.15514/ISPRAS-2017-29(1)-12.