Specifying and building a formal secure Virtual Monitor Machine prototype
Hongliang Liang, Qiuping Yi, Shuo Tian · 2010 3rd IEEE International Conference on Broadband Network and Multimedia Technology (IC-BNMT) · 2010
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.