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:ensiie2017-2018-ias-tp [Frama-C]

User Tools

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

Site Tools


mantis:frama-c:ensiie2017-2018-ias-tp

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

mantis:frama-c:ensiie2017-2018-ias-tp [2018/01/08 17:27] (current)
virgile Exercise sheet for ENSIIE course
Line 1: Line 1:
 +====== 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 {{:​mantis:​frama-c:​ensiie-2017-2018:​array.c|array.c}}
 +
 +<code 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));
 +}
 +</​code>​
 +Cette fonction est un exemple tiré des [[https://​wiki.sei.cmu.edu/​confluence/​display/​c/​ARR30-C.+Do+not+form+or+use+out-of-bounds+pointers+or+array+subscripts|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:
 +
 +<code c>
 +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));
 +}
 +</​code>​
 +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%%'':​
 +
 +<code c>
 +  insert_in_table(101,​ Frama_C_interval(INT_MIN,​ INT_MAX));
 +</​code>​
 +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 [[http://​sourceforge.net/​projects/​safeclib/​|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 {{:​mantis:​frama-c:​ensiie-2017-2018:​strispassword_s.c|strispassword_s.c}}. La bibliothèque fournit un jeu de test dans {{:​mantis:​frama-c:​ensiie-2017-2018:​test_strispassword_s.c|test_strispassword_s.c}}. Ces fichiers ainsi que les en-têtes nécessaires sont fournis dans l’{{mantis:​frama-c:​ensiie-2017-2018:​strispassword.zip|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 [[https://​tls.mbed.org|mbedtls]]. Les fichiers nécessaires sont dans l’archive {{mantis:​frama-c:​ensiie-2017-2018:​mbedtls.zip|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 [[http://​cs.smith.edu/​~orourke/​books/​ftp.html|//​Computational Geometry in C//]] de J. O’Rourke. On le trouvera {{mantis:​frama-c:​ensiie-2017-2018:​extreme.c|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 [[https://​github.com/​attractivechaos/​klib|klibc]]. Le code a déjà été préparé pour une analyse par Frama-C dans le repository [[https://​github.com/​Frama-C/​open-source-case-studies/​|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 {{mantis:​frama-c:​ensiie-2017-2018:​khash.zip|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.
 +
  
mantis/frama-c/ensiie2017-2018-ias-tp.txt · Last modified: 2018/01/08 17:27 by virgile