| 安全计算机系统的Bell—LaPadula形式化模型 |
| |
| 引用本文： | 王贵林,卿斯汉,等.安全计算机系统的Bell—LaPadula形式化模型[J].计算机科学,2001,28(12):89-92. |
| |
| 作者姓名： | 王贵林 卿斯汉 |
| |
| 作者单位： | 中国科学院软件研究所 |
| |
| 基金项目： | 国家自然科学基金跨学科重点项目(No. 19931010)，国家973高科技项目基金(No.G1999035810、G1999035802) |
| |
| 摘 要： | 一、引言著名的Bell-LaPadula形式化模型(简称为BLP模型)是由MITRE公司的Bell和LaPadula在文中提出的,随后被广泛用于形式化地描述和证明计算机系统的安全。文给出了信息保密系统的Bell-LaPadula模型的形式化描述,并证明了几个结论。其中一个重要的结论就是,判断信息系统是否为保密系统的充分必要条件。但我们发现,该结论的证明是错误的。事实上,文给出的只是一个充分条件,而不是必要条件。另外,文将Bell-LaPadula作了修改和扩充,得到了一个新的修改BLP模型,并成功地将修改后的模型用于设计SecLinux安全操作系统。但文并没有给出修改BLP模型的形式化证明。借助于一个新的概念-动作(action),我们给出了在Bell-LaPadula形式化模型下,计算机系统安全的充分必要条件。同时,本文还对Bell-LaPadula形式化模
|
| 关 键 词： | 计算机系统 安全 Bell－LaPadula形成化模型 信息安全 |
The Bell-LaPadula Formal Model for Secure Computer Systems |
| |
| Abstract: | |
| |
| Keywords: | |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
点击此处可从《计算机科学》下载全文 |
|
