From Exponential to Polynomial-Time Security Typing Via Principal Types

Download Now Date Added: Jan 2011
Format: PDF

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.