传统BLP模型的Z规范  

The Formalization of the BLP Security Model Using Z

作　　者：杨小明[1] 

机构地区：[1]湖州师范学院信息工程学院,浙江湖州313000

出　　处：《湖州师范学院学报》2007年第1期53-58,共6页Journal of Huzhou University

基　　金：湖州师范学院校级课题(200623)

摘　　要：安全模型是安全系统开发的基石,而形式化方法则为准确理解安全模型提供了高保障依据.形式语言Z对经典的多级安全模型BLP模型进行了规范描述,并验证了模型的正确性,为安全模型的形式化建模提供了方法和依据.The security model is the cornerstone for developing the security operating system, while the formal method provides high level assurance for the understanding of the security model accurately. The Z language is used to specify the classical MLS model, to testify the correctness of the model and to provide valuable method and ground for the formal specification of the security model.

关 键 词：安全模型 形式化方法 规范 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]