Abstract: Operation systems are the base of computer software system which have complex controlling logics, and their security and reliability arc very critical. In almost all of standards of security operating system in the world, formal specification and verification on them are needed. Inrecent years, several system meeting level "mandatory access control" and "structural protection" in GB 17859-1999 were designed and implemented by domestic research agencies. However,systems conformed to higher levcles arc still in blank. In this paper, we reported a VMM-based security prototypcCASVisor,a system towards "level verified design",which is designed and implemented in our group. CASVisor has formal definition of the system specification, which can be used to guide high-performance implementation in C programs, and support formal analysis and verification. Moreover,CASVisor can be used as rapid prototype to simulate the system design.

Key words: Secure operating system, VMM, Haskell, Monad, Formal prototype