Об интеграции формальных методов в задачах верификации операционных систем

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

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

1. Proceedings of the 1st International Conference on Integrated Formal Methods. Edited by K. Araki, A. Galloway, K. Taguchi, York, 28-29 June 1999. Springer-Verlag, 1999. ISBN:1-85233-107-0.

2. L. De Moura, N. Bjørner. Z3: an Efficient SMT Solver. Proceedings of TACAS’2008. LNCS 4963:337-340, Springer-Verlag, 2008.

3. http://github.com/Z3Prover/z3

4. C. Barret, C. L. Conway, M. Deters, L. Hadarean, D. Jovanović, T. King, A. Reynolds, C. Tinelli. CVC4. Proceedings of CAV’2011, LNCS 6806:171-177, Springer, 2011.

5. http://cvc4.cs.nyuedu/web

6. M. Veanes, C. Campbell, W. Grieskamp, W. Schulte, N. Tillmann, L. Nachmanson. Model-based Testing of Object-oriented Reactive Systems with SpecExplorer. Proceedings of FORTEST’2008, LNCS 4949:39-76, Springer-Verlag, 2008.

7. N. Tillmann, J. de Halleux. Pex - White Box Test Generation for.NET. Proceedings of TAP’2008, LNCS 4966:134-153, Springer-Verlag, 2008.

8. P. Godefroid. Random Testing for Security: Blackbox vs. Whitebox Fuzzing. Proceedings of 2-nd International Workshop on Random Testing, p. 1-1, ACM, 2007.

9. T. A. Henzinger, R. Jhala, R. Majumdar, G. Sutre. Software Verification with BLAST. Proceedings of SPIN’2003, Model Checking Software, LNCS 2648:235-239, Springer-Verlag, 2003.

10. T. Ball, B. Cook, V. Levin, S. K. rajamani. SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft. Proceedings of IFM’2004, LNCS 2999:1-20, Springer-Verlag, 2004.

11. D. Beyer, M. E. Keremoglu. CPAchecker: a Tool for Configurable Software Verification. Proceedings of CAV’2011, LNCS 6806:184-190, Springer, 2011.

12. G. Canet, P. Cuoq, B. Monate. A Value Analysis for C Programs. Proceedings of SCAM’2009, p. 123-124, IEEE, 2009.

13. J.-R. Abrial, M. Butler, S. Hallerstede, L. Voisin. An Open Extensible Tool Environment for Event-B. Proceedings of ICFEM’2006, Formal Methods and Software Engineering, LNCS 4260:588-605, Springer-Verlag, 2006.

14. А. К. Петренко. Унификация в автоматизации тестирования. Позиция UniTESK. Труды Института системного программирования РАН 14(1):7-22, 2008.

15. В. В. Кулямин. Интеграция методов верификации программных систем. Программирование, 35(4):41-55, 2009.

16. В. В. Кулямин. Методы верификации программного обеспечения. Статья-победитель конкурса обзорно-аналитических статей по направлению «Информационно-телекоммуникационные системы», 2008 (http://www.ispras.ru/publications/2008/methods_of_software_verification/).

17. E. Clarke, O. Grumberg, S. Jha, Y. Lu, H. Veith. Counterexample-Guided Abstraction Refinement. Proceedings of CAV’2000, LNCS 1855:154-169, Springer-Verlag, 2000.

18. М. У. Мандрыкин, В. С. Мутилин, А. В. Хорошилов. Введение в метод CEGAR - уточнение абстракции по контрпримерам. Труды Института системного программирования РАН 24: 219-292, 2013. DOI: 10.15514/ISPRAS-2013-24-12

19. В. В. Кулямин, А. К. Петренко. Развитие подхода к разработке тестов UniTESK. Труды Института системного программирования РАН 26(1):9-26, 2014. DOI: 10.15514/ISPRAS-2014-26(1)-1

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

21. Е. М. Новиков. Развитие метода контрактных спецификаций для верификации модулей ядра операционной системы Linux. Диссертация на соискание ученой степени к.ф.-м.н., Москва, 2013.

22. И.С. Захаров, В.С. Мутилин, А.В. Хорошилов. “Моделирование окружения с использованием шаблонов для статической верификации модулей ядра Linux”. // Программирование, Том 41, 2015, №3, сс. 3-19.

23. P. N. Devyanin, A. V. Khoroshilov, V. V. Kuliamin, A. K. Petrenko, and I. V. Shchepetkov. Using Refinement in Formal Development of OS Security Model. Proceedings of PSI’2015.

24. П. Н. Девянин. Ролевая ДП-модель управления доступом и информационными потоками в операционных системах семейства Linux. ПДМ, 2012, № 1, 69-90.