### Skapa referens, olika format (klipp och klistra)

**Harvard**

Hunt, S. och Sands, D. (2006) *On flow-sensitive security types*.

** BibTeX **

@conference{

Hunt2006,

author={Hunt, Sebastian and Sands, David},

title={On flow-sensitive security types},

booktitle={POPL'06, Proceedings of the 33rd Annual. ACM SIGPLAN - SIGACT. Symposium on Principles of Programming Languages},

abstract={ 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. },

year={2006},

}

** RefWorks **

RT Conference Proceedings

SR Electronic

ID 18056

A1 Hunt, Sebastian

A1 Sands, David

T1 On flow-sensitive security types

YR 2006

T2 POPL'06, Proceedings of the 33rd Annual. ACM SIGPLAN - SIGACT. Symposium on Principles of Programming Languages

AB 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.

LA eng

LK http://www.cs.chalmers.se/~dave/papers/Hunt-Sands-POPL06.pdf

OL 30