A Quantale of Information
A Quantale of Information
复制标题
信息量子
DOI：
10.1109/csf51468.2021.00031
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
David Sands
中科院分区：
文献类型：
--
作者：
Sebastian Hunt;David Sands
信息流属性是广泛的程序转换、程序分析和安全属性的语义基石。在确定性系统中，可以从输入传输到输出的各种信息可以通过将信息表示为可能值集合上的等价关系来捕获，使用输入域上的等价关系来建模可以学习的内容，以及使用输出上的等价关系来建模可以观察的内容。给定值集合上的等价关系集合形成格，其中偏序模型信息的包含，而格连接模型组合信息的效果。这种优雅的和一般的结构有时被称为lattice of information.In本文中，我们确定了一个抽象的信息流，这是以前没有研究过的，即析取依赖（取决于x或y，不同于取决于x和y）。我们认为，这细化了空间的语义模型依赖的方式，这是既有趣的，在其本身的权利，并已在安全设置的实际利益的应用程序（特别是，在所谓的“中国墙政策”有效的情况下）。为了对析取依赖进行建模，我们以更丰富的结构的形式引入信息网格的非平凡概括，建立在一组等价关系上，这些等价关系在一个叫做平铺闭包的新条件下闭合。这种结构形成了一个Quantale -一个配备了张量操作的晶格-其中晶格连接对应于信息的析取组合，而张量对应于合取组合。利用这一点，我们概括的信息流属性的定义，并表明该定义的关键属性需要支持组合推理程序。
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 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.In this paper we identify an abstraction of information flow which has not been studied previously, namely disjunctive dependency (depending on x or y, as distinct from depending on both x and y). We argue that this refines the space of semantic models for dependency in a way which is both interesting in its own right and which has applications in security settings of practical interest (in particular, where so-called “Chinese wall policies” are in effect).To model disjunctive dependency we introduce a nontrivial generalisation of the lattice of information in the form of a richer structure, built on sets of equivalence relations closed under a novel condition called tiling-closure. This structure forms a quantale - a lattice equipped with a tensor operation - in which lattice join corresponds to disjunctive combination of information, and tensor corresponds to conjunctive combination. Using this we generalise the definition of information flow properties, and show that the definition has the key properties needed to support compositional reasoning about programs.
DOI：
10.1145/1111037.1111045
发表时间：
2006-01
期刊：
--
影响因子：
--
作者：
Sebastian Hunt;David Sands
通讯作者：
Sebastian Hunt;David Sands