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/