ENHANCING EXPRESSIVENESS OF INFORMATION FLOW LABELS: RECLASSIFICATION AND PERMISSIVENESS
Increasing the expressiveness of information flow labels can improve the permissiveness of an enforcement mechanism. This thesis studies two formulations of expressive information flow labels: RIF labels and label chains. Restrictions that a reactive information flow (RIF) label imposes on a value depend on the sequence of operations used to derive that value. This allows declassification, endorsement, and other forms of reclassification to be supported in a uniform way. Piecewise noninterference (PWNI) is introduced as the appropriate security policy. A type system is given for static enforcement of PWNI in programs that associate checkable classes of RIF labels with variables. Two checkable classes of RIF labels are described: general-purpose RIF automata and κ-labels for programs that use cryptographic operations. But labels themselves can encode information, and thus, certain restrictions should be imposed on their use, too. A new family of dynamic enforcement mechanisms is derived to leverage arbitrarily long label chains, where each label in the chain defines restrictions for its predecessor. These enforcers satisfy Block-safe Noninterference (BNI), which proscribes leaks from observing variables, label chains, and blocked executions. Theorems characterize where longer label chains improve permissiveness of dynamic enforcement mechanisms that satisfy BNI. These theorems depend on semantic attributes of such mechanisms as well as on initialization, threat model, and size of lattice of labels.