Analyse Statique de Programmes – TP Frama-C

ENSIIE 3ème année – année scolaire 2016/2017 Enseignants: Tristan Le Gall et Virgile Prevosto

3 janvier 2017

Exercice 1:

On considère le programme suivant, également disponible dans le fichier string.c

int f(char* dest, int len, const char* src) {
  int i = 0;
  while (src[i] != 0 && src[i] != ' ' && i < len) {
    dest[i] = src[i];
    i++;
  }
  dest[i] = 0;
  return i-1;
}

int main() {
  const char* test[] = "Example of character string";
  char result1[10], result2[10];
  int res = f(result1, 9, test);
  f(result2, 9, test + res + 1);
  return 0;
}

Lancer l’analyse de valeur sur ce programme, à l’aide de la commande frama-c -val string.c. Qu’observe-t-on pour les valeurs possibles des éléments des tableaux result1 et result2?
Même question en utilisant l’interface graphique (frama-c-gui -val string.c)
Insérer des appels à la famille de fonctions built-in Frama_C_show_each_* pour étudier l’évolution des valeurs de i, dest, src et dest[i] lors du calcul du point fixe pour la boucle de la fonction f. On rappelle qu’une fonction dont le nom commence par Frama_C_show_each_ peut prendre un nombre arbitraire d’arguments, dont l’évaluation dans l’état courant de l’analyse de valeur sera affiché sur la sortie standard chaque fois que l’analyse atteint ce point.
Une première possibilité d’amélioration des résultats consiste à utiliser l’option -wlevel, qui modifie le moment où le widening se déclenche. Observer ce qui se passe si on utilise -wlevel 10
Une seconde possibilité consiste à dérouler syntaxiquement certaines boucles. Pour cela, on utilise l’annotation /*@ loop pragma UNROLL n; */ où n est un entier au-dessus de la boucle qu’on veut dérouler. Dérouler 10 fois la boucle de la fonction f interne. Qu’observe-t-on?
La méthode privilégiée d’amélioration des résultats de l’analyse de valeur est l’option -slevel qui autorise l’analyse à propager un certain nombre d’états distincts par instruction avant de faire l’union. Qu’obtient-on comme résultat avec -slevel 20?
Que calcule ce programme?

Exercice 2: Contexte d’exécution

On reprend le programme de l’exercice précédent. On va désormais s’intéresser à ce qui se passe si la chaîne test initiale contient 99 caractères arbitraires (et le 0 terminal).

En utilisant la fonction Frama_C_interval déclarée dans l’en-tête __fc_builtin.h fourni avec Frama-C, définir une fonction void init(char* s, int length) qui remplit le bloc pointé par s avec des caractères non nuls arbitraires et un 0 terminal.
Modifier la fonction main pour que test ait un contenu arbitraire tel qu’indiqué en début d’énoncé.
Lancer Value Analysis (en jouant éventuellement avec les paramètres de précision) sur cette nouvelle fonction main. Que constate-t-on?
Après avoir corrigé le cas échéant la fonction f, relancer Value Analysis. D’où provient l’alarme résiduelle? Modifier init pour que le contenu initial de test ne risque pas de provoquer d’erreur à l’exécution, et relancer Value Analysis pour le confirmer.

Exercice 3: Fonction de Bessel

On s’intéresse au fichier bessel.c de la dietlibc, une implantation minimaliste de bibliothèque système (https://www.fefe.de/dietlibc/). Plus précisément, on cherche à déterminer la sensibilité de la fonction j0 à une incertitude sur son argument.

Écrire une fonction main qui calcule j0(3) et la différence entre ce résultat et j0(x) où x est dans l’intervalle [3-0.125,3+0.125]
Utiliser Value Analysis pour vérifier que la variation du résultat de j0 autour de 3 reste faible.

Exercice 4: Fonction crypt

On s’intéresse désormais à la fonction crypt de la dietlibc, dont l’implantation est fournie dans le fichier crypt.c

À l’aide de man, retrouver le comportement attendu de la fonction
En déduire une fonction init qui préparera un contexte d’analyse de crypt pour un mot de passe de 29 caractères ASCII arbitraires.
À l’aide de l’analyse de valeur, vérifier que le chiffrement d’un tel mot de passe ne peut pas conduire à une erreur à l’exécution.
Observer le contenu du buffer contenant le mot de passe chiffré à la fin de l’exécution de crypt. Que peut-on en dire?

Exercice 5: Chaînes dynamiques

On s’intéresse à la bibliothèque sds (http://github.com/antirez/sds), qui se présente sous la forme d’un fichier en-tête sds.h et d’un fichier d’implantation sds.c. On va chercher à vérifier que la concaténation de deux sds obtenues à partir de chaînes C standard de 50 caractères (quelconques) ne peut provoquer d’erreur à l’exécution.

Écrire la fonction d’initialisation du contexte et la fonction main correspondante.
Lancer Value Analysis. Que constate-t-on?
Fournir une implantation naïve de malloc qui utilise deux tableaux char __alloc[SIZE_MAX] où seront faites les allocations et size_t __alloc_size[SIZE_MAX] qui stocke à chaque indice où une allocation a lieu la taille du bloc alloué. Relancer l’analyse de valeur avec cette implantation. Obtient-on de meilleurs résultats?
Fournir les implantations des fonctions de la bibliothèque standard manquantes et vérifier qu’il n’y a effectivement pas d’erreur à l’exécution possible.

Exercice 6: Compression de petites chaînes

On s’intéresse maintenant à la bibliothèque smaz, qui propose une fonction de compression optimisée pour les courtes chaînes ASCII. On partira de la fonction de test main du fichier smaz_test.c. Le code est disponible dans cette archive.

smaz utilise des fonctions de la bibliothèque standard C pour lesquelles il faut fournir une implantation que Value Analysis puisse analyser. Écrire une telle implantation pour strlen.
Supprimer de main la partie qui teste la compression d’une chaîne aléatoire (on s’y intéressera dans un second temps), et utiliser Value Analysis pour vérifier qu’aucune erreur à l’exécution n’est possible pendant la compression et la décompression des chaînes données en exemple. Le cas échéant, fournir des implantations pour les fonctions de la bibliothèque standard utiles.
Modifier main pour vérifier que la compression et la décompression d’une chaîne aléatoire de longueur au plus 50 ne risque pas de provoquer d’erreur à l’exécution