Methods for deductive verification of c code using AstraVer Toolset
Some practical methods for deductive verification of C code for compliance with ACSL specifications are described. For verification, Astraver Toolset based on the Frama-C platform is used. Approbation of these methods was carried out during the verification of access control module in PARSEC security subsystem of secure operating system Astra Linux Special Edition. For example, the method of global ghost variables allows monitoring shared memory, this is helpful for verification of certain functions. There is also a specification validation method that can help find out if the written specification is lacking. Thanks to these methods, it is possible to simplify function specifications, reduce labour intensity and speed up deductive verification. Examples of the use of the proposed methods are given.
Keywords
deductive software verification,
ACSL,
Frama-C,
AstraVer Toolset,
Astra LinuxAuthors
| Kokorin Artem O. | LLC "RusBITech-Astra" | akokorin@astralinux.ru |
| Tievskiy Stanislav D. | LLC "RusBITech-Astra" | stievskiy@astralinux.ru |
| Devyanin Petr N. | Academy of Cryptography of the Russian Federation; LLC "RusBITech-Astra" | pdevyanin@astralinux.ru |
Всего: 3
References
https://astralinux.ru/products/astra-linux-special-edition/- Операционная система специального назначения Astra Linux Special Edition. 2022.
Буренин П. В., Девянин П. Н., Лебеденко Е. В. и др. Безопасность операционной системы специального назначения Astra Linux Special Edition: учеб. пособие для вузов. 3-е изд., перераб. и доп. М.: Горячая линия - Телеком, 2019. 404 с.
Девянин П. Н. Модели безопасности компьютерных систем. Управление доступом и информационными потоками: учеб. пособие для вузов. 3-е изд., перераб. и доп. М.: Горячая линия - Телеком, 2020. 352 с.
Abrial J.-R., Butler M., Hallerstede S., et al. Rodin: An open toolset for modelling and reasoning in Event-B // Intern. J. Software Tools for Technology Transfer. 2010. V. 12. No. 6. P. 447-466.
Девянин П. Н., Ефремов Д. В., Кулямин В. В. и др. Моделирование и верификация политик безопасности управления доступом в операционных системах. М.: Горячая линия - Телеком, 2019. 214с.
Девянин П. Н., Леонова М. А. Приёмы по доработке описания модели управления доступом ОССН Astra Linux Special Edition на формализованном языке метода Event-B для обеспечения её автоматизированной верификации с применением инструментов Rodin и ProB // Прикладная дискретная математика. 2021. №52. С. 83-96.
https://fstec.ru/normotvorcheskaya/informatsionnye-i-analiticheskie-materialy/2171-informatsionnoe-soobshchenie-fstek-rossii-ot-10-fevralya-2021-g-n-240-24 -647. Информационное сообщение ФСТЭК России от 10.02.2021 № 240/24/647.
https://frama-c.com/html/acsl.html - ANSI/ISO C Specification Language. 2022.
https://www.ispras.ru/technologies/astraver_toolset/- Система верификации AstraVer Toolset. 2022.
Kirchner F., Kosmatov N., Prevosto V., et al. Frama-C: a software analysis perspective // Formal Aspects of Computing. 2015. No. 27(3). P. 573-609.
Filliatre J.-C. and Paskevich A. Why3 -where programs meet provers // LNCS. 2013. V. 7792. P. 125-128.
Marche C. and Moy Y. The Jessie Plugin for Deductive Verification in Frama-C. INRIA Saclay Ile-de-France and LRI, CNRS UMR, 2012.
Колисниченко Д. Н. Разработка Linux-приложений. СПб.: БХВ-Петербург, 2012. 432 с.
