Analyse Statique de programmes - TP Frama-C

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

Enseignants : Virgile Prevosto et Julien Signoles

22 janvier 2013

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 Oxygen-20120901.

Prise en main

Frama-C est fondé sur un ensemble de greffons proposant chacun un type particulier d’analyse. 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 et -ocode.

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.

PGCD

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

int pgcd(int x, int y) {
     int a = x, b = y;
     while(b!=0) {
          int tmp = mod(a,b);
          a = b; b = tmp;
     }
     return a;
}

Afin de contourner une imprécision de Frama-C, on n’utilise pas l’opérateur % habituel, mais une opération mod spécifiée de la manière suivante:

/*@ requires y != 0;
    assigns \result \from x,y;
    ensures -(y) < \result < y || y<\result< -y;
    ensures \result == x%y;
*/
int mod(int x, int y);

Une première analyse

On définit une petite fonction de test:

int P;

void test() {
     P=pgcd(49,28);
}
  1. On utilise l’option -main test pour indiquer à Frama-C que le point d’entrée est test et -val pour lancer l’analyse de valeur. Quelles est la valeur obtenue pour P?
  2. Pour voir ce qui se passe à l’intérieur de la boucle, on peut utiliser une fonction Frama_C_show_each_XXX(...), où XXX est un suffixe quelconque. Cette fonction provoquera l’affichage des intervalles trouvés pour chacun de ses arguments chaque fois que l’analyse passe par le statement correspondant. Ainsi, Frama_C_show_each_a(a) en début de boucle permettra de voir comment évoluent les valeurs possibles pour a. Que constate-t-on?
  3. Le problème observé vient du fait que les valeurs pour a superposent tous les pas de boucle, et qu’on effectue du widening. Une première approche permet de retarder le moment où on a recours à l’élargissement, en augmentant la valeur de l’option -wlevel (3 par défaut). Tester différentes valeurs. Qu’obtient comme résultats pour P?
  4. Une meilleure option consiste à augmenter la valeur de l’option -slevel (1 par défaut), qui permet de propager jusqu’à n états séparés pour chaque statement. Tester différentes valeurs. Qu’obtient-on comme résultats pour P?

Analyse générique

  1. On choisit maintenant comme point d’entrée pgcd elle-même. Quels sont les problèmes recensés par Frama-C?
  2. Pour montrer que la pré-condition de mod est toujours vérifiée, on va avoir recours à une annotation ACSL: quand l’analyse de valeur rencontre une disjonction, et si la valeur du slevel le permet, elle utilise un état pour chaque branche de la disjonction. Écrire une annotation permettant de ne pas émettre d’alarme. La disjonction doit respecter deux critères:
    1. elle doit couvrir tous les cas possible: l’analyse de valeur doit pouvoir la valider
    2. chaque cas doit permettre à l’analyse de valeur de réduire l’état correspondant: il faut utiliser des conjonctions d’inégalités impliquant une variable.

PPCM

On considère maintenant la fonction ppcm ci-dessous (et donnée également dans ppcm.c), avec une fonction test2 permettant de faire un test particulier.

int ppcm(int x, int y) {
     int a = x, b = y;
     while(b!=0) {
          int tmp = mod(a,b);
          a = b; b = tmp;
     }
     return x * y / a;
}

void test2() {
     P=ppcm(49,28);
}
  1. étudier la valeur trouvée pour P après l’exécution de test2
  2. Dans un contexte générique, la multiplication à la fin de ppcm peut mener à un overflow. On va limiter le cas d’étude à des valeurs comprises entre -10000 et 10000 pour x et y. En se servant de la fonction interval donnée ci-dessous, fournir une fonction main qui appelle ppcm dans ce contexte.
  3. Peut-on avoir une division par 0 lors de l’exécution de ppcm avec des paramètres quelconques? Corriger éventuellement la fonction.
/*@ requires a<=b;
  ensures a<=\result<=b;
*/
int interval(int a, int b);

SHA-3

On considère à présent l’implémentation en C de la fonction de hachage cryptographique Keccak librement disponible sur cette page. Cette fonction a été sélectionnée fin 2012 à l’issue de la compétition SHA-3 pour remplacer SHA-2. On cherche dans cet exercice à montrer que l’implantation de référence est exempt d’erreur à l’exécution pour des messages inférieurs à une certaine taille.

Récupération des fichiers

L’archive Keccak contient en fait plusieurs implantations: une en C pur, et d’autres optimisées et comportant certaines portions en assembleur. Seule la première nous intéresse. On va commencer par utiliser Frama-C pour générer un fichier qui regroupe les fonctions de cette implantation, et uniquement celles-ci. À l’aide du fichier makefile, et plus particulièrement de sa variable SOURCE_REFERENCE, trouver la liste des fichiers .c à considérer (NB: on ne s’intéresse pas aux fichiers main*, puisque nous utiliserons nos propres fonctions main). Générer un fichier C faisant le link de ceux-ci à l’aide de la commande frama-c -print -ocode resultat.i entree1.c entree2.c ... On travaillera désormais avec le fichier resultat.i, qui alternativement est disponible ici

Analyse

Il manque à ce résultat quelques fonctions de la stdlib dont Frama-C aura besoin, et qui sont données ici. On s’intéresse à la fonction main suivante (fichier):

#include <stdio.h>
#include "KeccakNISTInterface.h"

#define HASHLEN 64

BitSequence msg[80] = "hello, world";

int main(void) {
  BitSequence hash[HASHLEN/8];
  unsigned long i;
  hashState context;
  Init(&context, HASHLEN);
  Update(&context,msg,80);
  Final(&context,hash);
  for (i=0; i<HASHLEN/(8*sizeof(unsigned long)); i++)
       printf("%lu\n",((unsigned long *)hash)[i]);
  return 0;
}
  - compiler cette application (''resultat.i'' et ''main'') avec ''gcc'', et exécuter le résultat obtenu. Qu'observe-t-on?
  - Lancer l'analyse de valeurs de Frama-C sur ''resultat.i'' et ''main''. Qu'observe-t-on comme résultats ?
  - Le cas échéant, corriger le code en vous basant sur la documentation de ''KeccakNISTInterface.h'', et relancer compilation et analyse. Qu'observe-t-on
  - À l'aide de la fonction ''interval'', modifier ''main'' pour que ''msg'' contienne une suite aléatoire de caractères, et relancer l'analyse. Y'a-t-il des erreurs à l'exécution possibles?