Formal verification of a mandatory integrity control model for the KasperskyOS operating system

Models of mandatory integrity control in operating systems usually restrict accesses of active components of a system to passive ones and represent the accesses directly. This is suitable in case of monolithic operating systems whose components that provide access to resources are part of the trusted computing base. However, due to the sheer complexity of such components, it is extremely nontrivial to prove such a model to be adequate to the real system. KasperskyOS is a microkernel operating system that organizes access to resources via components that are not necessarily part of the trusted computing base. KasperskyOS implements a specifically developed mandatory integrity control model that takes such components into account. This paper formalizes the model and describes the process of automated proof of the model's properties. For formalization, we use the Event-B language. We clarify parts specific to Event-B to make our presentation accessible to professionals familiar with discrete mathematics but not necessarily with Event-B. We reflect on the proof experience obtained in the Rodin platform.