Abstract:To satisfy the requirement of access verification protection level for secure operating system and development the next generation secure operating system with high security levels, we design and implement the Verification-oriented Secure Operating System prototype (VSOS) in microkernel architecture. VSOS meets the two of the principles of designing security kernel, which suggest that reference monitor must be tamper proof and always be involved, by designing and implementing the new reference monitor. However, the introducing of reference monitor causes great performance penalty on VSOS. In order to improve the performance of the VSOS, a code path-based optimization method is used to improve the way of implementing and calling reference monitor as well as implementation of the security mechanism such as trusted path. Experiment results demonstrate that both the performance and the user experience of VSOS are refined by using this method.