摘要

  • Dorothy E. Denning 在 1976 年的个人论文中，把安全类别组织成偏序，并用最小上界（join）计算由多个输入共同影响的结果至少应属于哪个类别。
  • 模型既追踪赋值和输入输出造成的显式流，也追踪控制条件造成的隐式依赖；但证明只覆盖程序表示出来的流动、声明过的标签和选定的许可关系。
  • 隐蔽信道、错误分类、实现缺陷和缺乏依据的降密仍需分别治理。通过格检查，是一项控制的证据，不是整个系统的安全判决。

两个输入共同决定一个结果时，结果应放到哪里？在 1976 年的论文 《A Lattice Model of Secure Information Flow》 中，Dorothy E. Denning 给出了一条简洁规则：先找出两个输入都允许到达的最低安全类别，也就是它们的最小上界，通常称为 join；结果的目标类别必须允许接收这一敏感度的信息。

图上看，它像一组由低到高的节点。但格模型的关键不是图形，而是把政策变成可检验的次序。Denning 用 A → B 表示“A 类的信息获准流入 B 类”。这个关系具有自反性、传递性和反对称性，因此构成偏序。偏序并不要求任意两个类别都能直接比较。两个项目隔离区可以彼此独立，同时在更高处拥有共同的接收类别；join 就是政策允许的最小共同上界。

若输出 c 同时依赖输入 a 和 b，一致性条件可以写成：class(a) join class(b) → class(c)。这句话没有证明 c 在现实中无害。它只说明在当前分类与次序之内，来自这些输入的信息获准到达 c。

流动指的是影响，而不只是复制

这套模型最有穿透力的地方，是把信息流定义为影响关系。b := a 是显式流；控制条件即使没有复制数值，也可能产生隐式流。

Denning 讨论过形如 if a = 0 then b := c 的语句。观察者从 b 的最终状态可能推知赋值是否发生，进而获知关于 a 的信息。因此，除了 c 经赋值流向 b，a 也经由控制条件隐式影响 b。只追踪“哪些字节被拷贝”的工具会漏掉后一条依赖。

这一区分对今天仍很实用。权限审核常问“谁能读取这条记录”，而软件还会通过分支、错误路径、计数器、资源选择和响应时间传播信息。Denning 的框架要求分析者先问：哪些输入能够影响哪些输出？再组合这些输入的类别，并检验目标是否符合政策。

编译期认证能说明什么

格模型支持在程序运行前认证信息流。分析器可以给变量和表达式关联安全类别，把控制条件的类别传播到受其影响的语句，并拒绝违反许可关系的程序。后来的 《Certification of Programs for Secure Information Flow》 对这种机制做了进一步展开。

作者边界也必须写清。1976 年的格模型论文由 Dorothy E. Denning 单独署名；认证论文由 Dorothy E. Denning 与 Peter J. Denning 合著，先有 Purdue Technical Report 76-181，后于 1977 年刊登在 Communications of the ACM。把合著成果全部归给 Dorothy，会抹去共同作者；把两篇论文混成一篇，也会掩盖从形式模型到认证方法的演进。

这种认证确实带来强证据。评审者不必只接受“程序原则上不应向下泄露”的愿望，而能针对模型中的变量、操作和控制结构，逐一检查派生类别是否获准到达目标；源代码发生变化后，也能重新执行同一检验。

证明在哪些地方停止

Denning 同样明确说明限制。1976 年论文处理合法信道和存储信道，并不处理进程通过系统负载等方式制造的隐蔽信道。程序没有表达出来的流，认证无法验证。越界访问、悬空引用、编译器缺陷、部署了不同的二进制文件，或硬件故障，都可能切断“已认证语义”与“实际执行”之间的联系。

政策输入本身也可能错误。错误标签上的精确证明，仍然只是精确地证明了错误前提。敏感数据若被标成公开，格模型可能完全正确地允许一条组织本不想允许的流。相反，Dorothy 与 Peter Denning 合著的 《Data Security》 指出，只允许向上流动容易造成过度分类。授权降密和信息损失程序可以缓解这种压力，但它们需要格关系之外的证据：谁有权批准、什么信息被消除、失败后由谁承担责任。

隐蔽信道进一步说明了边界。时间与资源消耗可以传递信息，却不呈现为普通赋值或存储流。一个输出即使在形式上获准，也可能到达不安全终端、过大的受众，或在下游丢失标签。格模型从未承诺独自解决这些问题；组织把“符合模型”说成“系统安全”时，过度承诺才开始发生。

1999 年，Denning 在 《The Limits of Formal Security Models》 中再次强调：形式推理在简化模型及其假设内部建立结论，而现实攻击经常走到模型盒子之外。这不是对形式方法的否定，反而要求人们准确说明每次成功检查究竟建立了什么。

把认证放进完整证据链

因此，现代工程组织需要保存的不是一个写着“安全”的绿灯，而是一条可追溯证据链：

  1. 定义类别、join 和许可流的版本化政策；
  2. 数据与输出标签的来源及审批记录；
  3. 同时覆盖显式依赖和已建模隐式依赖的分析结果；
  4. 从被评审源代码到编译器、二进制文件和部署的可复现关联；
  5. 独立的降密权限与日志；
  6. 能在运行时和终端维持标签与目标约束的控制；
  7. 针对静态模型之外的隐蔽信道和侧信道测试或监测。

Bell–LaPadula 属于相邻的多级安全史，也出现在 Denning 的参考文献中，但它不能替代她自己的论证。这里独特的推进，是把信息依赖、类别组合和程序认证接在一起。访问控制问主体能否执行某项操作；Denning 的格模型追问，实际影响一个结果的信息要求这个结果承接什么类别。

这正是论文持续有用的原因。它既不是万能证明，也不只是一个比喻，而是对一个精确问题给出精确答案，并迫使负责任的读者把其余问题逐项列出。

来源