Model checking for inter-process communications of SELinux

摘要

Security Enhanced Linux (SELinux) is a high secure operating system. Inter-process communications is the most important aspect of operating system. The goal of this paper is to discuss and use Finite State Automaton to verify the security of IPC mechanisms of SELinux. At last, we use SPIN model checker to verify IPC mechanisms and give an improved method.