Type abstraction and faceted types for declassification

Abstract

El tipado de seguridad para control de ujos de información previene que información con- dencial sea liberada hacia canales públicos. La propiedad fundamental de control de ujos de información, conocida como no-interferencia, de ne que un observador público no puede aprender nada sobre datos privados. No-interferencia es teóricamente muy atractiva , sin embargo, en la práctica: sistemas reales necesitan intencionalmente desclasi car alguna información, de forma selectiva. Entre los distintos enfoques de desclasi cación de ujos de información, uno particularmente expresivo es etiquetas-como-funciones que asegura una noción de no-interferencia relajada. Dicho enfoque permite a los programadores especi car políticas de desclasi cación, funciones, que capturan la forma intencional en que información pública puede ser calculada a partir de información privada. Motivado por el enfoque etiquetas-como-funciones, en esta tesis, nosotros proponemos un enfoque etiquetas-como-tipos para capturar políticas de desclasi cación de una manera simple y expresiva. En lugar de usar funciones como etiquetas, nosotros usamos tipos como etiquetas. Es decir, nosotros usamos tipos para indicar cuando un valor es público, privado o cuando es parcialmente desclasi cado. En consecuencia los tipos de seguridad son tipos con facetas, dígase un par de tipos que de nen las vistas de una valor para un observador privilegiado y un observador público respectivamente. Nosotros desarrollamos el enfoque de etiquetas-como-tipos usando mecanismos estándares de abstracción de tipos. Primero exploramos la forma de abstracción de tipos provista por subtipos en el contexto de programación orientada a objetos, donde los tipos de los objetos son interfaces, dígase un conjunto de métodos disponibles para el cliente de un objeto. Segundo, exploramos desclasi- cación basada en tipos para lenguajes funcionales, usando el mecanismo de abstracción de tipos provisto por los tipos existenciales. Finalmente, extendemos el enfoque de desclasi - cación para el contexto de orientación a objetos con polimor smo de etiquetas, formalizando una noción de polimor smo para desclasi cación. Las distintas realizaciones del enfoque etiquetas-como-tipos disfrutan una fuerte propiedad llamada no-interferencia relajada basada en tipos, la cual provee un principio de razonamiento modular para desclasi cación basada en tipos. El enfoque de etiquetas-como-tipos tiene el bene cio práctico de de nirse sobre conceptos que son bien conocidos para los desarrolladores (dígase tipos, subtipo, etc.) para construir sistemas con seguridad de ujos de información que limpiamente tengan en cuenta desclasi cación controlada y expresiva. Por tanto, esta tesis provee un fundamento necesario y sólido para integrar desclasi cación basada en tipos en lenguajes de programación existentes.

Information- ow security typing statically prevents con dential information from leaking to public channels. The fundamental information ow property, known as noninterference, states that a public observer cannot learn anything from secret data. As attractive as it is from a theoretical viewpoint, noninterference is impractical: real systems need to intentionally declassify some information, selectively. Among the di erent information ow approaches to declassi cation, a particularly expressive labels-as-functions approach was proposed, enforcing a notion of relaxed noninterference by allowing programmers to specify declassi cation policies, functions, that capture the intended manner in which public information can be computed from secret data. Motivated by the labels-as-functions approach, in this thesis, we propose a labels-as-types approach to capture declassi cation policies in a simple and expressive manner. Instead of using functions as labels, we use types as labels. That is, we use types to indicate when a value is public, secret or when it is partially declassi ed. Therefore security types are faceted types, i.e. a pair of types that de nes the views of a value to the privileged and public observers respectively. We develop the labels-as-types approach using standard type abstraction mechanisms such as subtyping, parametric types and existential types. We rst explore the form of type abstraction provided by subtyping in the setting of objectoriented programming, where object types are interfaces, i.e. the set of methods available to the client of an object. Second, we explore type-based declassi cation for functional languages, using the type abstraction mechanism provided by existential types. Finally, we extend the object-oriented type-based declassi cation approach to handle label polymorphism. As labels are types, label polymorphism reduces to type polymorphism; and as types are used to express declassi cation, we formalize a notion of declassi cation polymorphism. The di erent realizations of the labels-as-types approach enjoy a strong property called type-based relaxed noninterference, which provides a modular reasoning principle for typebased declassi cation. The labels-as-types approach has the practical bene ts of relying on concepts that are well-known to developers (i.e. types, subtyping, etc.) in order to build systems with information ow security that cleanly account for controlled and expressive declassi cation. Therefore, this thesis provides a necessary and solid basis to integrate typebased declassi cation in existing programming languages.