P.N. Devyanin

This article represents approaches to conclusion adequacy formal models of access control and their realization in computer systems. Scientific research of complex systems uses their modeling with statistical and experimentally methods frequently. But they use for adequacy of conclusion formal models of access control and information flows difficultly. It is the problem of modern computer security. This is problem of modern computer security. This article discusses approach of phased decision this problem. Kind of security model access control and information flows (for example, mandatory access control) choose at first step (with compliance goals of security). Formal model must be constructed at second step. Describe conditions and results of application rules transformation of states must be detailed within framework of formal model. Security conditions, with compliance goals of security, must be described later. For example, possibility of separation de-jure elements of formal models (which must be realize in real OS) and de-facto elements of formal models within framework of DP-model of access control and information flows in operating systems (OS) of Linux sets (ROSL DP-model) (which only used for theoretical analyzing of OS security, for example, for describe conditions of creation of illegal information flows) demonstrates. Conditions and results of application rules transformation of states must be transformed in definition specifications functions of access control in OS, at third step. Software of these functions suggests strong conclusion using methods, provided support for program correctness after this realization.