AI summaryⓘ
The authors study a special type of policy where information can depend on one secret at a time but never both together, like choosing which client's data to look at, without mixing them. These policies don’t fit into the usual mathematical framework (lattices), so previous work introduced a new semantic tool called a quantale but left it unclear how to enforce such policies. The authors develop a related type system that fits these policies and uncover that the basic type object splits into two parts, affecting enforcement precision. They find that some enforcement methods are too strict and reject safe programs, but by adjusting how types are specialized during checking, they can recover precision and sound enforcement results.
disjunctive policyquantaleflow-sensitive type systemuniversal type objectmonotone renamingprincipal typingsidempotent generatorssecret sharingethical walllattice
Abstract
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.