形式化安全模型：把“应该安全”写成可判定的规则

安全设计最危险的句子之一是“系统会适当地保护敏感数据”。“适当”究竟是什么意思？谁能读、谁能写，进程切换角色后怎么算，授权与强制策略冲突时听谁的，状态变化后安全性是否仍然成立？如果这些问题没有精确定义，测试人员就只能凭经验猜测。

形式化安全模型把策略写成集合、关系、序与状态转换：主体发起操作，客体承载信息，标签描述安全属性，规则判断一次操作是否允许。它不会替我们消灭实现漏洞，却能给设计、代码审查、测试和审计提供同一把尺子。

学习目标与共同语言

学完后，你应能独立完成五件事：用支配关系判断多级读写；解释机密性规则与完整性规则为何方向相反；把商业交易拆成受约束数据、转换过程和验证过程；依据访问历史计算利益冲突墙；说明一个可信执行机制为什么必须每次介入、不可篡改并且能够验证。

先约定共同语言。主体 S 是主动发起访问的用户、进程或服务；客体 O 是文件、记录、内存段、消息或设备；访问方式 A 可以是读、追加、读写、执行、调用。标签函数 L(x) 把实体映射到安全类。若安全类同时包含等级与类别，可写成：

L(x) = (level(x), categories(x))

定义 x ⪰ y（x 支配 y）当且仅当 level(x) ≥ level(y) 且 categories(x) ⊇ categories(y)。于是“秘密 + 研发”不一定支配“内部 + 财务”：等级虽高，却缺少财务类别。安全类因此通常是偏序格，而不是人人都可比较的一条直线。

一个通用的访问判定可写成：

允许(S, O, A) = 自主授权(S,O,A) ∧ 强制规则(S,O,A) ∧ 当前状态满足前置条件

这揭示了两个常见误区。ACL 中有权限不代表一定能访问，因为强制规则还可能拒绝；“某用户最高可到秘密级”也不代表其当前进程就在秘密级，主体通常有最高许可级和当前运行级两个值。

Bell–LaPadula：以机密性约束信息流

机密性策略的目标是阻止高敏感信息在未经批准时流到低级区域。设主体当前安全级为 Lc(S)，客体分类为 Lo(O)，则核心规则是：

• 简单安全属性（禁止向上读）：读取要求 Lc(S) ⪰ Lo(O)。
• 星属性（禁止向下写）：追加要求 Lo(O) ⪰ Lc(S)；若一次操作同时读写同一客体，则通常要求二者标签相等。
• 自主安全属性：当前发生的访问必须也存在于访问矩阵 M[S,O] 中。

“禁止向上读”容易理解：内部级进程不能读取秘密文件。“禁止向下写”更关键。假设秘密级进程已读到秘密计划，随后把内容写入公开文件；公开用户虽然没有读取秘密文件，却能从公开副本取得同样信息。星属性正是封堵这条经由写入产生的降级通道。

状态四元组与安全不变式

把系统当前状态写成 v = (b, M, f, H)：

• b 是当前正在发生的访问三元组集合 (主体, 客体, 方式)；它不是“有权访问”，而是“正在访问”。
• M 是访问矩阵，记录主体被授予哪些自主权限。
• f 是标签函数集合，至少记录客体分类、主体最高许可级和主体当前运行级。
• H 是客体层次，如目录树；子客体标签不得低于其父客体所要求的标签约束。

状态安全的含义不是“从未发生攻击”，而是 b 中每个当前访问都同时满足三类属性。系统操作会改变四元组：取得/释放访问改变 b，改变主体或客体级别改变 f，授予/撤销权限改变 M，创建/删除客体改变 H。若初始状态安全，并且每个允许的状态转换都保持安全不变式，则所有可达状态仍安全。这就是把“逐次判定”提升为“对运行轨迹作证明”的关键。

推导案例：教师发布试卷

教师以高等级角色读取试卷模板后，创建的新试卷会继承高等级；学生无法读取。要发布试卷，不能让教师进程直接把文件写到低等级区，因为那是向下写。正确路径是把“降级”交给独立、受控且可审计的发布流程：检查内容、确认授权、生成低等级副本并记录责任人。学生答卷则可以从低等级会话写到教师等级的提交区，这是向上写；但学生随后可能不能直接读取已提交客体，因此界面若要显示答案，应保留低等级本地草稿或通过专门回显机制处理。

Biba：以完整性阻断低可信污染

机密性问“秘密会不会泄露”，完整性问“可信数据会不会被未经授权或低可信来源改变”。为主体和客体赋完整性级 I(S) 与 I(O)，严格完整性策略包含三条规则：

• 简单完整性：主体修改客体要求 I(S) ⪰ I(O)，也就是禁止向上写。
• 完整性约束：主体读取客体要求 I(O) ⪰ I(S)，也就是禁止向下读。
• 调用属性：主体 S1 调用主体 S2 要求 I(S1) ⪰ I(S2)，防止低完整性主体借用高完整性服务替它污染高可信数据。

为何高完整性进程不能读取低完整性文件？如果只禁止低完整性进程写高完整性文件，一个带缺陷或被植入恶意逻辑的高完整性进程仍可能读取不可信输入，再把结果写进高完整性数据库。禁止向下读切断了“低可信输入 → 高可信进程 → 高可信客体”的间接污染链。

实际系统不一定采用最严格版本。完整性标签可以映射为“未经验证输入、普通业务数据、经复核数据、发布基线”。下载目录中的脚本属于低完整性，构建服务与发布仓库属于高完整性；发布服务不应直接读取未校验产物，更不能让低完整性进程修改已签名版本。

Clark–Wilson：用良构事务保护商业数据

按等级限制信息流对账务、库存、医疗记录等业务并不够。真正的业务要求通常是“余额不能直接改，只能通过转账；借贷必须平衡；发起人不能同时审批；每笔变化必须可追溯”。Clark–Wilson 把完整性落实为良构事务与职责分离。

四类元素构成工作流：

• 受约束数据项 CDI：必须保持业务不变式的数据，如账户余额、订单状态、审计日志。
• 非受约束数据项 UDI：尚未信任的外部输入，如表单、上传文件、消息字段。
• 完整性验证过程 IVP：检查所有 CDI 是否仍处于有效状态，如总账平衡、库存非负。
• 转换过程 TP：把一组有效 CDI 变成另一组有效 CDI，或验证 UDI 后将其转为 CDI。

认证规则与执行规则

认证回答“什么过程在什么数据上是正确的”：IVP 必须正确识别有效状态；TP 对指定 CDI 集合执行时必须保持有效状态；用户—TP—CDI 关系要满足职责分离；TP 必须向仅追加日志写入足够信息以重建操作；接受 UDI 的 TP 对任何输入都只能产生合法 CDI 或拒绝。

执行回答“系统如何确保只能这样做”：CDI 只能由已认证 TP 按批准关系修改；系统维护用户可执行的 TP 及其可操作 CDI 列表；执行前认证用户身份；只有认证管理者能改变这些关系，而且认证者不得执行自己认证的生产操作。

以转账为例，用户提交“从 A 向 B 转 100”是 UDI；转账 TP 校验金额、权限和余额，把 A、B 两个 CDI 从一个平衡状态转换到另一个平衡状态；系统把操作人员、时间、旧值、新值和事务编号写入追加日志；日终 IVP 再核对总额。数据库管理员即使能维护系统，也不应获得绕过 TP 直接改余额的路径。

动态利益冲突墙：让历史参与授权

利益冲突策略不按高低级别划分数据，而把信息组织为三层：单个对象属于某公司的数据集 DS；相互竞争公司的数据集组成冲突类别 CI；主体的访问历史决定未来权限。每个主体都有自己不断变化的一堵墙。

读规则是：主体可读取对象 O，当且仅当 O 所在 DS 已被该主体访问，或者 O 所在 CI 中尚未访问任何 DS。第一次读取甲银行后，可以继续读甲银行，但不能再读同属银行业 CI 的乙银行；仍可首次选择能源业中的任一公司。

仅限制读取不足以阻止间接泄露。设小林读过甲能源和甲银行，小周读过乙能源和甲银行。若小林能把甲能源信息写进双方都可读的甲银行数据集，小周便间接得到竞争对手信息。因此写规则要求：目标必须先满足读规则，并且主体当前可读的所有受保护对象都与写入目标处于同一 DS。其结果很严格：跨多个数据集做分析的人往往只能读，不能向受保护数据集写。

经过充分净化、无法识别具体公司的汇总数据可放入独立的净化数据集，不受普通墙约束。但“去掉公司名”不必然等于安全；小样本、唯一金额、时间组合仍可能重新识别主体，净化本身必须由受信流程完成。

信息流、隐式流与工程映射

显式流直接通过赋值或消息传递出现，例如 public = secret。隐式流由控制条件编码，例如：

if secretBit == 1:
    publicFlag = 1
else:
    publicFlag = 0

公开变量没有直接读取秘密值，却精确暴露了一位秘密信息。异常、响应时间、缓存命中、文件锁、CPU 占用与消息长度还会形成隐蔽通道。经典访问模型主要约束受控对象上的显式读写，不能自动消除所有共享资源通道。

工程上可采用三种互补方法。静态信息流类型系统在编译时传播标签并拒绝违规路径；动态污点跟踪在运行时给输入和派生值附标签；架构隔离把不同安全域放在不同进程、容器、主机或时间窗口中。允许从高到低的信息必须通过明确的解密、脱敏、聚合或审批函数，称为受控降级；完整性方向上，从低可信输入提升为高可信数据则需要校验、签名、复核或可信转换。

把多级安全映射到 RBAC 时，可以为每个安全级创建读角色与写角色，用户许可级限制其可激活角色；对象权限按标签分配；会话只激活当前工作级所需角色。普通角色不能改变标签，降级、角色管理与策略维护交给独立管理角色。数据库还要选择分类粒度：整库、表、行、列或单元格。粒度越细，查询可能通过谓词、连接或空结果推断高等级事实。

低级用户插入一个与高级隐藏行相同主键时，系统若提示冲突，就泄露隐藏行存在；若覆盖，则破坏完整性；若保留两个不同标签的同键记录，则形成多实例。多实例降低推断风险，却让数据语义和应用逻辑更复杂。能用整库或表级隔离解决时，通常比细粒度多实例更容易正确实现。

可信系统、参考监控器与可信平台

“信任”是依赖者愿意相信系统符合规格；“可信度”则要求有令人信服的证据证明它值得信。可信计算基 TCB 是真正执行某项安全策略的硬件、固件和软件集合。TCB 越大，必须审查、隔离和验证的代码越多，因此应尽量小而边界清晰。

参考监控器是主体到客体之间的强制检查点，依赖安全策略库做决定，并把安全事件写入审计记录。它必须具备三项性质：

1. 完全介入：每一次访问都检查，不能只在“打开文件”时检查一次，然后允许通过别的句柄、共享内存或缓存绕过。
2. 隔离保护：攻击者不能修改监控逻辑、策略库或审计链，也不能从旁路直接触达客体。
3. 可以验证：结构足够小且明确，能够通过形式分析、代码审查与系统测试证明其确实执行规则。

这三点解释了为何安全内核、最小权限代理、系统调用边界与硬件保护有价值。普通 ACL 可能允许一个木马代表受害者读取敏感文件，再写入攻击者准备的公开文件；机密性参考监控器即使看到 ACL 允许，也会因向下写而拒绝，强制策略优先于所有者授予。

可信平台模块进一步提供硬件信任根。度量启动逐阶段计算组件摘要并把结果扩展进受保护寄存器，形成不可随意改写的启动记录；远程证明用带挑战随机数的签名说明当前配置，随机数防止重放旧证明；密封存储把密钥绑定到特定平台状态，只有度量值满足策略时才释放。要注意，证明“运行的是已知版本”不等于证明“该版本没有漏洞”，它提供的是身份与状态证据，不是万能正确性证明。

枚举规则，而不是凭感觉猜

下面的实验台把主体与客体设为 0–3 四个等级，并对同一次读写同时计算机密性与完整性。它不访问网络、不读本机文件，所有计算都在页面内完成。尝试固定主体为 2，依次改变客体等级，观察两种模型何时给出相反结果。

为了验证实现没有漏掉组合，我们在沙盒环境中还穷举了 4 个主体等级 × 4 个客体等级 × 2 种操作 = 32 种情况。真实输出如下：

BLP: allow=20, deny=12, total=32
Biba: allow=20, deny=12, total=32
ChineseWall 银行/甲银行: ALLOW
ChineseWall 能源/青山能源: ALLOW
ChineseWall 银行/乙银行: DENY
ChineseWall 能源/青山能源: ALLOW

两种格模型允许数量相同并不表示策略相同；它们在对称等级集合上只是把方向反转。测试时应验证具体输入—输出对，而不是只比较通过率。动态墙的第三次请求被拒绝，是因为同一冲突类别已经选择甲银行；第四次继续访问原能源数据集则仍允许。

可把这种枚举法扩展成属性测试：断言 BLP 允许读必有 S ≥ O，允许写必有 S ≤ O；断言同一主体一旦在某 CI 访问 DS-A，任何 DS-B 的后续读取都拒绝；断言任何 CDI 的状态变化都能在授权 TP 和追加日志中找到对应记录。

局限、选型

形式化模型的力量来自抽象，也受限于抽象。标签可能分错；合法降级不在基本规则内；共享资源可形成隐蔽通道；并发、撤权延迟和缓存会破坏“每次检查”的假设；细粒度数据库标签会引入推断与多实例；多个模型同时启用时还可能把正常业务完全封死。更根本的是，模型证明通常针对设计规格，缓冲区越界、竞态、供应链篡改或错误配置仍可能让实现偏离规格。

选型时先从业务不变式出发：防止敏感数据向低域流动，采用机密性格与受控降级；防止低可信输入污染发布基线，采用完整性标签、可信转换与签名验证；保护商业账务，采用良构事务、职责分离和可重建日志；防止顾问接触竞争客户，采用历史相关的利益冲突墙；要求策略不可绕过，则缩小 TCB，并围绕参考监控器建立完全介入、隔离与验证证据。

最后把模型变成可执行工程清单：明确主体、客体、操作和标签；写出允许关系与状态不变式；定义合法降级、净化与升级入口；把所有入口收敛到不可绕过的检查点；对管理操作进行职责分离和审计；穷举小状态空间并对大系统做属性测试；持续检查实现边界是否与模型假设一致。