Renaming or Tightness: Enforcing Disjunctive Information Flow Policies

The paper addresses the enforcement of disjunctive information flow policies, which allow a value to depend on at most one of two secrets but never both. Examples include the Chinese Wall policy (an analyst may consult one client's file or the other's, but not both), secret sharing (one share may be released but not its sibling), and clinical dashboards (a patient's diagnosis or identity may be shown, never the pair). Such policies are not lattice-shaped: in a lattice the join of two admissible dependencies is admissible again.

Hunt and Sands introduced the quantale of information to give disjunctive policies a semantics, but left the enforcement layer open. This paper builds the flow-sensitive type system family that the quantale calls for.

The quantale of information [2] keeps the lattice of information as a special case and adds a second combination operator: disjunction remains the join, and conjunction becomes a tensor ⊗ that is not idempotent, so that combining a disjunctive dependency with itself may reveal strictly more than the dependency alone. For the ethical-wall label S = tc ∼1, ∼2 of Example 1, S ⊗ S = ⊤.

Example 1 (the second read): Client files r1 and r2 are independent. An upstream process produces a summary s under the ethical wall, so its label is the disjunctive element S = tc ∼1, ∼2. A report generator uses the summary twice:

C3 = (u:= s; w:= s).

The pair (u, w) is within the wall: Whichever client's data the summary honoured on this run, both copies honour the same one, so an observer of u and w learns exactly what an observer of s learns. But a type system whose environments hold elements of the quantale must give u and w the type S each, and the joint observation of two variables is their tensor: S ⊗ S = ⊤. The certificate says the report may reveal both clients' files. The mechanism has forgotten that the two copies are one choice.

The powerset of variables carries two structures at once. Read as an ordered monoid under union it is the free commutative idempotent monoid on the variables. With no idempotence imposed, the free commutative monoid has multisets as its elements. Over a quantale they come apart:

• Over the multiset object U N: the whole of [1] survives unconditionally: monotone renaming, canonical derivations, principal typings and internal completeness, for every affine labelling (Theorem 2). This object counts uses, so on Example 1 it answers ⊤.

• Over the set object U: "specialisation is no longer a homomorphism. It factors as a strict homomorphism after an oplax section that crushes multiplicities (Proposition 4), and the bound it produces is smaller. It is sound for every labelling (Theorem 4) and strictly smaller as soon as a disjunctive source is read twice (Theorem 5)." On Example 1 it answers S, which is the truth.

• The free locale L (the literal transcription of the lattice-era object): "It is tight on Example 1, since union is idempotent, but it identifies the join with the tensor and so erases the difference between 'this run depended on X1, that run on X2' and 'some run depended on X1 ∪ X2', which is precisely the distinction the quantale exists to make (Corollary 2)."

Of the three objects, the multiset one loses same-source correlation, the locale one loses branch disjunction, and only U keeps both.

Theorem 2: Over U N, for every affine σ: ασ N and its right adjoint both satisfy the premises of Lemma 1 (monotone, lax monoidal, lax unital); canonical derivations hold in both directions; 1 ⊢ M σ C Γ′ iff ασ N(Δ C N) ⊑ Γ′, so Δ C N is a principal typing; and no member of the family certifies more M-typings than the M-system itself.

Theorem 3: The M-system is an image: A C M(1, σ) = ασ N(Δ C N) pointwise.

Theorem 4 (soundness of the set bound): Let M = QoI(D), σ affine and g legal for σ. Then for every C and W, π W ∘ ⟦C⟧ ∘ ĝ: ασ(J W) ⇒ Id.

Theorem 5: Let σ(v0) be non-idempotent and C3 as in Example 1. The judgement bounding the joint observation of u, w by σ(v0) is semantically true and is obtained by specialising the universal typing, while every joint bound for u, w derivable in the M-system is above σ(v0) ⊗ σ(v0).

Theorem 6: ασ(J W) = ασ N(J W N) for every C and W iff every σ(v) is ⊗-idempotent. Over a finite set of secrets the idempotent elements of QoI(D) are exactly the principal ideals together with ⊥, so the condition says that every label is a classical equivalence-relation label.

Proposition 7 (the independent-attribute ceiling): Let a mechanism of the independent-attribute shape be sound, by any rules whatsoever. Then for C3 of Example 1 and W = u, w it certifies a bound ⊒ σ(v0) ⊗ σ(v0). No rule is named in that argument. Once the two entries are separate elements of M, the information that they were served by one mediator is gone, and the tensor cannot recover it.

Theorem 7 (no-go): Let R be renaming-stable, let (V, ι, h σ) be a type object over R, and let Δ C V be any postcondition R-derivable in V from ι. Then h σ(⊗ w∈W Δ C V(w)) is above the greatest lower bound of the joint bounds for W that R derives in M from σ directly. For R the rules of Figure 1 that bound is ασ N(J W N).

Proposition 8 (exactness for principal typings): Let the type object have every h σ a quantale homomorphism with h σ(ιv) = σ(v), and let the derivation be the algorithmic one. Then h σ(⊗ w∈W Δ C V(w)) = ασ N(J W N).

The conclusion: On a quantale one may have renaming or tightness, but not both.

Corollary 1 (a second read certifies nothing): Call m saturated when m ⊗ m = ⊤. The ethical-wall label S and the label of a two-share split are saturated. If σ(v0) is saturated and some member of J W N uses v0 at least twice, then ασ N(J W N) = ⊤, so by Theorem 7 no mechanism in the paradigm certifies W against any policy below ⊤.

Theorem 8 (secure programs are rejected): Let σ(v0) be saturated and consider the policy (σ, u, w, σ(v0)) with C3 of Example 1. Then C3 complies with the policy and is accepted by the mechanism of Section VIII, while every sound independent-attribute mechanism rejects it, whatever its rules and whatever universal object it specialises from.

"The rejected program is not a pathology constructed for the proof. It is one source read twice: the reconstruction step of secret sharing, a sanitised report quoted in two places, any dashboard that renders one disjunctively labelled value in two panels."

Theorem 9 (deferred specialisation): Let environments take values in U, so that typing is universal typing, and let the labelling act only on the observation, through ασ. The result is sound for every affine σ (Theorem 4), is below every judgement derivable with M-valued environments, and agrees with M-valued typing iff every σ(v) is idempotent.

Theorem 10 (minimality of the read-out): Every join preserving read-out β: U → M that is sound for σ satisfies β ⊒ ασ pointwise, so ασ is the least sound join preserving read-out.

Corollary 3 (sandwich): For every C, W and affine σ, ασ(J W) ⊑ ασ N(J W N), the left side being the floor of sound join-preserving read-outs and the right side the ceiling of the renaming paradigm, with equality iff the labels are idempotent.

The paper separates three uses of a walled source:

1. One source, one use: A report reads s once. Both bounds are S, so the policy is certified by any mechanism.

2. One source, two uses: Example 1. The universal type is ŝ ⊗ ŝ = ŝ and the set bound is S, while the multiset bound is S ⊗ S = ⊤. Only the deferred read-out certifies it.

3. Two sources, one use each: A report reads s1 and s2. Both bounds are S ⊗ S = ⊤, which is correct: the two mediators may honour different disjuncts, one revealing r1 and the other r2, so the pair reveals the secret and the wall is genuinely breached.

Proposition 9 (decidability): For finite Var: U(Var) is finite and its elements are represented by the antichain of their maximal sets, so universal typing terminates and compliance against a finite QoI(D) target is decidable. U N(Var) is infinite and has no ascending chain condition, but downsets of N Var are finite unions of ideals by Dickson's lemma, and by Proposition 5 only multiplicities below the largest label order affect the specialised bound, so a finite truncation decides the multiset side as well.

Proposition 10 (finite truncation): Let N ≥ max v ordσ(v), let N≤N be 0,..., N under the capped sum min(a+b, N), and let U N≤N be the downset quantale of (N≤N) Var. Capping multiplicities extends to a surjective quantale homomorphism c N: U N → U N≤N, the algorithmic systems commute with it, and ασ N factors through it.

"Disjunctive policies were given a semantics before they were given an enforcement mechanism, and building the mechanism turns out to force a choice that the lattice era never had to make. The universal object that made flow-sensitive typing reusable across policies splits: the free commutative quantale on the variables keeps the entire mechanism and loses same-source correlation, the free object with idempotent generators keeps precision and loses renaming, and the lattice-era object loses branch disjunction. No object with a renaming-capable specialisation improves on the first, so for the ethical-wall and secret-sharing labels a second read of a source leaves nothing to certify, and programs that respect the wall are rejected. Deferring specialisation to the judgement level recovers the missing precision, through the least sound join-preserving read-out."

Based on the paper, here are the specific improvements I can make to AI systems:

Improvement: Implement a type system for AI systems that tracks disjunctive dependencies (where a value may depend on at most one of several secrets) using the quantale of information, with a deferred specialisation mechanism.

What the improved system can do:

• Distinguish between this run depended on secret A vs. this run depended on secret A or B in a way that preserves the branch disjunction (which disjunct was chosen) without conflating it with the union of secrets.

• Correctly certify programs that read a single disjunctively-labelled source twice (e.g., a sanitised report quoted in two places) as safe, whereas naive type systems would reject them as leaking both secrets.

• Detect genuine breaches where two different disjunctively-labelled sources are each read once, correctly flagging that the pair may reveal both secrets.

A disjunctive policy allows a value to depend on at most one of two secrets and never on both: an analyst may consult one client's file or the other's, a share of a split secret may be released but not its sibling. Such policies are not lattice-shaped, and Hunt and Sands introduced the quantale of information to give them a semantics, leaving the enforcement layer open. We build the flow-sensitive type system family that the quantale calls for, and show that the object which makes such families useful, the universal type object from which every member specialises, splits in two, with a consequence for enforcement. Over the free commutative quantale on the program variables the whole mechanism survives for every policy: monotone renaming, canonical derivations, principal typings, internal completeness. Over the free object with idempotent generators the certified bound is strictly more precise and still sound, because it records that two reads of one source honour one disjunct. The gap cannot be closed from inside the independent-attribute family: no mechanism of that shape whose labelling maps support monotone renaming certifies a bound more precise than the first, and for principal typings under generator-exact homomorphic specialisation the two coincide. Under the ethical-wall and secret-sharing labels the second read of a disjunctive source therefore drives every such certificate to no guarantee, and programs that satisfy the policy are rejected. The literal transcription of the lattice-era object is no escape either: it is a further quotient that loses branch disjunction. Precision is recovered by deferring specialisation to the judgement level, and the resulting read-out map is the least sound join-preserving one.