Preview

Труды Института системного программирования РАН

Расширенный поиск

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

https://doi.org/10.15514/ISPRAS-2015-27(5)-10

Полный текст:

Аннотация

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

Об авторах

А. К. Петренко
ИСП РАН; МГУ им. М. В. Ломоносова; Московский физико-технический институт (государственный университет); НИУ ВШЭ
Россия


В. В. Кулямин
ИСП РАН; МГУ им. М. В. Ломоносова; НИУ ВШЭ
Россия


А. В. Хорошилов
ИСП РАН; МГУ им. М. В. Ломоносова; Московский физико-технический институт (государственный университет); НИУ ВШЭ
Россия


Список литературы

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.


Для цитирования:


Петренко А.К., Кулямин В.В., Хорошилов А.В. Об интеграции формальных методов в задачах верификации операционных систем. Труды Института системного программирования РАН. 2015;27(5):175-190. https://doi.org/10.15514/ISPRAS-2015-27(5)-10

For citation:


Petrenko A.K., Kuliamin V.V., Khoroshilov A.V. Integration Points of Operating System Verification Techniques. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2015;27(5):175-190. (In Russ.) https://doi.org/10.15514/ISPRAS-2015-27(5)-10

Просмотров: 16


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 2079-8156 (Print)
ISSN 2220-6426 (Online)