Abstract
In this paper, we develop a novel notion of dependent information flow types. Dependent information flow types fit within the standard framework of dependent type theory, but, unlike usual dependent types, crucially allow the security level of a type, rather than just the structural data type itself, to depend on runtime values. Our dependent function and dependent sum information flow types provide a direct, natural and elegant way to express and enforce fine grained security policies on programs, including programs that manipulate structured data types in which the security level of a structure field may depend on values dynamically stored in other fields, still considered a challenge to security enforcement in software systems such as data-centric web-based applications. We base our development on the very general setting of a minimal λ-calculus with references and collections. We illustrate its expressiveness, showing how secure operations on relevant scenarios can be modelled and analysed using our dependent information flow type system, which is also shown to be amenable to algorithmic type checking. Our main results include type-safety and non-interference theorems ensuring that well-typed programs do not violate prescribed security policies.
Original language | English |
---|---|
Title of host publication | POPL 2015 - Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages |
Place of Publication | New York |
Publisher | ACM - Association for Computing Machinery |
Pages | 317-328 |
Number of pages | 12 |
Volume | 2015-January |
ISBN (Electronic) | 978-1-4503-3300-9 |
DOIs | |
Publication status | Published - 14 Jan 2015 |
Event | 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015 - Mumbai, India Duration: 12 Jan 2015 → 18 Jan 2015 |
Conference
Conference | 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015 |
---|---|
Country/Territory | India |
City | Mumbai |
Period | 12/01/15 → 18/01/15 |
Keywords
- Dependent type systems
- Information flow