%0 Journal Article
%T Formal Secure VMM Prototype Towards Level Verified Design<br>面向访问验证保护级的安全VMM形式化原型系统设计和实现
%A YI Qiu-ping
%A LIU Jian
%A WU Shu
%A <br>易秋萍
%A 刘剑
%A 武术
%J 计算机科学
%D 2010
%I 
%X 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.
%K Secure operating system
%K VMM
%K Haskell
%K Monad
%K Formal prototype<br>安全操作系统，VMM
%K Haskell
%K Monad，形式化原型
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=64A12D73428C8B8DBFB978D04DFEB3C1&aid=1C7EC8CB23A53F5685AA640ED1704867&yid=140ECF96957D60B2&vid=42425781F0B1C26E&iid=59906B3B2830C2C5&sid=CD775AE9DDBD7B53&eid=869807E2D7BED9EC&journal_id=1002-137X&journal_name=计算机科学&referenced_num=0&reference_num=0