Geodesic
About methods of developing consistent description of the MROSL DP-model for OS and DBMS for its verification with Rodin and ProB tools
Prikladnaya Diskretnaya Matematika. Supplement, no. 14 (2021), pp. 126-132.

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

Access control mechanism performs one of the main functions to ensure the security of information security tools, such as OS or DBMS. Formal models of access control are developed to achieve confidence in correctness of this mechanism, to create conditions for the scientific justification of its compliance with the security requirements. The paper presents methods of consistent description of the MROSL DP-model in the language used in mathematics (mathematical notation) and in Event-B formal method (formalized notation). The first result of using these methods in refining the formalized notation was provision the possibility of its joint verification by deductive method and method of model checking using the Rodin and ProB tools. The second result was modeling using Event-B formal method of interacting systems with their own developed access control mechanisms, such as OS and DBMS, which is necessary to match the description of the model in mathematical notation. These methods are formed on expression of the properties of the original hierarchical description of the model in mathematical notation in a sequential refinement of the model levels based on the refinement technique of Rodin and on application of total functions instead of directly using axiom of mathematical induction.
Keywords: formal model of access control, verification, assurance requirements, Astra Linux Special Edition. 
@article{PDMA_2021_14_a27,
     author = {P. N. Devyanin and M. A. Leonova},
     title = {About methods of developing consistent description of the {MROSL} {DP-model} for {OS} and {DBMS} for its verification with {Rodin} and {ProB} tools},
     journal = {Prikladnaya Diskretnaya Matematika. Supplement},
     pages = {126--132},
     publisher = {mathdoc},
     number = {14},
     year = {2021},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/PDMA_2021_14_a27/}
}
TY  - JOUR
AU  - P. N. Devyanin
AU  - M. A. Leonova
TI  - About methods of developing consistent description of the MROSL DP-model for OS and DBMS for its verification with Rodin and ProB tools
JO  - Prikladnaya Diskretnaya Matematika. Supplement
PY  - 2021
SP  - 126
EP  - 132
IS  - 14
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/PDMA_2021_14_a27/
LA  - ru
ID  - PDMA_2021_14_a27
ER  - 
%0 Journal Article
%A P. N. Devyanin
%A M. A. Leonova
%T About methods of developing consistent description of the MROSL DP-model for OS and DBMS for its verification with Rodin and ProB tools
%J Prikladnaya Diskretnaya Matematika. Supplement
%D 2021
%P 126-132
%N 14
%I mathdoc
%U http://geodesic.mathdoc.fr/item/PDMA_2021_14_a27/
%G ru
%F PDMA_2021_14_a27
P. N. Devyanin; M. A. Leonova. About methods of developing consistent description of the MROSL DP-model for OS and DBMS for its verification with Rodin and ProB tools. Prikladnaya Diskretnaya Matematika. Supplement, no. 14 (2021), pp. 126-132. http://geodesic.mathdoc.fr/item/PDMA_2021_14_a27/

[1] Bell D. E., LaPadula L.J., Secure Computer Systems: Unified Exposition and Multics Interpretation, MITRE Corp., Bedford, Mass., 1976

[2] Biba K. J., Integrity Considerations for Secure Computer Systems, MITRE Corp., Bedford, Mass., 1975

[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., Modeling in Event-B: System and Software Engineering, Cambridge University Press, 2010 | Zbl

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

[6] Vypiska iz Trebovanii po bezopasnosti informatsii, utverzhdennykh prikazom FSTEK Rossii No 76 ot 02.06.2020, https://fstec.ru/tekhnicheskaya-zashchita-informatsii/dokumenty-po-sertifikatsii/120-normativnye-dokumenty/2126-vypiska-iz-trebovanij-po-bezopasnosti-informatsii-utverzhdennykh-prikazom-fstek-rossii-ot-2-iyunya-2020-g-n-76

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

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

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

[10] 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., ed. P. N. Devyanin, Goryachaya liniya – Telekom, M., 2019, 404 pp.

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

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

[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

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

[15] 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 | Zbl