INF889A - Révisions

Garanties

Soit le défaut de code CWE-23, défini comme suit :

The product uses external input to construct a pathname that should be within a restricted directory, but it does not properly neutralize sequences such as “..” that can resolve to a location that is outside of that directory.

Considérons un outil de détection de ce 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 données par l’outil s’il fonctionnait :

  • en se basant sur le fuzzing ?
  • en se basant sur l’instrumentation ?
  • 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;
}

1. Représenter son CFG
2. Représenter son arbre d’exécutions
3. Faire une exécution dynamique symbolique en traitant x et y comme entrée symbolique

Treillis

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

1. 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

2. Si on souhaite raisonner à la fois sur la parité et sur le signe d’un nombre, que peut-on faire ? Détailler.

3. Définir l’opérateur \(\hat{+}\) qui est une sur-approximation de l’addition de deux nombres.

4. Énoncer la propriété de monotonicité pour \(\hat{+}\)

5. Démontrer que votre définition de \(\hat{+}\) est monotone.

6. Énoncer la propriété qui permet de s’assurer que \(\hat{+}\) est une sur-approximation sûre.

7. Prouver que votre définition de \(\hat{+}\) est une sur-approximation sûre.

8. Définir sur le treillis parité, 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.

Analyse de flot de donnée

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 = \lambda s. Join(n)(s)[\texttt{x}\mapsto\texttt{undef}]\)
• pour une affectation x = e, on a \(\llbracket n \rrbracket = \lambda s.Join(n)(s)[\texttt{x}\mapsto\texttt{def}]\)
• pour tout autre nœud, on a \(\llbracket n \rrbracket = \lambda s.Join(n)(s)\)

Où \(Join(n, s) = \lambda n. \lambda 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 ?