计算机科学
計算機科學
계산궤과학
COMPUTER SCIENCE
2010年
12期
85-90
,共6页
安全操作系统%VMM%Haskell%Monad%形式化原型
安全操作繫統%VMM%Haskell%Monad%形式化原型
안전조작계통%VMM%Haskell%Monad%형식화원형
操作系统是计算机软件系统的基础,具有控制逻辑复杂、安全性和可靠性要求高等特点.在国内外高等级安全操作系统的规范和标准中,都提出了对内核进行形式化规范和验证的要求.近年来国内相关研究机构相继开发了满足GB 17859-1999"强制访问控制级"和"结构化保护级"的安全操作系统原型,但对更高级别的安全操作系统的研发尚属空白.在"面向访问验证保护级安全操作系统"课题的研究中,设计并实现了一个基于Haskell的安全VMM原型系统--CASVisor.CASVisor严格定义了系统的形式化规范,可用于指导高性能的C程序的实现,并为形式化的分析和验证打下基础,同时CASVisor具备模拟功能,以便实施基于快速原型的开发方法.
操作繫統是計算機軟件繫統的基礎,具有控製邏輯複雜、安全性和可靠性要求高等特點.在國內外高等級安全操作繫統的規範和標準中,都提齣瞭對內覈進行形式化規範和驗證的要求.近年來國內相關研究機構相繼開髮瞭滿足GB 17859-1999"彊製訪問控製級"和"結構化保護級"的安全操作繫統原型,但對更高級彆的安全操作繫統的研髮尚屬空白.在"麵嚮訪問驗證保護級安全操作繫統"課題的研究中,設計併實現瞭一箇基于Haskell的安全VMM原型繫統--CASVisor.CASVisor嚴格定義瞭繫統的形式化規範,可用于指導高性能的C程序的實現,併為形式化的分析和驗證打下基礎,同時CASVisor具備模擬功能,以便實施基于快速原型的開髮方法.
조작계통시계산궤연건계통적기출,구유공제라집복잡、안전성화가고성요구고등특점.재국내외고등급안전조작계통적규범화표준중,도제출료대내핵진행형식화규범화험증적요구.근년래국내상관연구궤구상계개발료만족GB 17859-1999"강제방문공제급"화"결구화보호급"적안전조작계통원형,단대경고급별적안전조작계통적연발상속공백.재"면향방문험증보호급안전조작계통"과제적연구중,설계병실현료일개기우Haskell적안전VMM원형계통--CASVisor.CASVisor엄격정의료계통적형식화규범,가용우지도고성능적C정서적실현,병위형식화적분석화험증타하기출,동시CASVisor구비모의공능,이편실시기우쾌속원형적개발방법.
