SPECIFYING AND BUILDING A FORMAL SECURE VIRTUAL MONITOR MACHINE PROTOTYPE

摘要：

To defend against growing security threats and attacks faced today, formal specification and verification of secure operating systems are important and almost a must for high assurance level certification. In this paper, we report the work of specifying and building a VMM-based security prototype SecBase, a system towards “verified design level of security standards in China. SecBase’s specification is formally defined, which can be used to guide high-performance C programs implementation, and support formal analysis and verification. Our experiments show that SecBase can quickly be developed and can provide well security separation, for the benefit of its formal specifications.

关键词： Virtualization Secure Operating System VMM Haskell Formal prototype

作者: Hongliang Liang Qiuping Yi Shuo Tian

作者单位: Beijing University of Posts and Telecommunications, Beijing, China State Key Laboratory of Computer State Key Laboratory of Computer Science, Institute of Software,Chinese Academy of Sciences, Beijing State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijin

会议类型: 国际会议

会议名称: 2010 3rd IEEE International Conference on Broadband Network & Multimedia Technology(2010年第三届IEEE宽带网络与多媒体国际会议 IC-BNMT 2010)

会议地点: 北京

会议语种:英文

页码: 916-920

在线出版日期: 2010-10-26（万方平台首次上网日期，不代表论文的发表时间）