Quarterly journal published in SPbPU
and edited by prof. Peter Zegzhda
Peter the Great St. Petersburg Polytechnic University
Institute of computer sciences and technologies
information security of computer systems
Information Security Problems. Computer Systems
Published since 1999.
ISSN 2071-8217
Representing MROSL DP-model in Event-B notation

Devyanin P. N., Kuliamin V. V., Petrenko A. K., Khoroshilov A. V., Shchepetkov I. V.


The paper presents an approach of transforming the mandatory entity-role access control and information flow model for Linux-based operating system (MROSL DP-model) from human-readable mathematical representation to machine-readable Event-B notation. The transformation allows to prove consistency of the model and its properties using tools support that ensures correctness of the proofs and lack of omissions possible in manual reasoning about complex mathematical objects. Moreover, the formal model enables further specification and verification of its implementation in Astra Linux Special Edition using deductive verification techniques.

Keywords: Computer security, DP-model, operating system Astra Linux.
Pages 7-15