Summary

  • Dorothy E. Denning’s 1976 model orders security classes and uses their least upper bound, or join, to calculate the minimum class that may receive information derived from several inputs.
  • The model covers explicit transfers and implicit dependencies through control conditions, but its proof is only about flows represented by the program, under declared labels and a chosen permission order.
  • Covert channels, defective implementations, mistaken classification and unjustified declassification remain separate problems. Passing a lattice check is evidence about one control, not a verdict on the whole system.

Suppose a program combines two inputs. One is classified at level A and the other at level B. Where may the result go? Dorothy E. Denning’s 1976 paper, “A Lattice Model of Secure Information Flow”, answers with a compact rule: first compute the least security class that both inputs are allowed to reach. That class is their least upper bound, usually called the join. The destination must be permitted to receive information at least that sensitive.

The rule is easy to draw as a hierarchy, but its point is not the picture. It is the conversion of policy into an order that a program analysis can test.

Denning writes the relation as A → B: information associated with class A is permitted to flow into class B. The relation is reflexive, transitive and antisymmetric, so it forms a partial order. Partial matters. Two classes need not be directly comparable. A compartment for one project and a compartment for another can remain distinct even if both have a common class above them. The join supplies the least common destination permitted by the policy.

If output c depends on inputs a and b, the consistency condition can be read as: class(a) join class(b) → class(c). This is not a claim that c is harmless. It is a claim that, under the declared classes and order, the information represented by those inputs is permitted to reach c.

Dependency, not merely copying

The strongest part of the model is its definition of flow through influence. Information flows when information associated with one object affects information associated with another. An assignment such as b := a is an explicit flow. A condition can create an implicit flow even when it copies no value.

Denning’s example has the form if a = 0 then b := c. The final state of b can reveal something about a, because an observer may learn whether the assignment happened. Information therefore flows from a to b through control, as well as from c to b through assignment. An analysis that only follows copied bytes misses the first dependency.

This distinction remains operationally important. Authorization reviews often ask who may read a record, while software moves evidence through branch conditions, error paths, counters, resource choices and output timing. The 1976 paper supplies a disciplined vocabulary: identify which inputs can affect which outputs, combine their classes, and test the resulting flow against policy.

What compilation can certify

The model supports compile-time certification. An analyzer can associate classes with variables and expressions, propagate the class of a controlling condition, and reject a program whose represented dependencies violate the permitted-flow relation. The later paper “Certification of Programs for Secure Information Flow” develops that mechanism in more detail.

Authorship is part of the record. The 1976 lattice paper is Dorothy E. Denning’s solo work. The certification paper is joint work by Dorothy E. Denning and Peter J. Denning, published in Communications of the ACM in 1977 after Purdue Technical Report 76-181. Treating the later mechanism as Dorothy’s alone erases a collaborator; treating the two papers as one text hides the sequence from model to certification method.

The resulting assurance is meaningful. A reviewer no longer has to accept “the program should not leak downward” as an aspiration. For modeled variables, operations and control structures, the reviewer can ask whether every derived class is allowed to reach its destination. The answer can be checked before the program runs and repeated after a source change.

Where the proof stops

Denning also states the boundary. The 1976 paper addresses legitimate and storage channels, not covert channels such as a process manipulating system load. Certification cannot verify a flow that the program representation does not specify. Unchecked bounds, dangling references, compiler defects, a mismatched executable or hardware malfunction can break the connection between certified semantics and actual execution.

The policy inputs can also be wrong. A precise proof over a mistaken label is still precise. If a sensitive source is marked public, the lattice may correctly permit a flow that the organization never intended. Conversely, the later survey “Data Security”, co-authored by Dorothy and Peter Denning, explains how upward-only class rules tend to overclassify derived information. Authorized downgrading and information-losing programs are responses to that pressure, but both require evidence beyond the lattice relation. A person must decide why a release is legitimate, what information was removed, and who is accountable if the assumption fails.

Covert channels make the boundary more concrete. Timing and resource consumption can communicate without appearing as ordinary assignment or storage flow. An output may also be formally permitted and still reach an insecure endpoint, an excessive audience or a downstream system that strips its label. The lattice does not promise to solve those problems; overclaiming begins when an organization says that it does.

In her 1999 acceptance speech, “The Limits of Formal Security Models”, Denning returned to this lesson in first-person terms: formal reasoning establishes results inside a simplified model and its assumptions, while real attacks often step outside that box. This is not a rejection of formal methods. It is a reason to state exactly what a successful check has established.

One proof in a longer evidence chain

For a modern engineering organization, the useful artifact is therefore not a green badge called “secure.” It is a chain of evidence:

  1. a versioned policy defining classes, joins and permitted flows;
  2. provenance for the labels assigned to data and outputs;
  3. analysis results that include both explicit and represented implicit dependencies;
  4. a reproducible link from reviewed source to compiler, binary and deployment;
  5. separate authority and logging for declassification;
  6. runtime and endpoint controls that preserve labels and destinations; and
  7. tests or monitoring for covert and side channels outside the static model.

Bell–LaPadula belongs to the neighboring history of multilevel security and appears in Denning’s references. It should not displace her own argument. Her distinctive move here is to make information dependency, class combination and certification work together. Access rules ask whether a subject may perform an operation. Denning’s lattice asks what class must follow from the information that actually influences a result.

That difference is why the paper still matters. It offers neither a magical proof nor a mere metaphor. It gives one precise question a precise answer—and makes responsible readers identify every other question for themselves.

Sources