Mots clés. sécurité, vérification de bytecode, algorithme de Kildall, ...

Note. Vous pouvez télécharger une version pdf de ce rapport.

 Table des matières

• 1  Introduction
• 2  Le langage étudié
  • 2.1  Les types
  • 2.2  Les fonctions
    • 2.2.1  Les expressions
    • 2.2.2  Les filtrages
• 3  Un compilateur pour le langage
  • 3.1  Mise en oeuvre
  • 3.2  Génération des contraintes et calcul du type de retour
  • 3.3  Résolution du système d'affectations
• 4  La machine virtuelle
• 5  Vérification du bytecode : algorithme de Kildall
  • 5.1  Préliminaires
  • 5.2  L'algorithme de Kildall
• 6  Applications de l'algorithme de Kildall : vérifications de type et de forme
  • 6.1  Vérification de type
  • 6.2  Vérification de forme
    • 6.2.1  Les états
    • 6.2.2  La fonction de flot
• 7  Conclusion
• 8  Références

 1  Introduction

 2  Le langage étudié

 2.1  Les types

  type tnat = Z | S of tnat;;
  type env = Nil | C of tnat * env;;

 2.2  Les fonctions

 2.2.1  Les expressions

 2.2.2  Les filtrages

function add(x,y) = match x with
Z -> y // si x = 0 add(x,y)=y
|
S(u) -> add(u, S(y)) //add(u+1,y)=add(u,y+1)
;;

 3  Un compilateur pour le langage

• les types définis explicitement dans le programme (on dira par la suite que ces types sont connus)
• les types polymorphes, c'est-à-dire qui dépendent de certains paramètres

 3.1  Mise en oeuvre

 3.2  Génération des contraintes et calcul du type de retour

• Soit une expression qui peut être :
  • une variable
  • un constructeur avec ses arguments éventuels
  • une fonction avec ses arguments
• Soit un filtrage constitué d'une variable, d'un motif auquel on identifie la variable, et de deux corps (le premier s'exécute si l'identification réussit, l'autre en cas d'échec); le premier bloc sera appelé bloc positif et le deuxième bloc négatif. Par la suite, ce filtrage sera noté Match(v, m, body₁, body₂).

• Si le corps de la fonction est une expression e :
  Le type de celle-ci est le type de retour de la fonction. e peut avoir plusieurs formes :
  • si e est une variable v : dans ce cas, le type de e est celui de v (type pris dans l'environnement courant)
  • si e = c(e₁,…, e_n ) (où c est un constructeur et chacun des e_i une expression) : si les types inférés (des arguments du constructeur) sont égaux aux types attendus, alors le type de e est celui du constructeur c, sinon il y a une erreur de typage.
  • si e = f(e₁,…, e_n) (où f est un symbole fonctionnel) : le type de e est le type de retour de f, si celle-ci est bien typée et que les types des arguments e₁,…,e_n sont compatibles avec la signature de f. Pour cela, on cherche le prototype de f dans la liste des signatures précédemment calculées. S'il n'y est pas, on suppose que le prototype de f est le plus général possible. Puis on le recalcule afin de préciser ses types.
• Si le corps de la fonction est un filtrage :
  Soient v la variable à filtrer, m le motif auquel on identifie v, body₁ le bloc positif et body₂ le bloc négatif. Les contraintes induites directement par le principe d'exécution d'un filtrage sont :
  • la variable v est de même type que le motif m (puisqu'on les identifie)
  • les deux blocs body₁ et body₂ sont de même type. En effet, si le filtrage réussit, le type de retour de la fonction sera égal au type de body₁. Dans le cas contraire, le type de retour de la fonction sera égal au type de body₂. Or le type de retour pour une fonction donnée est unique.

• type de v =type de m
• type de body1 = type de body2

• Soient t_1, …, t_n les types des arguments de c (dans la déclaration des types du programme source). Alors pour tout i, t_i = type de e_i

• Soient t_1, …, t_n les types des arguments de f (dans la liste des signatures). Alors pour tout i, t_i = type de e_i

• Si m est de type connu (ie, ce n'est pas une variable de type) alors :
  • si le type de v est connu et que les types de v et m ne sont pas les mêmes, alors le bloc est mal typé.
  • si le type de v est une variable de type alors on rajoute la contrainte type de v ←type de m
• Si le type de m est une variable de type : soient t₁ et t₂ les types de v et m et soit t le résultat de l'unification entre t₁ et t₂. Si t₁=t, alors, on rajoute la contrainte t₂← t₁, sinon (t₂=t) on rajoute la contrainte t₁← t₂.
• Si le type de b₁ et le type de b₂ sont deux types connus et différents, alors la fonction est mal typée.
  Sinon : soient t₁ et t₂ les types des blocs b₁ et b₂ et soit t le résultat de l'unification entre t₁ et t₂.
  • si t₁=t, alors, on rajoute la contrainte t₂← t₁
  • si t₂=t, alors, on rajoute la contrainte t₁← t₂.

• si t_i et τ_i sont connus et différents alors l'expression est mal typée
• sinon : soit u_i l'unification de t_i et τ_i
  • si t_i = u_i alors on rajoute la contrainte τ_i ← t_i
  • sinon on rajoute la contrainte t_i ← τ_i

 3.3  Résolution du système d'affectations

• Si t₂ ≠ t alors rajouter (t₁, t₂ ) à ls
• Sinon si t' ≠ t₁ alors rajouter (t₁, t') à ls

• Si t = t' alors retourner ls
  
• Sinon si ∀ ( v, v' ) ∈ ls, v ≠ t'alors up ← t'
  sinon soit up le second membre de la première occurence d'un couple (t, t'' )
  retourner (t, up)::(propa (t, up) ls

• Si t = t' alors retourner ls
  
• Sinon si ∀ (v, v') ∈ ls, v ≠ t alors retourner propa (t,t') ls
  sinon soit t'' le second membre de la première occurence d'un couple ( t, t''' )
  up← unification(t', t'')
  ls₁ ← apply_equation (t, up) ls
  ls₂ ← apply_equation (t', up) ls₁
  ls ← apply_equation (t'', up) ls₂
  retourner ls

 4  La machine virtuelle

1. Branch (c, j) : branchement conditionnel (traduction du match)
   Identifie le sommet de la pile avec le constructeur c. Si le branchement réussit, c'est-à-dire que le sommet de la pile est de la forme c(a₁,…,a_n), on dépile l'élément au sommet, puis on empile les arguments a₁,…,a_n de c et l'instruction suivante est exécutée, sinon, on saute à l'instruction j.
2. Build (c, n) : appel à un constructeur c d'arité n
   Les n arguments (arg₁, …, arg_n) nécessaires à l'appel du contructeur sont dépilés (si la taille de la pile est insuffisante, la VM renverra une erreur). Ensuite, la valeur c(arg₁,…,arg_n) est empilé.
3. Call(f, n) : appel à une fonction f d'arité n
   On dépile les n éléments (a₁, …, a_n ) en sommet de pile (si la pile n'est pas assez grande, la VM renvoie une erreur) puis on empile le résultat de l'évaluation de f(a₁, …, a_n), celle-ci étant effectuée sur une nouvelle pile d'exécution.
4. Load(i) : chargement d'une valeur d'adresse i
   La VM empile la i-ième valeur de la pile.
   
5. Stop : arrêt de la machine
   La VM arrête l'analyse du bloc de la fonction en cours d'exécution. Un cas typique est l'apparition d'une erreur.
6. Return : retour de résultat
   L'analyse du bloc en cours s'arrête et l'état courant est retourné.

 5  Vérification du bytecode : algorithme de Kildall

 5.1  Préliminaires

• ≤ est un ordre partiel sur Σ. Intuitivement, dire que s₁ ≤ s₂ pour 2 états s₁ et s₂, cela signifie que s₁ est au moins aussi cohérent que s₂.
• sup est une loi interne binaire sur Σ, et sup(s₁, s₂) est la borne supérieure de s₁, s₂ (selon la loi ≤)
• ∀ s ∈ Σ, s ≤ ⊤ (tout état est plus cohérent que l'état inconsistant)
• Il n'existe aucune suite infinie strictement décroissante d'états s₁ > s₂ > … > s_n > …, où > est la relation définie par: ∀ (s₁, s₂ ) ∈ Σ², ( s₁ > s₂ ) ⇐⇒ (s₂ ≤ s₁∧ s₁ ≠ s₂ ). On notera au passage que > est la relation moins cohérent que.

• boolean est le type des booléens, ne contenant que les éléments true et false.
• N list est le type des listes d'entiers naturels et Σ list celui des listes d'états. En particulier, le type programme est une partie de Σ list.
• Étant donné une liste ls et un élément e, e::ls est la liste obtenue en insérant e au début de ls.
• Soit ls une liste à m éléments et k un entier.
  • Si k ∈ {0,1,...,m−1} , ls[k] est le (k+1)-ième élément de ls
  • Si k≥ m, ls[k] est un paramètre arbitrairement fixé.

• Le graphe de flot d'un bytecode bc est un graphe orienté F, dont les sommets sont les numéros des instructions de bc et tel que, pour tous sommets i et j de F,(i, j) est un arc de F si et seulement si l'instruction j peut être exécutée juste après l'instruction i.
• succs: N → N list. Pour un noeud p du graphe de flot du bytecode en cours de vérification, succs(p) renvoie la liste des noeuds successeurs de p.
• step: N ∗ Σ → (N ∗ Σ ) list. Il s'agit de la fonction de flot. step(p, s) calcule la liste de tous les couples (k,s_k), où k est un successeur de p et s_k l'état obtenu en exécutant l'instruction p à partir de l'état s.
• correct: programme ∗ N → boolean. correct(ss, p) = true si et seulement si le p-ième état de ss est correct.
• correctprog: programme → boolean. Un programme est correct si et seulement si tous ses états sont cohérents et corrects:
  correctprog(ss)⇐⇒ ∀ p, 1 ≤ p ≤ n, ss[p]≠ ⊤ ∧ correct(ss, p).
• On étend la définition de la relation ≤ sur Σ list:
  • [ ] ≤ [ ]
  • ∀ (s₁, s₂) ∈ Σ², ∀ (ls₁, ls₂ ) ∈ (Σ list)², (s₁ ≤ s₂ ∧ ls₁ ≤ ls₂ )⇒ (s₁ :: ls₁ ≤ s₂ :: ls₂ ).

 5.2  L'algorithme de Kildall

• Entrées:
  • un programme ss, i.e une liste de n états
  • un code bcode de n instructions
  • une relation ≤ sur Σ
  • une loi sup sur Σ
  • une fonction de flot step
• Sortie: un programme reslt
• Spécifications: reslt est obtenu à partir de ss en remplaçant les états associés aux instructions instables de bcode par les états calculés à partir de leurs prédecesseurs.
  
• Méthode:
  // 1. Initialisation
  wl← Ø
  reslt← ss
  // Génération de la work list
  Pour chaque numéro d'instruction p dans bcode faire
      Si p n'est pas stable alors wl← wl ∪ {p}
  fin pour
  Tant que wl≠ Ø faire
      Extraire un numéro d'instruction p de wl
      // 2. Propagation
       sucp← step(ss, p) //calculer les successeurs de p
      Pour chaque couple (q,s) de sucp faire
           up ← sup(ss[q], s)
           Si up ≠ ss[q] alors // q n'est donc pas encore stable
                 wl← wl ∪ {q}
           reslt← replace(reslt, q,up)
      fin pour
  fin tant que
  retourner reslt

 6  Applications de l'algorithme de Kildall : vérifications de type et de forme

• ∀ s ∈ Σ, ⊥ ≤ s
• ∀ s ∈ Σ, s ≤ ⊤
• ∀ s₁, s₂ ∈ Σ \ { ⊥, ⊤ }, s₁ ≤ s₂ ⇐⇒ s₁ = s₂

• ∀ s ∈ Σ, sup( s, ⊥ ) = s
• ∀ s ∈ Σ, sup( s, ⊤ ) = ⊤
• ∀ s₁, s₂ ∈ Σ \{ ⊥, ⊤ }, sup( s₁, s₂ ) = s₁  si  s₁ = s₂ sinon sup( s₁, s₂ ) = ⊤

 6.1  Vérification de type

  (* succ : prend en argument un entier x et renvoie x+1 *)
  let succ (x) = S (x);;

  Load 0;
  Build (S,1);
  Return;

1. Branch c j :
   fstep (p,s) =
   • si s = ⊥ alors [⊥ ; ⊥ ]
   • si s = ⊤ alors [ ⊤ ; ⊤ ]
   • si s ∈ S alors
     • si s est de la forme l@[rt] alors
       soit (t₁, …, t_n ) → t la signature de c
       si rt = t alors [l@[ t₁, …, t_n ] ; s ]
       sinon [⊤ ; ⊤]
       
     • sinon [ ⊤ ; ⊤ ]
   
   
2. Build c n :
   fstep (p,s) =
   • si s = ⊥ alors [ ⊥ ]
   • si s = ⊤ alors [ ⊤ ]
   • si s ∈ S alors
     • si s est de la forme l@[ts₁,...,ts_n] alors
       soit ( t₁, …, t_n )→ t la signature de c
       si ∀ i, 1 ≤ i ≤ n, compatibles (t_i,ts_n) alors [l@[t]]
       sinon [ ⊤ ]
       
     • sinon [⊤]
3. Call g n :
   fstep (p,s) =
   • si s = ⊥ alors [⊥]
   • si s = ⊤ alors [ ⊤ ]
   • si s ∈ S alors
     • si s est de la forme l@[ts₁,...,ts_n] alors
       soit s = ( t₁,…, t_n ) → t, la signature de f
       rt ← Compatibility s [ts₁,...,ts_n]
       s'il y a erreur alors [⊤]
       sinon [l@rt]
       
     • sinon [ ⊤ ]
4. Load j :
   fstep (p,s) =
   • si s = ⊥ alors [⊥]
   • si s = ⊤ alors [⊤]
   • si s ∈ S alors
     si s est de la forme [ts₁,...,ts_n] alors [ts₁,...,ts_n,ts_j]
     sinon [⊤]
5. Stop : fstep (p,s) =[ ]
6. Return :
   fstep (p,s) =
   • si s = ⊥ alors [⊥]
   • si s = ⊤ alors [⊤]
   • si s ∈ S alors
     • si s est de la forme l@[rt] alors
       soit s = ( t₁,…, t_n ) → t la signature de f
       si rt = t alors l@[rt]
       sinon [⊤]
       
     • sinon [⊤]

 6.2  Vérification de forme

 6.2.1  Les états

 6.2.2  La fonction de flot

1. Return :
   fstep (p,s) =
   • si s = ⊥ alors [⊥]
   • sinon
     • si s est de la forme ls@[e], σ alors [s]
       
     • sinon [⊤]
2. Stop : fstep (p,s) = [ ]
3. Load j :
   fstep (p,s) =
   • si s = ⊥ alors [⊥ ]
     
   • sinon
     • si s est de la forme (ls,σ )alors
       si j < n alors [(ls@[ls[j]], σ )]
       sinon [⊤]
       
     • sinon [⊤]
4. Build c m :
   fstep (p,s) =
   • si s = ⊥ alors [⊥]
     
   • sinon
     • si s est de la forme (ls@[e₁, e₂, …, e_m], σ) alors [(ls@[c(e₂, …, e_m)], σ)]
       
     • sinon [⊤]
5. Call g m :
   fstep (p,s) =
   • si s = ⊥ alors [⊥]
   • sinon
     • si s est de la forme (ls@[e₁, e₂, …, e_m], σ) alors [(ls@[g(e₂, …, e_m)], σ)]
     • sinon [⊤]
6. Branch c label :
   fstep (p,s) =
   • si s = ⊥ alors [⊥;⊥]
   • sinon
     • si s est de la forme (ls@[v], σ) alors
       soit vars := new_vars (arity(c))
       soit e := c(vars)
       retourner [(ls[v:=e]@vars,[(v,e)]∘ σ); s]
       
     • sinon
       si s est de la forme (ls@[cons(ls₁)], σ) alors
       • si cons = c alors [(ls@ls₁, σ); s]
       • sinon [⊥;s]
       
       sinon [⊤;⊤]

 7  Conclusion

 8  Références

This document was translated from L^AT_EX by H^EV^EA.