Non-interférence

Non-interférence dans le λ-calcul et le λ-calcul par valeur

Si M est un terme dont les différents sous-termes peuvent ˆetre publics ou secrets et si M se réduit vers une valeur V , l’enjeu de la non-interférence est de savoir si l’observation de cette valeur V , intuitivement publique, donne une information sur un sous-terme secret de M. Dans le cadre du λ-calcul, nous souhaitons examiner cette propriété intuitive en s’inspirant de l’approche des analyses de flot d’information telle que celle développée par Simonet et Pottier [37, 39]. Ces derniers garantissent une propriété de non-interférence en utilisant un typage dans lequel les types ont deux composantes : (1) un type `a la ML “classique” (par exemple, le type entier int) et (2) un niveau de sécurité qui permet de distinguer les termes secrets des termes publics. La propriété de non-interférence s’énonce informellement de la fa¸con suivante : si le terme M est du type entier public, si x est une variable libre de M dont le type est de niveau secret, si V et V ′ sont des valeurs de mˆeme type que x et si M{x\V } et M{x\V ′} se réduisent vers des entiers n et n ′ , alors ces entiers sont égaux. Ainsi, si la réduction de M{x\V } aboutit `a une valeur n, cette valeur n ne dépend pas de V et ne fournit donc aucune information sur V . Pour revenir `a l’intuition originale de Goguen et Meseguer, un changement d’une valeur secrète V en V ′ n’a pas d’effet visible du point de vue des valeurs publiques obtenues `a l’issue des réductions de M{x\V } et M{x\V ′}. Il est important de noter ici que le canal caché constitué par l’information selon laquelle la réduction de M{x\V } aboutit ou non `a une valeur, n’est pas pris en compte. Dans cette section, on s’inspire de la démarche de Simonet et Pottier pour définir une propriété de non-interférence dans le cadre du λ-calcul non typé. Dans le cadre des travaux de Simonet et Pottier, prouver la non-interférence d’un sous-terme V de M avec le résultat n de la réduction de M, consiste `a montrer que si en rempla¸cant V par une valeur (de mˆeme type que V ) quelconque V ′ , on obtient une valeur n ′ , alors les valeurs n et n ′ sont les mˆemes : on a n = n ′ . On souhaite adapter cette approche de la non-interférence au λ-calcul : si (C[ ],N) est un sous-terme de M et si M →→ V , montrer la non-interférence de N au cours de la réduction menant `a V consiste, informellement, `a montrer qu’en rempla¸cant N par N′ , si C[N′ ] →→ V ′ , alors les valeurs V et V ′ sont les mˆemes. Le λ-calcul et le λ-calcul par valeur ne contiennent pas de constantes telles que les entiers. Les seules valeurs sont les abstractions. Si la notion de “mˆeme valeur” est évidente pour les entiers, cette notion est moins claire dans le cas des abstractions. Pour illustrer ce sujet plus concrètement, on considère l’exemple des réductions des termes M = (λx.Iλy.x)V et M′ = (λx.Iλy.x)V ′ o`u I = V = λz.z et V ′ = λz.u. R : (λx.Iλy.x)V → Iλy.V → λy.V R′ : (λx.Iλy.x)V ′ → Iλy.V ′ → λy.V ′ Le terme M′ est le terme M o`u la valeur V a été changé en V ′ . Les valeurs finales des réductions R et R′ ne sont pas égales. Pourtant, les valeurs V et V ′ n’ont participé `a aucune réduction. Intuitivement, les valeurs λy.V et λy.V ′ sont identiques `a un sous-terme (strict) près. Ces valeurs ont été obtenues de la mˆeme fa¸con. Pour distinguer ces valeurs plus clairement, on pourrait utiliser le contexte C0[ ] = ([ ]I)I. On a C0[λy.V ] →→ I et C0[λy.V ′ ] →→ u. Ce contexte permet de distinguer ces résultats puisque dans le premier cas, on obtient une valeur, au contraire du deuxième cas. Cependant cette distinction est le fruit d’une interaction entre le contexte C[ ] et les sous-termes V et V ′ . En d’autres mots, le contexte C[ ] a interféré avec V et V ′ . En revanche, les sous-termes V et V ′ de M et M′ n’interfèrent pas dans les réductions R et R′ . Ceci nous amène `a ignorer les 110 Non-interférence sous-termes stricts des valeurs obtenues et `a définir dans ce but la notion d’observable. O(λx.M) = λx.Ω L’observable d’une abstraction est l’abstraction λx.Ω. Avec cette définition, on peut donner une première tentative de définition de la propriété d’interférence dans le λ-calcul, qui s’inspire de la définition informelle donnée précédemment. Enoncé 5.1 (Non-interférence) Le sous-terme (C[ ],N) de M n’interfère pas dans la réduction M = C[N] →→ V si et seulement si, pour tout N′ , la réduction C[N′ ] →→ V ′ implique la relation O(V ) = O(V ′ ). Un sous-terme n’interfère pas dans une réduction aboutissant `a une valeur si, une modification de ce sous-terme ne permet pas d’obtenir une valeur dont l’observable est différent. Comme dans le cas des analyses de flot d’information, on ne tient pas compte ici du canal caché que constitue l’information d’aboutissement vers une valeur. Plus concrètement, on ignore les cas o`u, en rempla¸cant N par N′ dans M, la réduction n’aboutit pas `a une valeur. Ceci se traduit dans la définition de l’interférence par le fait que la convergence de C[N′ ] vers une valeur est une hypothèse. La définition de l’observable d’une valeur et l’énoncé précédent soulèvent toutefois une difficulté : toutes les valeurs, c’est-`a-dire toutes les abstractions ont le mˆeme observable. Si on adoptait ces définitions, dans l’exemple de la réduction de M = (λx.Iλy.x)V , on obtiendrait que M n’interfère pas dans la réduction M →→ λy.V . En effet, en rempla¸cant le sous-terme M par un terme N quelconque et en supposant N →→ W, on a O(λy.V ) = O(W) = λy.Ω. Intuitivement, les valeurs λy.V et W ne sont pourtant pas les mˆemes. La notion d’observable utilisée ici ne capture pas cette intuition. On peut rapprocher cette imprécision des co¨ıncidences syntaxiques mentionnées dans la partie 1.3. Dans ce dernier cas, les étiquettes du λ-calcul permettent de distinguer des termes accidentellement identiques. Ainsi, le terme I(Ix) peut se réduire de deux fa¸cons différentes vers Ix. Ces termes Ix sont bien syntaxiquement égaux mais ne sont pas intuitivement les mˆemes. Dans le cas présent, on exploite aussi les étiquettes du λ-calcul pour pouvoir identifier les valeurs et plus particulièrement leur origine. On se place donc dans le λ-calcul étiqueté et on définit l’observable d’une valeur étiquetée de la fa¸con suivante. O((λx.M) α ) = (λx.Ω)α.

Le λm-calcul

Dans cette section, on examine informellement la propriété de non-interférence pour un langage inspiré de Core ML [37, 39] : le λm-calcul. Ce langage, fondé sur le λ-calcul présenté dans la section 1.1, dispose en plus de δ-règles pour les opérations arithmétiques et conditionnelles, et de traits impératifs dans le langage afin de pouvoir effectuer des affectations ou des lectures en mémoire. Nous aurions pu traiter dans une section intermédiaire le cas d’un λ-calcul augmenté seulement des δ-règles arithmétiques et conditionnelles. Cependant, comme l’ajout de ces traits fonctionnels ne change pas fondamentalement la situation par rapport au λ-calcul par valeur étudié dans la section 5.1, nous avons préféré ajouter ces δ-règles en mˆeme temps que les traits impératifs. Comme nous le verrons par la suite, la présence d’effets de bord change radicalement la nature de la question de la non-interférence. La syntaxe du langage étudié dans cette section, le λm-calcul, est décrite sur la figure 5.3. Pour alléger au maximum les notations de ce chapitre, on se permet de réutiliser certaines notations du λ-calcul (Λ,V,. . . ), dans la mesure o`u le contexte ne laisse aucune ambigu¨ıté. En plus des variables, abstractions et applications du λ-calcul, on ajoute les entiers n, l’addition M + N et le test ifz M then N else P qui porte sur la nullité d’un entier. On ajoute également des traits impératifs. Dans le λm-calcul, on dispose d’un ensemble dénombrable d’adresses M. Ces adresses, notées m, représentent les emplacements de la mémoire. Formellement, une mémoire est une application µ définie sur un sous-ensemble fini de M et qui associe une valeur `a chaque adresse de l’ensemble de définition dom(µ) de µ. Pour une bonne lisibilité, une mémoire µ sera notée 114 Non-interférence µ = {mi 7→ Vi}i∈I . Si la mémoire µ étend la mémoire µ ′ sur l’adresse m, on notera le produit tensoriel correspondant µ = (µ ′ ; m 7→ V ). La mémoire vide sera notée ∅. Pour manipuler la mémoire, quatre nouveaux types de termes sont ajoutés dans la syntaxe du λm-calcul. Les adresses m sont intuitivement absentes des termes initiaux. Elles sont créées au cours de la réduction par les références ref(M). L’affectation M:=N permet de modifier la valeur associée `a une adresse. La déréférence !M permet d’accéder `a la valeur associée dans la mémoire `a une adresse. Le terme Unit est ajouté pour les réductions qui ne produisent pas de résultat, par exemple l’affectation. Dans ce calcul, les valeurs sont les abstractions, les entiers, les adresses ou Unit. La réduction → du langage est définie sur la figure 5.4. Cette réduction met en relation deux configurations constituées chacune d’un terme et d’une mémoire. La règle (βm) est reprise du λ-calcul par valeur. L’opération de substitution du λ-calcul est étendue sur les nouveaux termes par la définition de la figure 5.5. Dans le λm-calcul, du fait de la définition de la (βm)-réduction, on ne substitue aux variables que des valeurs. On note que l’ordre d’évaluation est fixé par la règle de contexte (Ctx). Les contextes d’évaluation, définis sur la figure 5.6, imposent une évaluation de gauche `a droite sur les applications et les affectations. L’utilisation d’un ordre d’évaluation est dictée par la présence des effets de bord qui rendent le langage non confluent. Par exemple, la réduction de la configuration ((λy.λx.!m)(m:=2))(m:=0))/(m 7→ 1) peut aboutir `a 0, 1 ou 2 selon l’ordre d’évaluation choisi. La δ-règle (Plus) effectue l’addition de deux entiers. Si n est l’entier 0, la réduction de ifz n then M else N par la δ-règle (Ifz-true) aboutit au terme M. Si le test de nullité échoue, le terme N est obtenu par la règle (Ifz-false). Les règles décrites jusqu’`a présent ne modifient pas la mémoire. La mémoire est modifiée par trois règles. La réduction de la configuration ref(V )/µ par la règle (Ref) ajoute une nouvelle adresse m `a la mémoire µ et retourne cette adresse. Cette adresse est fraˆıche : elle n’appartient pas au domaine de µ. Hormis cette contrainte, le choix de m n’est pas spécifié. La valeur V lui est associée dans la mémoire (µ; m 7→ V ) obtenue. La réduction d’une configuration m:=V/(µ; m 7→ V ′ ) par la règle (Assign) change la valeur associée par la mémoire `a l’adresse m. La nouvelle mémoire associe V `a m. Le résultat de la réduction est Unit. La réduction d’une déréférence !m/(µ; m 7→ V ) par la règle (Deref) permet d’accéder `a la valeur associée `a l’adresse m par la mémoire. On illustre le langage et les difficultés engendrées pas les effets de bord en étudiant la réduction du terme M = (λy.(λ .!y) 1) ref(0) qui est illustrée sur la figure 5.7. Pour représenter la mémoire de fa¸con intuitive, on utilise une bande horizontale pour chaque adresse mémoire. Les opérations d’écriture sont matérialisées par une flèche annotée par E alors que les opérations de lecture sont matérialisées par une flèche annotée par L. La première réduction de M réduit la référence ref(0) ce qui ajoute `a la mémoire une nouvelle adresse m1. Cette dernière est associée en mémoire `a la valeur 0. La deuxième réduction est une (βm)-réduction. L’adresse m1 est substituée sous la déréférence. La troisième réduction est également une (βm)-réduction. Comme le corps de l’abstraction contractée ne contient pas la variable liée, l’argument 1 disparaˆıt. On en déduit intuitivement que ce sous-terme n’intervient pas dans le résultat final. La dernière réduction est une déréférence de l’adresse m1. La valeur associée `a m1 dans la mémoire est lue et donne la valeur finale de la réduction. Deux observations sont retenues de cet exemple : (1) le sous-terme 1 de M n’a pas contribué `a la valeur finale. (2) L’adresse m1 a participé `a l’obtention de la valeur finale. Comme on l’a vu dans la section précédente, pour exprimer une propriété de non-interférence sur une réduction, il faut identifier les sous-termes du terme initial qui influencent la valeur finale. Si un sous-terme n’influence pas cette valeur, c’est-`a-dire si la modification de ce sous-terme ne change pas l’observable de la valeur finale, alors ce sous-terme n’interfère dans cette valeur. Intuitivement, l’observation (1) nous pousse `a émettre l’hypothèse suivante : le sous-terme 1 n’interfère pas dans la réduction R.