Among other things, a separation kernel can be used to ensure the security of a computer system. This is a specialized operating system that
ensures the division of system resources into separate domains and complete
separation between them. In this master’s thesis, we formalize a separation
kernel model using a proof assistant. First, we select a proof assistant. The
selection process includes a theoretical review of some of the most commonly
used proof assistants and the implementation of an experiment in the Rocq
and Isabelle languages. The results are evaluated and Rocq is selected for
the formalization of the separation kernel. The formalization includes the
specification of kernel properties, the specification of security properties, and
the proof of these security properties for the defined kernel. This procedure
ensures the correct function of the kernel.
|
