On flow-sensitive security types
On flow-sensitive security types
复制标题
DOI：
10.1145/1111037.1111045
复制
发表时间：
2006-01
期刊：
影响因子：
--
通讯作者：
Sebastian Hunt;David Sands
中科院分区：
文献类型：
--
作者：
Sebastian Hunt;David Sands
本文研究了一类语义合理的流敏感类型系统的形式化性质，这些系统用于跟踪简单的While程序中的信息流。通过选择流格作为程序变量的幂集合，我们得到了一个系统，在很强的意义上，它包含了流格中的所有其他系统(特别是，对于每个程序，它提供了一个可以推断所有其他系统的主要类型)。与Amtoft和Banerjee的Hoare式独立逻辑(SAS‘04)相比，这一独特的系统被证明是等价的，尽管描述更简单。尽管如此，我们证明了对于给定的格选择，该族中的任何类型系统都不能比该格本身的类型系统给出更好的结果。最后，对于在这些系统中的任何一个可类型的程序，我们证明了如何构造在简单的流不敏感系统中可类型的等价程序。我们认为，这种通用方法在验证携带代码的设置中可能很有用。
This article investigates formal properties of a family of semantically sound flow-sensitive type systems for tracking information flow in simple While programs. The family is indexed by the choice of flow lattice.By choosing the flow lattice to be the powerset of program variables, we obtain a system which, in a very strong sense, subsumes all other systems in the family (in particular, for each program, it provides a principal typing from which all others may be inferred). This distinguished system is shown to be equivalent to, though more simply described than, Amtoft and Banerjee's Hoare-style independence logic (SAS'04).In general, some lattices are more expressive than others. Despite this, we show that no type system in the family can give better results for a given choice of lattice than the type system for that lattice itself.Finally, for any program typeable in one of these systems, we show how to construct an equivalent program which is typeable in a simple flow-insensitive system. We argue that this general approach could be useful in a proof-carrying-code setting.