开发设计一个安全的操作系统，首先要明确安全需求，一般来说，操作系统的安全需求可以归纳为四个方面：机密性（confidentiality）、完整性（integrity）、可追究性（accountability）和可用性（availability）。上述安全需求转化为一系列的安全策略，比如访问控制策略（ACP）和访问支持策略（ASP），前者反应系统的机密性和完整性需求，后者反应系统的可追究性和可用性需求。我们说一个系统是安全的，并非指该系统就是绝对安全，而是说这个系统的实现达到了当初设计时所制定的安全策略。
为了进一步设计我们的安全操作系统，我们还需要将安全需求、安全策略抽象为安全模型。安全模型是对安全策略所表达的安全需求的简单、抽象和无歧义的描述，它为安全策略关联上对应的实现机制，从而为开发安全系统提供方针，即安全模型描述了对于某个安全策略需要使用什么样的机制来实现，模型的实现则描述了如何把特定的机制应用于实际的系统当中。安全模型除了具备精确无歧义、简易抽象、容易理解的特点之外，还具有一般性，即安全模型只是关注安全相关的问题，不过度涉及系统的功能和实现。
安全模型可以分为形式化和形式化两种安全模型。非形式化模型仅模拟系统的安全功能，形式化安全模型则借助数学模型，精确地描述安全性及其在系统中使用的情况。J.P.Anderson曾指出，开发安全系统首先必须建立系统的安全模型，完成安全系统的建模之后，再进行安全内核的设计和实现。一般高等级安全操作系统开发时都要求使用形式化安全模型来模拟安全系统，因为形式化模型可以正确地综合系统的各类因素，如系统的使用方式、使用环境类型、授权的定义、共享的客体资源等，所有这些因素构成安全系统的形式化抽象描述，使得系统可以被证明是完整的、反映真实环境的、逻辑上能够实现程序可以受控执行的。
上面简单地介绍了安全需求—-安全策略—-安全模型的基本知识，介绍了形式化安全模型的优势，接下来，我们来具体看几个安全模型，加深对于安全模型的了解和认识。
一、机密性安全模型：BLP
之所以叫机密性模型，自己的理解是BLP主要关注的是信息的机密性，即信息不能由高安全等级流向低安全等级，一句话来概括BLP就是“下读上写”，什么意思？不着急，等我慢慢道来。
BLP模型是由D.Elliott Bell和Leonard J. LaPadula于1973年提出的一种适用于军事安全策略的计算机操作系统安全模型，它是最早、也是最常用的一种计算机多级安全模型之一。BLP将主体定义为能够发起行为的实体，如进程；将客体定义为被动的主体行为承担者，如数据、文件等；将主体对客体的访问分为r-只读、w-读写、a-只写、e-执行与c-控制等访问模式，其中c-控制是用来描述该主体用来授予或者撤销另一主体对某一个个客体的访问权限的能力。BLP的安全策略包括两个部分：自主安全策略和强制安全策略。自主安全策略借助访问矩阵实现，强制安全策略包括简单安全特性和*特性，系统对所有的主体和客体都分配一个访问类属性，包括密级和范畴，系统通过比较主体和客体的访问类属性来控制主体对客体的访问。
BLP的几个重要公理
1.公理，就是理所应当承认成立的判断。BLP主要有以下几个：
(1). 简单安全性
我们说一个状态v=(b, M, f, H)满足简单安全性，iff
任意的主体s(属于主体集合S)，若s对客体o(属于客体集合O)有读写权限，那么主体s的安全级一定支配客体o的安全级，这里的安全级支配意思是指主体的密级L(s) > 客体的密级L(o)，并且s的范畴Domain(s)包含o的范畴Domain(o)，一句话说就是显而易见的道理：A可以对B读写，那么A的安全级一定高于B（强制安全策略体现）。
(2). *特性
这类似一个分段函数，分情况来说就是，对于状态v=(b, M, f, H)满足相对于S子集S1的*特性，iff
任意属于S1的s，都有：
若s对于o只有只写权限，那么o的安全级支配s的安全级，即客体安全级高于主体安全级；
若s对于o有读写权限，那么客体o的安全级等于主体s的安全级；
若s对于o只有只读权限，那么主体s的安全级支配客体o的安全级；
看到了吧，其实BLP就是“下读上写”:信息只能由高等级读低等级，写操作可以由低等级到高等级，可读可写一定安全级相同
(3). 自主安全性：
若主体s可以对于客体o有访问属性A(r/w/a/c)，则该访问属性一定满足访问矩阵M(i)(j)。
(4). 兼容性公理：
对于客体o，如果o是O-1的叶节点，则叶结点的安全级支配O-1的安全级。
BLP模型的分析
从上面的介绍可以看出，BLP模型的安全策略包括强制存取控制和自主存取控制两部分，前者由简单安全性和特性组成（安全级），通过安全级强制性约束主体对客体的存取；自主存取控制通过存取控制矩阵按用户的意愿进行存取控制。虽然BLP在建立安全系统的活动中一直占据主导地位，但是严格实施BLP模型的系统往往是不实际的。这是因为真实的系统中，用户可能会违背特性，但是并不会违背系统的安全性。比如特性规定只能由高安全等级读取低安全等级，但是一个用户可能需要读取机密文件中的非机密信息，并且应用到另一份非机密文件中。因此为了增加系统的可用性，BLP模型添加了一类可信主体，这些主体是可信的，当且仅当他们可以违背特性，但是不能违背系统的安全性。
BLP模型的不足：
(1). BLP模型中，可信主体不受*特性约束，访问权限太大，不符合最小特权原则，应对可信主体的操作权限和应用范围进一步细化；
(2). BLP模型注重保密性控制，控制信息从高安全级传向低安全级，但是却缺少完整性控制，不能控制“上写”操作，可能导致隐蔽通道；因此大多数基于BLP模型实现的多级安全系统，规定只能向具有和主体安全级相同的客体写入信息，对BLP模型进行了修改。
(3). BLP模型使用了与可信主体相关的安全规则，导致很难确定系统执行的安全规则到底是哪个；
(4). BLP仅处理单极客体，缺乏处理多级客体（如磁盘）；
(5). 没有支持应用相关的安全规则；
二、完整性安全模型：Biba模型
这部分我们来介绍下完整性安全模型，BLP模型注重了机密性，但是忽略了完整性保护，于是后人对BLP模型进行了一些改进。1977年Biba等人提出了第一个完整性安全模型——Biba模型，主要应用类似BLP模型的规则来保护信息的完整性。Biba模型提出的不是一个唯一的安全策略，而是一个安全策略系列。比如非自主安全策略里的对于主体/客体的下限标记策略，使得主体、客体的完整级别动态变化；自主安全策略里的ACL和环机制等等，这里不再详述，有兴趣的童鞋可以去度娘谷歌。
Biba模型的优势在于其简单性以及和BLP模型相结合的可能性。简单性体现在Biba的严格完整性策略师BLP机密性策略的对偶，所以它的实现是直观和易于理解的；基于Biba和BLP的相似性，二者有可能结合产生机密性完整性一身的安全模型。但是其不足是：1. 完整性标签确定的困难性；2. Biba模型最主要的完整性目的是用于保护数据免受非授权用户的恶意修改，同时其认为内部完整性威胁应该通过程序验证来解决，但是在模型中并没有包括这个要求；3. Biba和BLP模型的结合看似容易，实则困难，而且即使结合之后，也无法低于病毒攻击。
三、完整性安全模型：Clark-Wilson完整性模型
1987年David Clark和David wilson提出的完整性模型具有里程碑意义，它是完整意义上的完整性目标、策略和机制的起源。为了体现用户完整性，CW模型提出了职责隔离目标；为了保证数据完整性，CW模型提出了应用相关的完整性验证进程；为了建立过程完整性，CW定义了对于转换过程的应用相关验证；为了约束用户、进程和数据之间的关系，CW使用了三元组结构。
CW模型的核心在于以良构事务（well-formal transaction）为基础实现在商务环境中所需的完整性策略。良构事务是指一个用户不能任意操纵数据，只能用一种能够确保数据完整性的受控方式来操作数据。为了确保数据项仅仅能被良构事务操作，首先得确认一个数据项仅仅能被一组特定的程序来操作，而这些程序是经过验证特殊构造，并且被正确安装的。
四、多策略安全模型：中国墙模型
1988年，Brewer和Nash根据现实的商业策略提出了中国墙（Chinese Wall）模型，该模型试图解决的问题是：为了保护相互竞争的客户，咨询公司需要在代理间建立密不可透的“墙”，比如分析员面对客户：银行A，石油公司A，石油公司B，则一旦分析员访问了石油公司A或B，则都不能再访问石油公司B或A，因为A和B处于竞争关系，因而用户只能访问其中之一；初始之时用户可以随意访问任意一个客体，但是一旦访问过一个客体，就不能再访问与该客体有竞争关系的其他客体，或者叫做不能访问其利益冲突类。这里体现了自由选择和强制控制的微妙组合。
