The purpose of research – development of a more advanced Windows NT family access control mechanism to protect against information leakage from memory by hidden channels. The method of research – analysis of Windows NT family models of mandatory access control and integrity control, modeling of access control security policy for specified security properties, automatic verification of models. The Lamport Temporal Logic of Actions (TLA +) used to describe the model and its specification is used. TLA+ allows automatic verification of the model with the specified security properties. The result of research – revealed the main limitations of the existing mandatory integrity control of operating systems of the Windows NT family. A set of structures of a multilevel model has been developed, reflecting the attributes that are significant for modeling the process of access of subjects to objects. The key mechanisms of access control in the operating system are modeled: management of users, groups, subjects, objects, roles, rights, discretionary and mandatory access control, mandatory integrity control - multilevel control of subjects’ access to objects. The model defines a mechanism for controlling the creation of subjects based on executable files to organize an isolated software environment. The values of the attributes of the model variables for the initialization stage are determined. The invariants of variables correctness in the process of verification and subjects to objects safe access are developed. The model was specified using the TLA + modeling language and verified.
Reducing Security Policy Size for Internet Servers in Secure Operating Systems