SYSTEM WARNING: 'session_name(): Cannot change session name when session is active' in '/home/gitlab-www/dokuwiki/inc/init.php' line 231

SYSTEM WARNING: 'session_set_cookie_params(): Cannot change session cookie parameters when session is active' in '/home/gitlab-www/dokuwiki/inc/init.php' line 232

mantis:frama-c:ensiie2014-2015-ias-tp [Frama-C]

User Tools

  • Logged in as: anonymous (anonymous)
  • Log Out

Site Tools


mantis:frama-c:ensiie2014-2015-ias-tp

Analyse Statique de Programmes -- TP Frama-C

ENSIIE 3ème année – année scolaire 2014/2015 Enseignants: Virgile Prevosto et Julien Signoles

19 décembre 2014

Exercice 0: Préliminaires

Le code se trouve dans le fichier fact.c.

On considère la fonction fact suivante, correspondant à l'exemple vu en cours:

    #include "__fc_builtin.h"

    int fact() {
      int x = Frama_C_interval(0,10);
      int y = 1;
      while(x>0) {
        y = y * x;
        x = x - 1;
      }
      return y;
    }
  1. lancer Frama-C avec la commande suivante: frama-c -val -main fact -cpp-extra-args=“-I$(frama-c -print-share-path)/libc” fact.c, et observer les résultats obtenus. Les différentes options utilisées sont:
  • -val pour lancer l'analyse de valeur
  • -main fact pour indiquer que le point d'entrée du programme est la fonction fact (le défaut étant main)
  • -cpp-extra-args=“-I$(frama-c -print-share-path)/libc” pour indiquer que le pré-processeur doit chercher les en-têtes (ici _fc_builtin.h) dans la bibliothèque standard de Frama-C. On utilise ici le built-in Frama_C_interval qui renvoie un entier quelconque compris entre les deux arguments de la fonction.
  1. Lancer l'interface graphique frama-c-gui avec les mêmes options, et cliquer sur différentes variables du programme pour observer les valeurs calculées par Value en ce point dans l'onglet information. Dans la suite, on pourra utiliser indifféremment l'interface console ou l'interface graphique (dans cette dernière, l'onglet console montre les mêmes affichages que le mode texte).
  2. Afin de tracer ce qu'il se passe pendant l'analyse, on peut demander à Value d'afficher des résultats intermédiaires avec un appel à des fonctions de la forme Frama_C_show_each_*(…), * pouvant être n'importe quel suffixe. Insérer par exemple l'appel Frama_C_show_each_fact(x,y); dans le corps de la boucle et relancer l'analyse. Qu'observe-t-on?
  3. Différentes options sont disponibles afin d'améliorer la précision des résultats de Value (frama-c -value-help donne la liste complète des options de Value). Nous allons nous intéresser à deux d'entre elles:
  • -wlevel n indique à Value de ne procéder à une opération d'élargissement qu'au bout de n tours de boucle. Par défaut, n vaut 3. Effectuer l'analyse avec différentes valeurs de n, et observer l'impact sur les résultats intermédiaires indiqués par Frama_C_show_each_fact et sur le résultat final.
  • -slevel n indique à Value de propager jusqu'à n états distincts avant de procéder à des unions (joins). n vaut par défaut 1 (on fusionne toujours les états). Même question que précédemment.
  1. Quand le slevel est suffisant, on peut utiliser des annotations ACSL sous forme de disjonction pour forcer Value à considérer un état séparé par élément de la disjonction. Ajouter par exemple l'assertion /*@ assert x ⇐ 5 || x > 5; */ après la définition de x dans la fonction fact, et relancer l'analyse avec un slevel suffisant. Qu'observe-t-on pour les résultats intermédiaires?
  2. En augmentant la borne supérieure utilisée pour Frama_C_interval, déterminer la plus grande valeur possible pour x avant que le calcul de fact ne provoque un débordement arithmétique.

Dans tout ce qui suit, on veillera à utiliser -slevel et des assert pour améliorer la précision des résultats.

Exercice 1: Suite de Fibonacci

Le code se trouve dans le fichier fibonacci.c. On considère la fonction fibo suivante:

int u[100] = { 1, 1 };

int fibo(int n) {
  int m = n;
  while (u[m]==0) { Frama_C_show_each_last_comp(m); m--; }
  if (n == m) return u[m];
  while(m<n) {
    Frama_C_show_each_fib(m,u[m]);
    u[m+1] = u[m] + u[m-1];
    m++;
  }
  return u[m];
}

qui renvoie le n-ième élément de la suite de Fibonacci, et stocke ses calculs intermédiaires dans un tableau global. 1. Lancer l'analyse sur la fonction fibo. Que remarque-t-on? 2. On souhaite restreindre les valeurs de n sur lesquelles on fait l'analyse. Pour cela, une possibilité consiste à écrire une fonction wrapper qui appelera fibo dans un environnement approprié. Par exemple, on peut commencer par étudier le cas n==4 avec la fonction main1 suivante:

int main1 () {
  return fibo(4);
}

Qu'obtient-on comme résultat? 3. Modifier main1 pour étudier le cas n==42. 4. Modifier main1 pour étudier un appel pour n quelconque entre 0 et 99. À partir de quelle valeur de n observe-t-on un débordement arithmétique?

Exercice 2: Buffer Circulaire

On considère le code du fichier ring_buffer.c, extrait de l'article Wikipedia sur les buffers circulaires. Ce code fait des allocations mémoires, pour lesquelles Value propose plusieurs comportements, choisis par une macro lors du preprocessing. On ajoutera sur la ligne de commande les arguments suivants:

  • -cpp-extra-args=“-DFRAMA_C_MALLOC_HEAP” pour sélectionner la version de malloc correspondante
  • $(frama-c -print-share-path)/libc/stdlib.c pour charger l'implantation de malloc en question.
  1. Effectuer l'analyse avec la fonction main du fichier, et vérifier qu'aucune erreur à l'exécution ne peut se produire pour ce test.
  2. Modifier la fonction main en utilisant les fonctions de _fc_builtin.h pour analyser un nombre arbitraire d'opérations cbWrite (avec un élément quelconque entre 0 et 1000) et cbRead, effectuées dans n'importe quel ordre (modulo le fait qu'on ne peut effectuer cbRead que sur un buffer non vide), et effectuer l'analyse à partir de cette nouvelle fonction.

Exercice 3: Compression

On s'intéresse à une implantation d'un algorithme de compression tiré de la Basic Compression Library de Marcus Geelnard (fichier rice.c, le code original se trouvant ici). L'en-tête rice.h correspondant est le suivant:

/*************************************************************************
* Supported binary formats
*************************************************************************/

/* These formats have the same endianity as the machine on which the
   (de)coder is running on */
#define RICE_FMT_INT8   1  /* signed 8-bit integer    */
#define RICE_FMT_UINT8  2  /* unsigned 8-bit integer  */
#define RICE_FMT_INT16  3  /* signed 16-bit integer   */
#define RICE_FMT_UINT16 4  /* unsigned 16-bit integer */
#define RICE_FMT_INT32  7  /* signed 32-bit integer   */
#define RICE_FMT_UINT32 8  /* unsigned 32-bit integer */


/*************************************************************************
* Function prototypes
*************************************************************************/

int Rice_Compress( void *in, void *out, unsigned int insize, int format );
void Rice_Uncompress( void *in, void *out, unsigned int insize,
                      unsigned int outsize, int format );

Écrire une fonction main permettant de vérifier avec Frama-C si la fonction de compression Rice_Compress peut présenter des erreurs à l'exécution si on l'appelle avec un buffer d'entrée de 512 unsigned char.

Exercice 4: Encryption

On s'intéresse à une implantation de l'algorithme AES développée pour les logiciels embarqués: tiny-AES, dont le fichier principal est aes.c, avec l'en-tête aes.h suivant:

void AES128_ECB_encrypt(uint8_t* input, const uint8_t* key, uint8_t *output);
void AES128_ECB_decrypt(uint8_t* input, const uint8_t* key, uint8_t *output);

void AES128_CBC_encrypt_buffer(uint8_t* output, uint8_t* input, uint32_t length, const uint8_t* key, const uint8_t* iv);
void AES128_CBC_decrypt_buffer(uint8_t* output, uint8_t* input, uint32_t length, const uint8_t* key, const uint8_t* iv);

Écrire une fonction main permettant de vérifier avec Frama-C si la fonction d'encryption AES128_CBC_encrypt_buffer peut présenter des erreurs à l'exécution lorsqu'on crypte un buffer d'entrée de 512 caractères.

mantis/frama-c/ensiie2014-2015-ias-tp.txt · Last modified: 2014/12/19 09:00 by signoles