Information flow properties are the semantic cornerstone of a wide range of program transformations, program analyses, and security properties. The variety of information that can be transmitted from inputs to outputs in a deterministic system can be elegantly and very generally captured by representing information as equivalence relations over the sets of possible values, using an equivalence relation on the input domain to model what may be learned, and an equivalence relation on the output to model what may be observed. The set of equivalence relations over a given set of values form a lattice, where the partial order models containment of information, and lattice join models the effect of combining information. This elegant and general structure is sometimes referred to as the lattice of information (Landauer & Redmond CSFW'93). In this work we identify an abstraction of information flow which has not been studied previously, namely disjunctive dependency. We argue that this is both interesting in its own right, providing for example an information flow based semantic model of Chinese-wall policies, and potentially provides increased precision in the application of dependency analysis to computation of quantitative properties. We achieve this via a generalization of the lattice of information to a quantale, a lattice equipped with a tensor operation where the lattice join corresponds to the disjunctive combination of information, and tensor corresponds to conjunctive combination.
Joint work with Sebastian Hunt, City, University of London. (Conditionally accepted to CSF 2021.)