Analyse Statique de Programmes – TP Frama-C

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

9 janvier 2018

Exercice 1: Préliminaires

On considère la fonction suivante, également disponible dans le fichier array.c

#include <stdlib.h>
#include <stdint.h>
#include <limits.h>
#include "__fc_builtin.h"

static int *table = NULL;
static size_t size = 0;

int insert_in_table(size_t pos, int value) {
  if (size < pos) {
    int *tmp;
    size = pos + 1;
    tmp = (int *)realloc(table, sizeof(*table) * size);
    if (tmp == NULL) {
      return -1;   /* Failure */
    }
    table = tmp;
  }
  table[pos] = value;
  return 0;
}

int main () {
  insert_in_table(100, Frama_C_interval(INT_MIN, INT_MAX));
  insert_in_table(SIZE_MAX, Frama_C_interval(INT_MIN, INT_MAX));
}

Cette fonction est un exemple tiré des règles de codage du CERT, qui montre un certain nombres de faiblesse pouvant entraîner des failles de sécurité.

Question 1

Lancez Frama-C avec la commande suivante: frama-c-gui -val array.c. Que constatez vous?

Question 2

Proposez une correction du code pour éviter l’alarme d’EVA, et vérifiez que votre solution ne provoque plus d’alarme.

Question 3

On modifie maintenant la fonction main comme suit:

int main () {
  insert_in_table(SIZE_MAX, Frama_C_interval(INT_MIN, INT_MAX));
  insert_in_table(100, Frama_C_interval(INT_MIN, INT_MAX));
  insert_in_table(101, Frama_C_interval(INT_MIN, INT_MAX));
}

Lancez Frama-C sur ce nouveau programme, et corrigez le cas échéant insert_in_table.

Question 4

On ajoute un quatrième appel à insert_in_table dans main:

  insert_in_table(101, Frama_C_interval(INT_MIN, INT_MAX));

Relancez l’analyse avec cette modification de main et vérifiez qu’il n’y a pas d’alarme. Observez dans l’interface graphique la fonction insert_in_table. Pourquoi y a-t-il du code mort (surligné en rouge), c’est à dire par lequel EVA n’est pas passé?

Question 5

Afin de prendre en compte la possibilité que l’appel à realloc renvoit NULL, remplacez-le par un appel à une fonction my_realloc, qui utilisera la fonction Frama_C_nondet, built-in de Frama-C qui renvoit aléatoirement la valeur de son premier ou de son deuxième argument, pour permettre de renvoyer soit NULL, soit une reallocation réussie. Relancez l’analyse dans ce nouveau contexte, en utilisant les options suivantes pour s’assurer que EVA garde bien séparés les états correspondant à une reallocation réussie ou non: -slevel 10 -val-split-return-function my_realloc:0,insert_in_table:0

Question 6

Corrigez l’implantation de insert_in_table et relancez l’analyse pour vérifiez qu’il n’y a plus d’alarme.

Exercice 2: strispassword_s

On s’intéresse désormais à certaines fonctions de la Safe C Library, qui vise à proposer des versions des fonctions de manipulation de buffer et de chaînes minimisant les possibilités de débordement de buffer. Dans cet exercice, on s’intéressera à la fonction strispassword_s, telle que définie dans le fichier strispassword_s.c. La bibliothèque fournit un jeu de test dans test_strispassword_s.c. Ces fichiers ainsi que les en-têtes nécessaires sont fournis dans l’archive strispassword.zip

Question 1

Lancez Frama-C sur les deux fichiers C. Que constatez-vous? On pourra utiliser l’option -variadic-no-translation pour éviter les warnings liés à printf.

Question 2

Relancez l’analyse en utilisant l’option -slevel n qui permet de conserver séparés jusqu’à n états abstraits par statement du programme. Arrivez-vous à supprimer certaines alarmes? ### Question 3 Une partie des problèmes vient du fait que la fonction strcpy de la bibliothèque standard n’est pas implantée et que sa spécification ACSL n’est pas adaptée à EVA. Proposez une implantation C de cette fonction et relancez l’analyse. Vérifiez qu’il n’y a plus d’alarme avec un slevel adapté.

Exercice 3: algorithme AES

On s’intéresse à l’implantation de l’algorithme de chiffrement AES dans la bibliothèque mbedtls. Les fichiers nécessaires sont dans l’archive mbedtls.zip

Question 1

Après avoir étudié l’interface mbedtls/aes.h, écrivez une fonction main qui chiffrera un buffer quelconque de 256 éléments au moyen d’une clé arbitraire de 128 éléments (et d’un vecteur d’initialisation arbitraire). On pourra comme dans le premier exercice utiliser Frama_C_interval pour remplir les tableaux correspondants.

Question 2

Lancez Frama-C pour vérifier qu’un tel chiffrement ne peut provoquer d’erreur à l’execution.

Exercice 4: points extrêmes d’un polygone

Le code de cet exercice est tiré du livre Computational Geometry in C de J. O’Rourke. On le trouvera ici. Il s’agit d’un algorithme pour calculer le point extrême d’un polygone suivant une direction donnée.

Question 1

Lancez Frama-C sur le fichier. Qu’observez-vous?

Question 2

Modifiez la fonction ReadPoly, toujours en utilisant Frama_C_interval, pour que le programme calcule les points extrêmes d’un polygone de 200 points dont les coordonnées seront comprises entre -1000 et 1000, et vérifiez qu’il n’y a pas d’erreur possible à l’exécution dans ce contexte.

Question 3

Modifiez main pour trouver le point extrême dans une direction quelconque et non plus horizontale et verticale, et vérifiez là encore l’absence d’erreur à l’exécution.

Exercice 5: fonction de hash

On s’intéresse ici à l’algorithme khash de la klibc. Le code a déjà été préparé pour une analyse par Frama-C dans le repository opensource-case-studies. Les deux fichiers nécessaires à l’analyse sont khash.h et khash.c qui contiennent respectivement l’implantation de la bibliothèque et le cas de test suggéré dans l’implantation. Ils sont disponible dans cette archive

Question 1

Lancez l’analyse sur khash.c et corrigez les éventuelles erreurs du programme. Veillez à bien paramétrer les options gouvernant la précision de l’analyse pour (une fois le(s) problème(s) corrigé(s)) parvenir à ne pas avoir d’alarme.

Question 2

Le programme utilise realloc, avec les mêmes problèmes que dans le premier exercice. Réutilisez votre implantation de my_realloc et relancez l’analyse pour vérifier qu’il n’y a toujours pas d’alarme.

Question 3

Modifiez la fonction main pour obtenir une plus grande couverture de code de kh_resize_32, kh_put_32 et kh_get_32, en ajoutant des appels à kh_put, kh_get et kh_value, et en utilisant Frama_C_interval pour apporter du non-déterminisme. Relancez l’analyse et vérifiez si de nouvelles alarmes sont émises.