Subject: Implémentation sécurisée de programmes distribués. Jour: 13/03/98 (Vendredi 13 mars) http://pauillac.inria.fr/bin/calendar/Seminaires S E M I N A I R E ____ ____ ___ / _ _ / __ __ /_ _ / / | _ __ _ / / \ / \ ___ / / | / /_ / __| / ___ /___/ __| / | __| |___ |_/ |_/ |____ / / __/ |_ |_/ |_ / |_/ / |_/ / / I N R I A - Rocquencourt, Salle de confe'rence du batiment 11 Vendredi 13 mars, 10h30 -------------- Cedric Fournet -------------- INRIA-Rocquencourt ================================================== Implémentation sécurisée de programmes distribués. ================================================== En collaboration avec Martin Abadi (DEC/SRC) et Georges Gonthier (INRIA Rocquencourt) Dans la plupart des applications distribuées, la communication entre machines s'exprime à l'aide d'abstractions telles que les canaux de communications ou les appels distants (remote procedure call, remote method invocation). L'implémentation de ces abstractions en termes d'opérations plus primitives fournit des garanties de sécurité plus ou moins fortes, par exemple en encryptant certains messages. Nous étudions ces propriétés de sécurité dans le cas des canaux de communication. Nous présentons d'abord un langage de haut niveau permettant de créer et de communiquer des canaux (avec de fortes garanties implicites de sécurité); ce langage est une variante du join-calcul, un calcul de processus adapté à la programmation distribuée. Nous montrons comment traduire systématiquement des programmes écrits dans ce langage vers un langage de plus bas niveau qui utilise des primitives cryptographiques. Notre traduction remplace chaque communication sur un canal sécurisé par plusieurs communications encryptées sur un canal public. Nous établissons un résultat de correction pour nos traductions. Ce résultat permet en particulier d'étudier dans le langage de haut niveau les propriétés sécuritaires qui apparaissent dans l'implémentation distribuée, sans prendre en compte les protocoles cryptographiques sous-jacents.