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

**Harvard**

Hunt, S. och Sands, D. (2011) *From Exponential to Polynomial-time Security Typing via Principal Types*.

** BibTeX **

@conference{

Hunt2011,

author={Hunt, S. and Sands, David},

title={From Exponential to Polynomial-time Security Typing via Principal Types},

booktitle={Lecture Notes in Computer Science. 20th European Symposium on Programming, ESOP 2011},

isbn={978-364219717-8},

pages={297-316},

abstract={Hunt and Sands (POPL'06) studied a flow sensitive type (FST) system for multi-level security, parametric in the choice of lattice of security levels. Choosing the powerset of program variables as the security lattice yields a system which was shown to be equivalent to Amtoft and Banerjee's Hoare-style independence logic (SAS'04). Moreover, using the powerset lattice, it was shown how to derive a principal type from which all other types (for all choices of lattice) can be simply derived. Both of these earlier works gave "algorithmic" formulations of the type system/program logic, but both algorithms are of exponential complexity due to the iterative typing of While loops. Later work by Hunt and Sands (ESOP'08) adapted the FST system to provide an erasure type system which determines whether some input is correctly erased at a designated time. This type system is inherently exponential, requiring a double typing of the erasure-labelled input command. In this paper we start by developing the FST work in two key ways: (1) We specialise the FST system to a form which only derives principal types; the resulting type system has a simple algorithmic reading, yielding principal security types in polynomial time. (2) We show how the FST system can be simply extended to check for various degrees of termination sensitivity (the original FST system is completely termination insensitive, while the erasure type system is fully termination sensitive).We go on to demonstrate the power of these techniques by combining them to develop a type system which is shown to correctly implement erasure typing in polynomial time. Principality is used in an essential way to reduce type derivation size from exponential to linear.},

year={2011},

}

** RefWorks **

RT Conference Proceedings

SR Electronic

ID 147149

A1 Hunt, S.

A1 Sands, David

T1 From Exponential to Polynomial-time Security Typing via Principal Types

YR 2011

T2 Lecture Notes in Computer Science. 20th European Symposium on Programming, ESOP 2011

SN 978-364219717-8

SP 297

OP 316

AB Hunt and Sands (POPL'06) studied a flow sensitive type (FST) system for multi-level security, parametric in the choice of lattice of security levels. Choosing the powerset of program variables as the security lattice yields a system which was shown to be equivalent to Amtoft and Banerjee's Hoare-style independence logic (SAS'04). Moreover, using the powerset lattice, it was shown how to derive a principal type from which all other types (for all choices of lattice) can be simply derived. Both of these earlier works gave "algorithmic" formulations of the type system/program logic, but both algorithms are of exponential complexity due to the iterative typing of While loops. Later work by Hunt and Sands (ESOP'08) adapted the FST system to provide an erasure type system which determines whether some input is correctly erased at a designated time. This type system is inherently exponential, requiring a double typing of the erasure-labelled input command. In this paper we start by developing the FST work in two key ways: (1) We specialise the FST system to a form which only derives principal types; the resulting type system has a simple algorithmic reading, yielding principal security types in polynomial time. (2) We show how the FST system can be simply extended to check for various degrees of termination sensitivity (the original FST system is completely termination insensitive, while the erasure type system is fully termination sensitive).We go on to demonstrate the power of these techniques by combining them to develop a type system which is shown to correctly implement erasure typing in polynomial time. Principality is used in an essential way to reduce type derivation size from exponential to linear.

LA eng

DO 10.1007/978-3-642-19718-5_16

LK http://www.cse.chalmers.se/~dave/papers/Hunt-Sands-ESOP11.pdf

OL 30