Analyse Statique de programmes - TP Frama-C

ENSIIE 3ème année - année 2011/2012

Enseignants : Virgile Prevosto et Julien Signoles

10 janvier 2012

Introduction

Le but de ce TP est d’utiliser l’outil Frama-C et en particulier son greffon d’analyse de valeur. La version installée à l’ENSIIE est Beryllium-20090902.

Prise en main

Frama-C est fondé sur un ensemble de greffons proposant chacun un type d’analyse particulier. La liste des greffons disponibles peut être obtenue par frama-c -help. De même, les options permettant de piloter le noyau s’obtiennent avec frama-c -kernel-help. Nous nous intéresserons en particulier aux options -main, -lib-entry et -pp-annot.

De plus, nous utiliserons avant tout le greffon value, fondé sur l’interprétation abstraite (cf. cours précédent). Ses options sont accessibles par frama-c -value-help. Les options les plus importantes pour ce TP sont -val, -slevel et -wlevel.

Enfin, il existe une interface graphique, frama-c-gui, qui accepte les mêmes options que frama-c.

Calcul de puissance

On considère la fonction pow ci-dessous (fichier pow.c), qui calcule n élevé à la puissance m

unsigned int pow(unsigned int n, unsigned int m) {
  unsigned int res = 1;
  unsigned int aux = n;
  while(m>1) {
    if (m%2 == 1) { res = res * aux; }
    m /= 2;
    aux = aux * n * n;
  }
  if (m%2 == 1) { res *= aux; }
  return res;
}

Une première analyse

On utilise l’option -main pow pour indiquer à Frama-C que le point d’entrée est pow et -val pour lancer l’analyse de valeur. Quelles sont les valeurs obtenues pour m, aux, et res?
L’analyse de valeur ne peut pas donner de résultats très intéressants dans un contexte aussi générique. On va donc construire un contexte d’appel un peu plus spécialisé. Pour cela, on dispose de la fonction interval ci-dessous (fichier interval.c)

volatile int entropy;

int interval(int a, int b) {
  int tmp = entropy;
  if (tmp <= a) { tmp = a; }
  if (tmp >= b) { tmp = b; }
  return tmp;
}

Par construction, la valeur retournée par interval est dans l’intervalle [a;b]. On utilise cette fonction pour appeler pow avec un exposant compris entre 1 et 16:

void main(void) {
  unsigned int m = interval(1,16);
  unsigned int res = pow(2,m);
}

Que donne l’analyse de la fonction main?

Afin d’améliorer la précision des résultats, on peut utiliser l’option -slevel n: elle demande à l’analyse de valeur de propager séparément jusqu’à n états. Utiliser cette option pour minimiser l’intervalle obtenu pour res. Est-ce conforme aux résultats attendus?
En complément de -slevel, on peut ajouter des assertions ACSL sous forme de disjonction (couvrant tous les cas possibles au point de programme correspondant): avec un -slevel approprié, Frama-C considérera séparément chaque branche de la disjonction. Utiliser ce comportement pour analyser séparément chacune des valeurs possibles de m. Est-ce conforme aux résultats attendus?
Pour examiner le déroulement de l’analyse, et non simplement le résultat final, on peut utiliser la famille de fonctions built-ins Frama_C_show_each_XXXX(), qui affichera les valeurs des arguments qu’on lui donne à chaque passage. Modifier main (en gardant l’assertion précédente) pour afficher le résultat obtenu pour chaque m. Est-ce bien la valeur attendue? Modifier éventuellement pow en conséquence.
On s’intéresse maintenant aux valeur de pow pour tout n et m compris entre 1 et 10. Écrire une fonction naive_pow qui calcule la puissance en multipliant m fois n par lui-même, et modifier main pour montrer à l’aide de l’analyse de valeur que naive_pow et pow donnent bien le même résultat pour les valeurs de n et m dans l’intervalle demandé.

SHA-1

On considère à présent l’implémentation en C de la fonction de hachage cryptographique sha1 librement disponible sur cette page. L’archive contient, outre l’implémentation proprement dite, un fichier de test shatest.c. Ce fichier utilise des fonctions de la bibliothèque standard du C (printf et strlen) qui ne sont pas implicitement connues par Frama-C. Nous allons donc remplacer ce fichier par celui-ci qui inclut une implémentation de strlen et remplace les utilisations de printf par des Frama_C_show_each_XXXX.

Lancer l’analyse de valeurs de Frama-C sur sha1.c et shatest.c. Qu’observe-t-on comme résultats ?
L’option -deps de Frama-C se fonde sur l’analyse de valeurs pour calculer les dépendances entre les sorties et les entrées de chaque fonction. Utiliser cette option et expliquer les résultats obtenus pour la fonction SHA1Result.
Utiliser à présent l’option -slevel n pour améliorer au maximum les résultats de l’analyse et supprimer toutes les alarmes.
Avec ces derniers résultats précis, expliquer les valeurs obtenues en sortie de la fonction main.
Une partie de shatest.c n’est pas exécutée (encadrée par #if 0 ... #endif) : supprimer le test du préprocesseur, relancer l’analyse et répondre de nouveau à la question précédente.
À l’aide de la fonction interval de l’exercice précédent, écrivez une fonction main permettant de vérifier qu’aucune exécution de sha1 sur des messages contenant au plus 64 caractères ne produit d’erreur à l’exécution.
Utiliser l’analyse de valeurs pour effectuer cette vérification.
Expliquer à nouveau les valeurs obtenues en sortie de la fonction main.