Geodesic
Methods for deductive verification of C code using AstraVer Toolset
Prikladnaya Diskretnaya Matematika. Supplement, no. 15 (2022), pp. 80-90 Cet article a éte moissonné depuis la source Math-Net.Ru

Voir la notice de l'article

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, AstraVer Toolset
Mots-clés : ACSL, Frama-C, Astra Linux. 
@article{PDMA_2022_15_a20,
     author = {A. O. Kokorin and S. D. Tievskiy and P. N. Devyanin},
     title = {Methods for deductive verification of {C} code using {AstraVer} {Toolset}},
     journal = {Prikladnaya Diskretnaya Matematika. Supplement},
     pages = {80--90},
     year = {2022},
     number = {15},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/PDMA_2022_15_a20/}
}
TY  - JOUR
AU  - A. O. Kokorin
AU  - S. D. Tievskiy
AU  - P. N. Devyanin
TI  - Methods for deductive verification of C code using AstraVer Toolset
JO  - Prikladnaya Diskretnaya Matematika. Supplement
PY  - 2022
SP  - 80
EP  - 90
IS  - 15
UR  - http://geodesic.mathdoc.fr/item/PDMA_2022_15_a20/
LA  - ru
ID  - PDMA_2022_15_a20
ER  - 
%0 Journal Article
%A A. O. Kokorin
%A S. D. Tievskiy
%A P. N. Devyanin
%T Methods for deductive verification of C code using AstraVer Toolset
%J Prikladnaya Diskretnaya Matematika. Supplement
%D 2022
%P 80-90
%N 15
%U http://geodesic.mathdoc.fr/item/PDMA_2022_15_a20/
%G ru
%F PDMA_2022_15_a20
A. O. Kokorin; S. D. Tievskiy; P. N. Devyanin. Methods for deductive verification of C code using AstraVer Toolset. Prikladnaya Diskretnaya Matematika. Supplement, no. 15 (2022), pp. 80-90. http://geodesic.mathdoc.fr/item/PDMA_2022_15_a20/

[1] Operatsionnaya sistema spetsialnogo naznacheniya Astra Linux Special Edition, , 2022 https://astralinux.ru/products/astra-linux-special-edition/

[2] Burenin P. V., Devyanin P. N., Lebedenko E. V. i dr., Bezopasnost operatsionnoi sistemy spetsialnogo naznacheniya Astra Linux Special Edition, ucheb. posobie dlya vuzov, 3-e izd., pererab. i dop., Goryachaya liniya — Telekom, M., 2019, 404 pp.

[3] Devyanin P. N., Modeli bezopasnosti kompyuternykh sistem. Upravlenie dostupom i informatsionnymi potokami, ucheb. posobie dlya vuzov, 3-e izd., pererab. i dop., Goryachaya liniya — Telekom, M., 2020, 352 pp.

[4] 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, 12:6 (2010), 447–466 | DOI

[5] Devyanin P. N., Efremov D. V., Kulyamin V. V. i dr., Modelirovanie i verifikatsiya politik bezopasnosti upravleniya dostupom v operatsionnykh sistemakh, Goryachaya liniya — Telekom, M., 2019, 214 pp.

[6] Devyanin P. N., Leonova M. A., “Priemy po dorabotke opisaniya modeli upravleniya dostupom OSSN Astra Linux Special Edition na formalizovannom yazyke metoda {Event-B} dlya obespecheniya ee avtomatizirovannoi verifikatsii s primeneniem instrumentov Rodin i ProB”, Prikladnaya diskretnaya matematika, 2021, no. 52, 83–96 | MR | Zbl

[7] Informatsionnoe soobschenie FSTEK Rossii ot 10.02.2021 No 240/24/647, https://fstec.ru/normotvorcheskaya/informatsionnye-i-analiticheskie-materialy/2171-informatsionnoe-soobshchenie-fstek-rossii-ot-10-fevralya-2021-g-n-240-24-647

[8] ANSI/ISO C Specification Language, , 2022 https://frama-c.com/html/acsl.html

[9] Sistema verifikatsii AstraVer Toolset, , 2022 https://www.ispras.ru/technologies/astraver_toolset/

[10] Kirchner F., Kosmatov N., Prevosto V., et al., “Frama-C: a software analysis perspective”, Formal Aspects of Computing, 27:3 (2015), 573–609 | DOI | MR

[11] Filliatre J.-C. and Paskevich A., “Why3 — where programs meet provers”, LNCS, 7792, 2013, 125–128 | Zbl

[12] Marche C. and Moy Y., The Jessie Plugin for Deductive Verification in Frama-C, INRIA Saclay Ile-de-France and LRI, CNRS UMR, 2012

[13] Kolisnichenko D. N., Razrabotka Linux-prilozhenii, BKhV-Peterburg, SPb., 2012, 432 pp.