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.