Geodesic
Comparison of methods for modeling access control in OS and DBMS in Event-B for the purpose of their verification with Rodin and ProB tools
Prikladnaya Diskretnaya Matematika. Supplement, no. 15 (2022), pp. 90-99.

Voir la notice de l'article provenant de la source Math-Net.Ru

The paper presents two methods of modeling interacting systems with developed access control mechanisms, such as OS and DBMS. These methods are the result of translating the description of the formal access control model of Astra Linux Special Edition OS (MROSL DP-model) from mathematical to formalized notation using the formal Event-B method, as well as its automatic verification using Rodin and ProB tools. The considered methods are based on the use of various options for constructing a hierarchy of specifications of the MROSL DP-model in the formalized notation using the technique “refinement”. We compare these methods showing their advantages and disadvantages. They consist in the complexity of writing specifications, the need to repeat proofs during the verification with the Rodin tool, the possibility of eliminating the effect of “combinatorial explosion” during the verification with the ProB tool. Based on the results of the comparison, it is concluded that considered methods can be useful in the development of other formal access control models and their verification using appropriate tools.
Keywords: formal access control model, Event-B, verification, deductive verification, Rodin, model checking, ProB. 
@article{PDMA_2022_15_a21,
     author = {M. A. Leonova and P. N. Devyanin},
     title = {Comparison of methods for modeling access control in {OS} and {DBMS} in {Event-B} for the purpose of their verification with {Rodin} and {ProB} tools},
     journal = {Prikladnaya Diskretnaya Matematika. Supplement},
     pages = {90--99},
     publisher = {mathdoc},
     number = {15},
     year = {2022},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/PDMA_2022_15_a21/}
}
TY  - JOUR
AU  - M. A. Leonova
AU  - P. N. Devyanin
TI  - Comparison of methods for modeling access control in OS and DBMS in Event-B for the purpose of their verification with Rodin and ProB tools
JO  - Prikladnaya Diskretnaya Matematika. Supplement
PY  - 2022
SP  - 90
EP  - 99
IS  - 15
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/PDMA_2022_15_a21/
LA  - ru
ID  - PDMA_2022_15_a21
ER  - 
%0 Journal Article
%A M. A. Leonova
%A P. N. Devyanin
%T Comparison of methods for modeling access control in OS and DBMS in Event-B for the purpose of their verification with Rodin and ProB tools
%J Prikladnaya Diskretnaya Matematika. Supplement
%D 2022
%P 90-99
%N 15
%I mathdoc
%U http://geodesic.mathdoc.fr/item/PDMA_2022_15_a21/
%G ru
%F PDMA_2022_15_a21
M. A. Leonova; P. N. Devyanin. Comparison of methods for modeling access control in OS and DBMS in Event-B for the purpose of their verification with Rodin and ProB tools. Prikladnaya Diskretnaya Matematika. Supplement, no. 15 (2022), pp. 90-99. http://geodesic.mathdoc.fr/item/PDMA_2022_15_a21/

[1] GOST R 59453.1-2021 «Zaschita informatsii. Formalnaya model upravleniya dostupom. Ch. 1. Obschie polozheniya», Standartinform, M., 2021, 16 pp.

[2] 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.

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

[4] 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.

[5] Abrial J.-R., Modeling in Event-B: System and Software Engineering, Cambridge University Press, 2010 | Zbl

[6] 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.

[7] Devyanin P. N., Leonova M. A., “Primenenie podtipov i totalnykh funktsii formalnogo metoda Event-B dlya opisaniya i verifikatsii MROSL DP-modeli”, Programmnaya inzheneriya, 11:4 (2020), 230–241

[8] GOST R 59453.2-2021 «Zaschita informatsii. Formalnaya model upravleniya dostupom. Ch. 2. Rekomendatsii po verifikatsiya formalnoi modeli upravleniya dostupom», Standartinform, M., 2021, 12 pp.

[9] 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

[10] Devyanin P. N., Telezhnikov V. Yu., Khoroshilov A. V., “Formirovanie metodologii razrabotki bezopasnogo sistemnogo programmnogo obespecheniya na primere operatsionnykh sistem”, Trudy ISP RAN, 33:5 (2021), 25–40

[11] Leuschel M. and Butler M., “ProB: an automated analysis toolset for the B method”, Int. J. Softw. Tools Technol. Transf., 10:2 (2008), 185–203 | DOI

[12] 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

[13] Abrial J.-R. and Hallerstede S., “Refinement, decomposition, and instantiation of discrete models: Application to Event-B”, Fundamenta Informaticae, 77:1–2 (2007), 1–28 | MR | Zbl