---
title: ENSIIE - Analyse Statique de Programmes 2012/2013
layout: clean_page
---
# 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](http://frama-c.com) et
en particulier son greffon d'[analyse de
valeur](http://frama-c.com/download/value-analysis-Oxygen-20120901.pdf).
La version installée à l'ENSIIE est
[Oxygen-20120901](http://frama-c.com/download.html).
### 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](/assets/dokuwiki/ppcm.c)), qui calcule `n` élevé à la puissance
`m`
``` c
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:
``` c
/*@ 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:
``` c
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](/assets/dokuwiki/ppcm.c)), avec une fonction
`test2` permettant de faire un test particulier.
``` c
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.
<!-- end list -->
``` c
/*@ 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](http://keccak.noekeon.org/KeccakReferenceAndOptimized-3.2.zip) de la
fonction de hachage cryptographique **Keccak** librement disponible sur
[cette page](http://keccak.noekeon.org/files.html). Cette fonction a été
sélectionnée fin 2012 à l'issue de la compétition **SHA-3** pour
remplacer [SHA-2](https://fr.wikipedia.org/wiki/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](/assets/dokuwiki/keccak_reference.c)
#### Analyse
Il manque à ce résultat quelques fonctions de la stdlib dont Frama-C
aura besoin, et qui sont données [ici](/assets/dokuwiki/keccak_lib.c).
On s'intéresse à la fonction `main` suivante
([fichier](/assets/dokuwiki/keccak_main.c)):
``` c
#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?
```