Session Types for Access and Information Flow Control - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 2010

Session Types for Access and Information Flow Control

Résumé

We consider a calculus for multiparty sessions with delegation, enriched with security levels for session participants and data. We propose a type system that guarantees both session safety and a form of access control. Moreover, this type system ensures secure information flow, including controlled forms of declassification. In particular, it prevents leaks due to the specific control constructs of the calculus, such as session opening, selection, branching and delegation. We illustrate the use of our type system with a number of examples, which reveal an interesting interplay between the constraints of security type systems and those used in session types to ensure properties like communication safety and session fidelity.
Nous étudions un calcul pour modéliser des sessions à partenaires multiples, avec délégation, où les données et les partenaires sont équipés de niveaux de sécurité. Nous présentons un système de types pour ce calcul, garantissant à la fois la sûreté des sessions, une forme de contrôle d'accès et la sécurité du flux d'information, tout en permettant la déclassification des données lors de leur transmission. En particulier, ce système de types permet de prévenir les fuites d'information dues aux primitives spécifiques du langage, que sont l'ouverture de session, la sélection, le branchement et la délégation. Nous illustrons l'utilisation de notre système de types par une série d'exemples, qui révèlent une interaction intéressante entre les contraintes apparaissant dans les systèmes de types classiques pour la sécurité et celles utilisées dans les types de session pour assurer des propriétés telles que l'absence d'erreurs de communication au cours d'une session et la conformité d'une session à un protocole donné.
Fichier principal
Vignette du fichier
RR-7368.pdf (436.2 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00511304 , version 1 (25-08-2010)

Identifiants

  • HAL Id : inria-00511304 , version 1

Citer

Sara Capecchi, Ilaria Castellani, Mariangiola Dezani-Ciancaglini, Tamara Rezk. Session Types for Access and Information Flow Control. [Research Report] RR-7368, INRIA. 2010, pp.48. ⟨inria-00511304⟩
98 Consultations
217 Téléchargements

Partager

Gmail Facebook X LinkedIn More