Sommaire

Défaut de code CWE-23

Expliquer en quoi consiste un vrai positif, un faux positif, un vrai négatif, et un faux négatif pour cet outil.

Vrai positif: le défaut de code est présent, et l’outil le détecte
Vrai négatif: le défaut de code n’est pas présent, et l’outil ne le détecte pas
Faux positif: le défaut de code n’est pas présent, mais l’outil le détecte
Faux négatif: le défaut de code est présent, mais l’outil ne le détecte pas

Quelles seraient les garanties données par l’outil s’il fonctionnait : …

Fuzzing : il faudrait une sorte d’instrumentation pour détecter l’accès à un fichier non autorisé. Par exemple, en traçant les appels système à open, et en ayant défini quels chemins sont autorisés. Il faudrait également que le fuzzer génère des entrées intéressantes pour ce défaut de code. Dans tous les cas, on ne peut pas couvrir toutes les possibilités d’entrées, et on aura donc des chemins inexplorés, donc des faux négatifs. Par contre, une erreur trouvée serait une vraie erreur, et on n’a donc pas de faux positifs.
Instrumentation : même raisonnement que pour le fuzzing
Exécution symbolique statique : en théorie, on n’a ni faux positifs, ni faux négatifs. Mais en pratique, dans le cas général, on ne peut pas explorer tous les chemins possibles, car ils sont potentiellement infinis. On va donc rater des chemins, et avoir des faux négatifs. Si l’implémentation est correcte, on n’aura pas de faux positifs.
Exécution symbolique dynamique : même raisonnement que pour le fuzzing, car on peut simplement voir l’exécution symbolique dynamique comme une forme de fuzzing.
Analyse de flot de donnée : on va devoir sur-approximer pour analyser le programme statiquement, on aura donc la présence de faux positifs. Mais, si l’implémentation est correcte, on n’aura pas de faux négatifs.

Représentation de programme

Les représentations graphiques sont disponibles ici

Exécution symbolique dynamique

Exécution 1

On choisi des valeurs initiales pour x et y, par exemple 0 et 0.

int f(int x, int y) {
  // store: x = 0, y = 0
  // store symbolique: x = a, y = b
  if (x > y) { // faux
    x = x + y;
    y = x - y;
    x = x - y;
    if (x - y > 0) {
      assert(0);
    }
  }
  // PC: !(a > b)
  return x;
}

Exécution 2

On a exploré dans l’exécution 1 le chemin avec la condition !(a > b). On l’inverse pour explorer le chemin avec la condition a > b. On génère donc les entrées suivantes, par exemple x = 1, y = 0.

int f(int x, int y) {
  // store: x = 1, y = 0
  // store symbolique: x = a, y = b
  if (x > y) { // vrai, PC = a > b
    x = x + y;
    // store: x = 1, y = 0
    // store symbolique: x = a + b, y = b
    y = x - y;
    // store: x = 1, y = 1
    // store symbolique: x = a + b, y = a
    x = x - y;
    // store: x = 0, y = 1
    // store symbolique: x = (a + b) - a = b, y = a
    if (x - y > 0) { // faux
      assert(0);
    } // PC = a > b && !(b - a > 0)
  }
  return x;
}

Exécution 3

On a donc exploré le chemin avec la condition a > b && !(b - a > 0). On inverse la dernière clause (car si on inverse la première, on se retrouve dans l’exécution 1) et on obtient a > b && b - a > 0. Si on donne cela a un solveur SAT, il nous dira unsat, car cela revient à trouver a et b tels que a > b && b < a, ce qui est impossible. Ce chemin n’est donc pas explorable.

Treillis

Définition

Ceci est une définition possible.

Éléments: \(\bot, \textit{Pair}, \textit{Impair}, \top\)

L’opérateur \(\sqcup\) est défini avec plusieurs règles:

\(\bot \sqcup x = x\)
\(x \sqcup \bot = x\)
\(\top \sqcup x = \top\)
\(x \sqcup \top = \top\)
\(x \sqcup x = x\)
\(\textit{Pair} \sqcup \textit{Impair} = \top\)
\(\textit{Impair} \sqcup \textit{Pair} = \top\)

La relation d’ordre \(\sqsubseteq\) est définie avec deux règles :

\(x \sqsubseteq \top\)
\(\bot \sqsubseteq x\)

Le digramme de Hasse est le suivant :

   ⊤
  /  \
Pair Impair
  \  /
   ⊥

Parité et signe

Si on souhaite raisonner sur la parité et le signe, on peut utiliser un treillis produit tel que défini dans le cours : \(\textit{Parité}\times\textit{Signe}\) où \(\textit{Parité}\) est le treillis défini a la question précédente, et \(\textit{Signe}\) est le treillis qu’on souhaite utiliser pour raisonner sur les signes.

Définition de +

L’opérateur \(\hat{+}\) est défini par la table suivante :

| + | \bot | Pair | Impair | \top | | \bot | \bot | \bot | \bot | \bot | | Pair | \bot | Pair | Impair | \top | | Impair | \bot | Impair | Pair | \top | | \top | \bot | \top | \top | \top |

Monotonicité

La monotonocité d’une fonction est définie par \(x \sqsubseteq x’ \implies f(x) \sqsubseteq f(x’)\). Pour une fonction à deux arguments (comme c’est le cas de \(\hat{+}\)), on a : \(x \sqsubseteq x’ \wedge y \sqsubseteq y’ \implies f(x, y) \sqsubseteq f(x’, y’)\).

Donc, pour que \(\hat{+}\) soit monotone, il faut que \(x \sqsubseteq x’ \wedge y \sqsubseteq y’ \implies x \hat{+} y \sqsubseteq x’ \hat{+} y’\).

On peut prouver que c’est vrai pour notre définition par une analyse de cas :

Si \(x = \bot\):
- On sait que \(\bot\) additionné à quoi ce soit donne \(bot\) (la ligne et colonne \(bot\) de notre table de définition ne contiennent que des \(\bot\)
- On doit montrer que \(x \hat{+} y \sqsubseteq x’ \hat{+} y\).
- Hors, ((x \hat{+} y = \bot\)
- Et \(\bot \sqsubseteq z\) est toujours vrai, ce qui prouve ce cas.
Si \(x = \top\):
- On sait que \(\top\) additionné à quoi ce soit donne soit \(\top\), soit \(\bot\) (uniquement dans le cas \(\top \hat{+} \bot\)).
- Dans le cas où on additionne à \(\bot\), on se retrouve \(\top \hat{+} \bot = \bot\), et le raisonnement est similaire au cas précédent : \(\bot \sqsubseteq z\) pour tout \(z\), donc ce cas est prouvé.
- Dans le cas où on obtient \(\top)\), on doit avoir un \(x’\) tel que \(\top \sqsubseteq x’\), donc on a obligatoirement \(x’ = \top\). On procède à un raisonnement similaire pour \(y\) et \(y’\), et cela prouve ce cas.
Si \(x = \textit{Pair}\)
- \(x’\) est soit \(\textit{Pair}\), soit \(\top\).
- Si \(x’ = \textit{Pair}\), il reste à montrer que \(\textit{Pair} \hat{+} y \sqsubseteq \textit{Pair} \hat{+} y’\), ce qui peut également se faire par une analyse de cas.
- Si \(x’ = \top\), on raisonne également par analyse de cas.
Si \(x = \textit{Impair}\), le raisonnement est le même.

Sur-approximation sûre

On introduit la fonction d’abstraction \(\alpha(n) = \textit{Pair}\) si n est pair, et \(\alpha(n) = \textit{Impair}\) si n est impair.

On souhaite prouver que \(\alpha(x + y) \sqsubseteq \alpha(x) \hat{+} \alpha(y)\).

On procède par analyse de cas, il n’y a ici que 4 cas : deux pour x pair, deux pour x impair :

x est pair, y est pair
- on veut \(\alpha(x + y) \sqsubseteq \alpha(x) \hat{+} \alpha(y)\)
- l’addition de deux nombres pairs donne un nombre pair, donc \(\alpha(x + y) = \textit{Pair}\)
- x est pair, donc \(\alpha(x) = \textit{Pair}\) (de même pour y)
- Donc, \alpha(x) \(\hat{+} \alpha(y) = \textit{Pair} \hat{+} \textit{Pair} = \textit{Pair}\)
- On a donc réduit chacun des côtés de l’inéquation à \textit{Pair}, ce qui prouve ce cas.
x est pair, y est impair
- on veut \(\alpha(x + y) \sqsubseteq \alpha(x) \hat{+} \alpha(y)\)
- l’addition d’un nombre pair avec un nombre impair donne un nombre impair, donc \(\alpha(x + y) = \textit{Impair}\)
- x est pair, donc \(\alpha(x) = \textit{Pair}\)
- y est impair, donc \(\alpha(y) = \textit{Impair}\)
- Donc, \alpha(x) \(\hat{+} \alpha(y) = \textit{Pair} \hat{+} \textit{Impair} = \textit{Impair}\)
- On a donc réduit chacun des côtés de l’inéquation à \textit{Impair}, ce qui prouve ce cas.
x est impair, y est pair : raisonnement similaire
x est impair, y est impair : raisonnement similaire

Eval

Il faut définir une fonction \(\textit{eval}\). Étant donné qu’on doit gérer le cas où on a des variables, ils nous faut une forme de store. Donc on va définir \(\textit{eval}(e, \sigma)\) où \(e\) et l’expression à évaluer, et \(\sigma\) est le store qui fait correspondre une valeur à chaque variable. \(\textit{eval})) retourne un élément du treillis \(\textit{Parité}\).

La définition est la suivante :

\(\textit{eval}(n, \sigma) = \alpha(n)\) si n est une constante constant
\(\textit{eval}(x, \sigma) = \sigma(x)\) si x est une variable
\(\textit{eval}(e_1 + e_2, \sigma) = \textit{eval}(e_1, \sigma) \hat{+} \textit{eval}(e_2, \sigma)\) où \(\hat{+}\) est l’opérateur d’addition défini plus haut.
\(\textit{eval}(e_1 * e_2, \sigma) = \textit{eval(e_1, \sigma) \hat{} \textit{eval}(e_2, \sigma)\) où \(\hat{}\) est l’opérateur de multiplication hypothétique sur notre treillis.

Analyse de flot de donnée

On traite dans ce qui suit \(\bot = \texttt{undef}\).

Le diagramme de Hasse est le suivant, dérivé depuis l’information que \(\texttt{undef} \sqsubseteq \texttt{def}\) :

undef
  |
 def

Depuis le diagramme de Hasse, il est évident que \(\texttt{def} \sqcup \texttt{undef} = \texttt{undef}\)
C’est une analyse forward, ce qui se voit à partir de la définition de la fonction \(\textit{Join}\), car on prends les valeurs précédentes. Pour raisonner sur la non-définition d’une variable, il faut raisonner sur son passé (« est-ce que x a été assigné avant le point de programme courant ? »).
C’est une analyse may, car elle répond à la question « est-ce la variable est potentiellement non-définie ? », car le fait qu’on a\(\texttt{def} \sqcup \texttt{undef} = \texttt{undef}\) implique que si on a une branche où x est assignée, et une autre branche où x n’est pas assignée, à la suite de cette branche, on a x qui a pour état \(\texttt{undef}\), indiquant que x est potentiellement non assigné. Voir le programme suivant pour exemple.

int x; // x: undef
if (cond) {
  x = 1; // x: def
} else {
  // x: undef
}
// x: undef
return x;

Pour la dernière question, le programme suivant est annoté avec les réponses :

     // x: bottom
1    int x;
     // x: undef
2    if (cond) {
       // x: bottom
3      x = 1;
       // x: def
4    }
     // x: undef
5    return x;