A mandatory integrity control model for the KasperskyOS operating system

Existing models of mandatory integrity control in operating systems restrict accesses of active components of a system to passive ones and represent the accesses directly: subjects get read or write access to objects. Such a representation can be used in modeling of monolithic operating systems whose components that provide access to resources are part of the trusted computing base. However, the implementation of these components is extremely complex. Therefore, it is arduous to prove the absence of bugs (vulnerabilities) in them. In other words, proving such a model to be adequate to the real system is nontrivial and often left unsolved. This article presents a mandatory integrity control model for a microkernel operating system called KasperskyOS. Microkernel organization of the system allows us to minimize the trusted computing base to include only the microkernel and a limited number of other components. Parts of the system that provide resource access are generally considered untrusted. Even if some of them are erroneous, the operating system can still provide particular security guarantees. To prove that by means of a model, we introduce the notion of object drivers as intermediaries in operations on objects. We define the requirements that object drivers must satisfy. We also add the means for analysis of the consequences of violations of the requirements. We state and prove that the model either preserves integrity if all active components satisfy the requirements, or restricts the negative impact if some of the components are compromised. Correct implementation of the model guarantees that compromised components will not affect components with higher or incomparable integrity levels. We describe a policy specification language developed in accordance with the model. We provide an example of using it to describe a security policy that ensures a correct update of a system operated by KasperskyOS.