Geodesic
The techniques of formalization of OS Astra Linux Special Edition access control model using Event-B formal method for verification using Rodin and ProB
Prikladnaâ diskretnaâ matematika, no. 2 (2021), pp. 83-96.

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

The paper presents techniques to specification access control model of OS Astra Linux Special Edition (the MROSL DP-model) in the formalized notation (formalized using the Event-B formal method), that are based on the use of several global types, separation of general total functions into specific total functions, reduction in the number of invariants and guard of events, which iterate over subsets of a certain set. The result of using these techniques was the simplification of automated deductive verification of formalized notation using the Rodin tool and adaptation of the model to verification by model checking formalized notation using the ProB tool. These techniques can be useful in development of the MROSL DP-model, and also in development of other access control models and verification using appropriate tools.
Keywords: access control model, deductive verification, Event-B, Rodin, model checking, ProB. 
@article{PDM_2021_2_a4,
     author = {P. N. Devyanin and M. A. Leonova},
     title = {The techniques of formalization of {OS} {Astra} {Linux} {Special} {Edition} access control model using {Event-B} formal method for verification using {Rodin} and {ProB}},
     journal = {Prikladna\^a diskretna\^a matematika},
     pages = {83--96},
     publisher = {mathdoc},
     number = {2},
     year = {2021},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/PDM_2021_2_a4/}
}
TY  - JOUR
AU  - P. N. Devyanin
AU  - M. A. Leonova
TI  - The techniques of formalization of OS Astra Linux Special Edition access control model using Event-B formal method for verification using Rodin and ProB
JO  - Prikladnaâ diskretnaâ matematika
PY  - 2021
SP  - 83
EP  - 96
IS  - 2
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/PDM_2021_2_a4/
LA  - ru
ID  - PDM_2021_2_a4
ER  - 
%0 Journal Article
%A P. N. Devyanin
%A M. A. Leonova
%T The techniques of formalization of OS Astra Linux Special Edition access control model using Event-B formal method for verification using Rodin and ProB
%J Prikladnaâ diskretnaâ matematika
%D 2021
%P 83-96
%N 2
%I mathdoc
%U http://geodesic.mathdoc.fr/item/PDM_2021_2_a4/
%G ru
%F PDM_2021_2_a4
P. N. Devyanin; M. A. Leonova. The techniques of formalization of OS Astra Linux Special Edition access control model using Event-B formal method for verification using Rodin and ProB. Prikladnaâ diskretnaâ matematika, no. 2 (2021), pp. 83-96. http://geodesic.mathdoc.fr/item/PDM_2021_2_a4/

[1] OS Astra Linux Special Edition, 2020

[2] Burenin P. V., Devyanin P. N., Lebedenko E. V., et al., Security of Operating System Astra Linux Special Edition, Goryachaya liniya — Telekom, M., 2019, 404 pp. (in Russian)

[3] Information message of FSTEC Russia dated 15.10.2020 No 240/24/4268

[4] Devyanin P. N., The Models of Security of Computer Systems: Access Control and Information Flows, Goryachaya liniya — Telekom, M., 2020, 352 pp. (in Russian)

[5] Devyanin P. N., Khoroshilov A. V., Kuliamin V. V., et al., “Integrating RBAC, MIC, and MLS in verified hierarchical security model for operating system”, Program. Comput. Soft., 46 (2020), 443–453

[6] Abrial J.-R., Modeling in Event-B: System and Software Engineering, 2010

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

[8] Devyanin P. N., Efremov D. V., Kuliamin V. V., et al., Modeling and Verification Access Control Security Policies on Operating Systems, Goryachaya liniya — Telekom, M., 2019, 214 pp. (in Russian)

[9] Devyanin P. N., “The level of negative roles of the hierarchical representation of MROSL DP-model”, Prikladnaya Diskretnaya Matematika, 2018, no. 39, 58–71 (in Russian)

[10] Devyanin P. N., “Approaches to formal modeling of access control in PostgreSQL within framework of the MROSL DP-model”, Prikladnaya Diskretnaya Matematika. Prilozhenie, 2018, no. 11, 95–98 (in Russian)

[11] Devyanin P. N., “About results of design hierarchical representation of MROSL DP-model”, Prikladnaya Diskretnaya Matematika. Prilozhenie, 2016, no. 9, 83–87 (in Russian)

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

[13] Devyanin P. N., Leonova M. A., “Application of subtypes and total functions of Event-B formal method for the formalization and verification of the MROSL DP-model”, Programmnaya Ingeneria, 11:4 (2020), 230–241 (in Russian)

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