Формальная верификация библиотечных функций ядра Linux
https://doi.org/10.15514/ISPRAS-2017-29(6)-3
Аннотация
В статье авторами рассматриваются результаты дедуктивной верификации набора из 26 библиотечных функций ядра ОС Linux с помощью стека инструментов AstraVer. В набор включены преимущественно функции, работающие с данными строкового типа. Целью верификации является доказательство свойств функциональной корректности. В статье рассматриваются аналогичные работы по верификации, сравниваются полученные результаты, рассматривается ряд проблем, с которыми сталкивались авторы предыдущих работ, в том числе проблемы, с которыми удалось справится в рамках данной работы и те, которые все ещё препятствуют успешной верификации. Также предлагается методология разработки спецификаций, примененная для рассматриваемого набора функций, которая включает некоторые шаблонные приёмы разработки спецификаций. Авторам удалось доказать полную корректность двадцати пяти функций. В статье приведены результаты доказательства полученных условий верификации каждой функции с помощью нескольких современных SMT-солверов.
Об авторах
Д. В. Ефремов
НИУ Высшая школа экономики
Россия
Россия
М. У. Мандрыкин
Институт системного программирования им. В.П. Иванникова РАН
Россия
Россия
Список литературы
1. MISRA C: 2012. Guidelines for the Use of the C Language in Critical Systems, ISBN 978-1-906400-10-1 (paperback), ISBN 978-1-906400-11-8 (PDF), March 2013.
2. AstraVer Toolset: инструменты дедуктивной верификации моделей и механизмов защиты ОС. ИСП РАН. Доступно по ссылке: http://linuxtesting.org/astraver, 15.10.2017.
3. Мандрыкин М.У., Хорошилов А.В. Высокоуровневая модель памяти промежуточного языка Jessie с поддержкой произвольного приведения типов указателей. Программирование, 2015, т. 41, №4, стр. 23–29.
4. Мандрыкин М.У., Хорошилов А.В. Анализ регионов для дедуктивной верификации Си-программ. Программирование. 2016, т. 42, № 5, стр. 3–29.
5. Carvalho N., Silva Sousa C., Pinto J.S., Tomb A. Formal verification of kLIBC with the WP frama-C plug-in. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 343–358. Springer, Heidelberg (2014)
6. Torlakcik M. Contracts in OpenBSD. MSc thesis. University College Dublin. April, 2010.
7. Efremov D., Mandrykin M. VerKer: Verification of Linux Kernel Library Functions. Доступно по ссылке: http://forge.ispras.ru/projects/verker, 15.10.2017.
8. Cuoq P., Kirchner F., Kosmatov N., Prevosto V., Signoles J., Yakobowski B. Frama-C: A Software Analysis Perspective. Proceedings of the 10th International Conference on Software Engineering and Formal Methods. SEFM'12. Thessaloniki, Greece. 2012. Lecture Notes in Computer Science, vol. 7504, pp. 233–247. Springer-Verlag. Berlin, Heidelberg. 2012.
9. Baudin P., Cuoq P., Filliâtre J., Marché C., Monate B., Moy Y., Prevosto V. ACSL: ANSI/ISO C Specification Language. Version 1.12. CEA LIST and INRIA. May, 2017. Доступно по ссылке: https://frama-c.com/download/acsl_1.12.pdf, 15.10.2017.
10. Moy Y. Automatic Modular Static Safety Checking for C Programs. PhD thesis. Université Paris-Sud. January, 2009.
11. Filliâtre J., Paskevich A. Why3: Where Programs Meet Provers. Proceedings of the 22Nd European Conference on Programming Languages and Systems. ESOP'13. Rome, Italy. LNCS, vol. 7792, pp. 125–128. Springer-Verlag.
12. Burghardt J., Clausecker R., Gerlach J., Pohl H. ACSL By Example: Towards a Verified C Standard Library. Version 15.1.1. Доступно по ссылке: https://github.com/fraunhoferfokus/acsl-by-example/raw/master/ACSL-by-Example.pdf, 15.10.2017.
13. Cok D., Blissard I., Robbins J. C Library annotations in ACSL for Frama-C: experience report. GrammaTech, Inc. March, 2017. Доступно по ссылке: http://annotationsforall.org/resources/links/GT-libc-experience-report.pdf, 15.10.2017.
14. Hatcliff J., Leavens G. T., Leino K. R. M., Müller P., Parkinson M. Behavioral interface specification languages. ACM Comput. Surv. vol. 44, issue 3, article 16, 58 p. June 2012.
15. ISO/IEC 9899: 2011: C11 standard for C programming language. JTC and ISO. April 7, 2016.
16. Hubert T., Marché C. Separation Analysis for Deductive Verification. Heap Analysis and Verification (HAV'07). Braga, Portugal, March 2007, pp. 81–93.
17. Moy Y. Union and Cast in Deductive Verification. Proceedings of the C/C++ Verification Workshop. Technical Report ICIS-R07015, pp. 1–16. Radboud University Nijmegen. July, 2007.
18. Signoles J. E-ACSL Executable ANSI/ISO C Specification Language. Version 1.12. CEA LIST. May, 2017. Доступно по ссылке: https://frama-c.com/download/e-acsl/e-acsl.pdf, 15.10.2017.
19. Marché C. [Frama-c-discuss] Frama-C/WP and CVC4 (version 1.5). Доступно по ссылке: https://lists.gforge.inria.fr/pipermail/frama-c-discuss/2017-August/005338.html, 15.10.2017.
Рецензия
Для цитирования:
Ефремов Д.В., Мандрыкин М.У. Формальная верификация библиотечных функций ядра Linux. Труды Института системного программирования РАН. 2017;29(6):49-76. https://doi.org/10.15514/ISPRAS-2017-29(6)-3
For citation:
Efremov D.V., Mandrykin M.U. Formal Verification of Linux Kernel Library Functions. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2017;29(6):49-76. (In Russ.) https://doi.org/10.15514/ISPRAS-2017-29(6)-3
Послать статью по эл. почте 