INF889A - Révisions

Sommaire

Garanties

Considérons un outil de détection de défaut de code.

Expliquer en quoi consiste un vrai positif, un faux positif, un vrai négatif, et un faux négatif pour cet outil.
Quelles seraient les garanties possibles données par l’outil s’il fonctionnait :
- en se basant sur le fuzzing ?
- en se basant sur l’exécution symbolique statique ?
- en se basant sur l’exécution symbolique dynamique ?
- en se basant sur l’analyse de flot de donnée ?

Représentation de programme

Soit la fonction suivante :

int f(int x, int y) {
  if (x > y) {
    x = x + y;
    y = x - y;
    x = x - y;
    if (x - y > 0) {
      assert(0);
    }
  }
  return x;
}

Représenter son CFG
Représenter son arbre d’exécution
Faire une exécution dynamique symbolique en traitant x et y comme entrée symbolique
Quelle entrée permet d’atteindre la ligne assert(0) ?

Treillis de parité

On souhaite raisonner sur la parité des nombres utilisés dans un programme. Un nombre est soit pair, soit impair.

Définir un treillis “Parité” qui permet de raisonner sur la parité d’un nombre.

donner ses éléments
définir l’opérateur \(\sqcup\)
définir l’opérateur \(\sqsubseteq\)
représenter le treillis par son diagramme de Hasse

Si on souhaite raisonner à la fois sur la parité et sur le signe d’un nombre, que peut-on faire ? Détailler.
Définir sur ce treillis (parité et signe) l’opérateur \(\hat{+}\) qui est une sur-approximation de l’addition de deux nombres.
Énoncer la propriété de monotonicité pour \(\hat{+}\)
Démontrer que votre définition de \(\hat{+}\) est monotone.
Énoncer la propriété qui permet de s’assurer que \(\hat{+}\) est une sur-approximation sûre.
Prouver que votre définition de \(\hat{+}\) est une sur-approximation sûre.
Définir sur ce treillis (parité et signe), la fonction \(\textit{eval}\) qui permet d’évaluer les éléments syntaxiques suivants :

une constante (par exemple, 42)
une variable (par exemple, x)
une addition (par exemple, x + 1)
une multiplication (par exemple, x * y). On peut faire l’hypothèse de l’existence d’un opérateur de multiplication sur notre treillis.

Treillis de taille de chaîne de caractère

On souhaite ajouter des chaînes de caractères à MiniC. On ajoute les constructions suivantes au langage :

Création d’une chaîne de caractère entre guillemets, par exemple "hello"
Concaténation de chaînes de caractères, par exemple concat("hello ", "world"), qui retourne une nouvelle chaîne de caractère "hello world"
Extraction d’une sous-chaîne de caractère, par exemple substr("hello", 1, 3) qui retourne une nouvelle chaîne de caractère "ell"

On s’intéresse particulièrement à la longueur des chaînes de caractères. Proposer un treillis qui permette :

De représenter les nombres qui sont constants
De représenter les chaînes de caractères par leur longueur

Définir:

Les éléments de ce treillis
La relation d’ordre (\(\sqsubseteq\))
La plus petite borne supérieure entre deux éléments (\(\sqcup\))
Une fonction d’abstraction (\(\alpha\)) afin d’avoir une correspondance de Galois entre \(\mathcal{P}(\textit{Val})\) et votre treillis.
Une version de concat sur votre treillis. Justifier dans les grandes lignes pourquoi celle-ci est sûre.
Une version de substr sur votre treillis. Justifier dans les grandes lignes pourquoi celle-ci est sûre.

Treillis de multiples d’intervalles

On souhaite définir un treillis qui représente des nombres par des multiples d’intervalles. Par exemple, l’ensemble \({0,2,4}\) sera représenté par \(2\cdot [0,2]\).

Définir ce treillis :

Définir la relation d’ordre partiel.
Définir la plus petite borne supérieure de deux intervalles. Par exemple, \(2\cdot[1,3] \sqcup 2\cdot [2,4] = 2\cdot [1,4]\); et \(2\cdot[1,3] \sqcup 3\cdot [1,2] = 1\cdot[2,6]\) (remarquez que \(1 = \textit{gcd}(2,3)\)).
Dessiner une fraction du diagramme de Hasse.
Définir une fonction d’abstraction. Par exemple, \(\alpha({3,6,9}) = 3 * [1,2]\); on peut observer que 3 est le plus grand commun diviseur de 3, 6, et 9, que \(1 = \textit{min}({3,6,9})/3\), et que \(2 = \textit{max}({3,6,9})/3\).
Dessiner une fraction du diagramme de Hasse.
Bonus: définir une correspondance de Galois entre ces multiples d’intervalles et les intervalles classiques vus au cours.

Analyse de flot de donnée pour variables non-définies

On considère une analyse de variable non-définie. Le treillis de base \(L_0\) est le treillis contenant deux valeurs, \(\texttt{undef}\) et \(\texttt{def}\), telles que \(\texttt{def} \sqsubseteq \texttt{undef}\). Les règles d’analyses sont les suivantes :

pour une déclaration de variable locale int x, on a \(\llbracket n \rrbracket(s) = join(n)(s)[\texttt{x}\mapsto\texttt{undef}]\)
pour une affectation x = e, on a \(\llbracket n \rrbracket(s) = join(n)(s)[\texttt{x}\mapsto\texttt{def}]\)
pour tout autre nœud, on a \(\llbracket n \rrbracket(s) = join(n)(s)\)

Où \(join(n, s) = \bigsqcup_{p\in\textit{pred}(n)} \llbracket p\rrbracket(s)\)

Représenter le treillis sous forme de diagramme de Hasse
Que vaut \(\texttt{def} \sqcup \texttt{undef}\) ?
Est-ce une analyse forward ou une analyse backward ? Pourquoi ?
Est-ce une analyse may ou une analyse must ? Pourquoi ?

Soit le programme suivant :

1    int x;
2    if (cond) {
3      x = 1;
4    }
5    return x;

Si la valeur dans le treillis avant la ligne 1 est \(\bot\), quelle est la valeur après la ligne 1 ?
Si la valeur dans le treillis avant la ligne 3 est \(\bot\), quelle est la valeur après la ligne 3 ?
Quelle est la valeur avant la ligne 5, en utilisant les résultats des deux questions précédentes comme valeurs de treillis pour les lignes 1 et 3 ?

Analyse symbolique

Soit le programme suivant :

int main() {
    int a = getchar();
    int b = getchar();
    int c = getchar();

    if (a > 42) {
        b = b + 2;
        if ((a + b) % 3 == 0) {
            c = c - 1;
        } else {
            c = c + 4;
        }
    } else {
        b = b - 1;
        if (b % 2 == 0) {
            c = c + 3;
        } else {
            c = c - 2;
        }
    }

    if (c % 5 == 0) {
        printint(1);
    } else if (a - b < 0) {
        printint(2);
    } else {
        printint(3);
    }

    return 0;
}

On fera ici l’hypothèse que trois caractères sont toujours donnés, donc que getchar() retourne toujours un nombre ≥0.

Faire une exécution symbolique dynamique à la main sur ce programme.
Combien de chemins contient ce programmes ? Combien parmi ceux-ci sont inatteignables ?

Analyse de code mort

On considère 3 outils qui détectent le défaut de code CWE-561 (Dead Code) :

Outil 1 est un linter qui détecte les conditions constantes.
Outil 2 procède par une analyse symbolique dynamique.
Outil 3 procède par une analyse dataflow.

Soit les fonctions suivantes :

int f1() {
  int x = 0;
  if (x == 42) {
    return 1;
  }
  return 0;
}

int f2() {
  int x = getchar();
  if (x > 255) {
    return 1;
  }
  return 0;
}

int f3() {
  int x = getchar();
  if (x < 10) {
    return 1;
  }
  return 0;
}

Pour rappel, getchar() est garanti de retourner un nombre entre -1 et 255.

On obtient les résultats suivant pour chaque outil:

Outil 1 détecte le défaut sur f1, mais pas sur f2 ni f3
Outil 2 détecte le défaut sur f1, f2, et f3
Outil 3 détecte le défaut sur f1, f2, mais pas f3

Commenter ces résultats. Lesquels sont des vrais positifs, faux positifs, vrais négatifs, faux négatifs ?
Quel outil est incorrect ? Quel outil est incomplet ?
Faire une hypothèse sur comment chacun de ces outils détecte le défaut.