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/