%0 Journal Article
%T The Bell-LaPadula Formal Model for Secure Computer Systems<br>安全计算机系统的Bell—LaPadula形式化模型
%A 王贵林
%A 卿斯汉
%J 计算机科学
%D 2001
%I 
%X 一、引言著名的Bell-LaPadula形式化模型(简称为BLP模型)是由MITRE公司的Bell和LaPadula在文中提出的,随后被广泛用于形式化地描述和证明计算机系统的安全。文给出了信息保密系统的Bell-LaPadula模型的形式化描述,并证明了几个结论。其中一个重要的结论就是,判断信息系统是否为保密系统的充分必要条件。但我们发现,该结论的证明是错误的。事实上,文给出的只是一个充分条件,而不是必要条件。另外,文将Bell-LaPadula作了修改和扩充,得到了一个新的修改BLP模型,并成功地将修改后的模型用于设计SecLinux安全操作系统。但文并没有给出修改BLP模型的形式化证明。借助于一个新的概念-动作(action),我们给出了在Bell-LaPadula形式化模型下,计算机系统安全的充分必要条件。同时,本文还对Bell-LaPadula形式化模
%K 计算机系统
%K 安全
%K Bell－LaPadula形成化模型
%K 信息安全
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=64A12D73428C8B8DBFB978D04DFEB3C1&aid=359C8B894EE17BA2&yid=14E7EF987E4155E6&vid=D3E34374A0D77D7F&iid=59906B3B2830C2C5&sid=CFAC5CB624A41AFD&eid=08805F9252973BA4&journal_id=1002-137X&journal_name=计算机科学&referenced_num=3&reference_num=12