Typing Secure Information Flow: Declassification and Mobility
Typage du flux d'information sûr: déclassification et mobilité
Résumé
We address the issue of confidentiality and declassification in a language-based security approach. We study, in particular, the use of refined type and effect systems for statically enforcing flexible information flow policies over imperative higher-order languages with concurrency. A general methodology for defining and proving the soundness of the type and effect system with respect to such properties is presented. We consider two main topics : The long-standing issue of finding a flexible information control mechanism that enables declassification. Our declassification mechanism takes the form of a local flow policy declaration that implements a local information flow policy. The largely unexplored topic of controlling information flow in a global computing setting. Our network model, which naturally generalizes the local setting, includes a notion of domain, and a standard migration primitive for code and resources. New forms of security leaks that are introduced by code mobility are revealed. In both the above settings, to take into account dynamic flow policies we introduce generalizations of non-interference, respectively named the non-disclosure and the non-disclosure for networks policies. Their implementation is supported by a concrete presentation of the security lattice, where confidentiality levels are sets of principals, similar to access control lists.
Nous nous intéressons au sujet de la confidentialité et de la déclassification. Nous étudions en particulier l'usage d'un système de types et d'effets pour assurer de manière statique des politiques de sécurité flexibles pour un langage d'ordre supérieur impératif avec concurrence. Une méthodologie générale pour définir et prouver la correction du système de types et d'effets pour de telles propriétés est présentée. Nous considérons deux points principaux : - La question de trouver un mécanisme flexible de contrôle d'information qui permet la déclassification. Notre mécanisme de déclassification prend la forme d'une déclaration de politique locale de flux qui implémente une politique locale de flux d'information. - La question jusqu'ici inexplorée de contrôler les flux d'information dans un environnement global. Notre modèle de réseau, qui généralise l'environnement global, inclut une notion de domaine et une primitive de migration standard pour le code et les ressources. De nouvelles formes de perte d'information, introduites par la mobilité du code, sont révélées. Dans les deux cas mentionnés ci-dessus, pour prendre en compte les politiques de flux globales nous introduisons des généralisations de la non-interférence, qui sont nommées non-divulgation et non-divulgation pour les réseaux. Ces généralisations sont obtenues `a l'aide d'une représentation concrète des treillis de sécurité, où les nivaux de confidentialité sont des ensembles de principaux, semblables `a des listes de contrôle d'accès.
Domaines
Loading...