Dependent information flow types

Luísa Lourenço, Luís Caires

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

28 Citations (Scopus)

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 languageEnglish
Title of host publicationPOPL 2015 - Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
Place of PublicationNew York
PublisherAssociation for Computing Machinery
Pages317-328
Number of pages12
Volume2015-January
ISBN (Electronic)978-1-4503-3300-9
DOIs
Publication statusPublished - 14 Jan 2015
Event42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015 - Mumbai, India
Duration: 12 Jan 201518 Jan 2015

Conference

Conference42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015
CountryIndia
CityMumbai
Period12/01/1518/01/15

Keywords

  • Dependent type systems
  • Information flow

Cite this