Preuve, analyse statique et vérification runtime

Master CILS

2018–19

Master CILS: Preuve, analyse statique et vérification runtime, 1

Besoin de sûreté

La fiabilité peut être parfois importante. . .

et parfois très importante !
I Centrales nucléaires, usines chimiques

I Commandes d’avions

I Pacemakers (voire cœur artificiel !)

I Réseaux ferroviaires, etc.

Systèmes auto-* ?

Master CILS: Preuve, analyse statique et vérification runtime, 2

Des conséquences importantes
De petites erreurs peuvent avoir des conséquences désastreuses :
Coût astronomique, vies humaines !

I Vol inaugural d’Ariane 5

I Mars Climate Orbiter
I London Ambulance Service Computer-Aided
Dispatch System
I Bug du Pentium d’Intel
I Debian/OpenSSL RNG

Master CILS: Preuve, analyse statique et vérification runtime, 3

Solutions classiques d’ingénierie pour la fiabilité

Quelques stratégies bien connues issue du génie civil :

I Calcul précis/estimation des forces, tensions, etc.

I Redondance matérielle

I Conception robuste (une petite erreur n’est pas catastrophique)

I Séparation claire en sous-systèmes

I Utilisation des motifs dont on sait qu’ils fonctionnent

Master CILS: Preuve, analyse statique et vérification runtime, 4

Pourquoi ça ne marche pas pour les logiciels ?
I Les systèmes logiciels calculent des fonction non continues
Une simple inversion de bit peut changer le comportement complètement
I La redondance en répliquant ne protège pas des bugs
La redondance du développement n’est viable que dans des cas extrêmes
I Pas de séparation claire en sous-système
Une erreur locale affecte en général tout le système
I La conception logicielle a une très grande complexité logique
I La plupart des ingénieurs ne sont pas formés à la correction des logiciels
I Le coût supposé est souvent préféré à la fiabilité
I ...

Master CILS: Preuve, analyse statique et vérification runtime, 5

Test

Une solution contre le manque de fiabilité : le test

Limites :
I Le test montre la présence d’erreurs, pas leur absence
Exhaustivité possible uniquement pour des systèmes triviaux
I Problème de la représentativité des cas de test
Comment tester l’inattendu ? Les cas rares ?
I Le test demande du travail, donc coûte cher

I Il n’est pas toujours réalisable avant le déploiement

Master CILS: Preuve, analyse statique et vérification runtime, 6

Méthodes formelles

Méthodes rigoureuses utilisées lors de la conception du système et le

développement
I Fondées sur les mathématiques et la logique → formelles
I Construire un modèle de l’implémentation et des exigences (spécification)
I Utiliser des outils pour prouver mécaniquement que le modèle d’exécution
formel satisfait la spécification

Master CILS: Preuve, analyse statique et vérification runtime, 7

Plusieurs approches de méthodes formelles

I Model checking
I Preuve
I Analyse statique
I Méthodes formelles pendant la conception (raffinement)

Master CILS: Preuve, analyse statique et vérification runtime, 8

Runtime verification

Sur un système qui peut évoluer, on veut être sûr que le comportement reste
celui prévu
I Production de traces
I Monitoring

Master CILS: Preuve, analyse statique et vérification runtime, 9

Méthodes formelles et runtime verifications dans le cycle en V
Analyse des besoins
Recette
et faisabilité

Tests
Spécifications
de validation

Conception
Tests d'intégration
Architecturale

Conception détaillée Tests unitaires

Codage
Master CILS: Preuve, analyse statique et vérification runtime, 10
Méthodes formelles : Pour qui ?

Applications critiques : vies humaines ou coût faramineux en jeux

I Aéronautique et espace (A380)

I Ferroviaire (Métro 14)

I Hardware (Intel)

Mais pas seulement :

I Gain de temps avant la découverte des bugs

I Au final, moins cher que de corriger les bugs après coup

Exemple : Facebook (Infer)

Master CILS: Preuve, analyse statique et vérification runtime, 11

 But de la vérification formelle
Etant donnée une spécification formelle S d’un programme P,
donner une preuve mathématique rigoureuse que toute exécution de P satisfait S

P est correct par rapport à S

Que faut-il pour vérifier formellement P ?

I une spécification formelle de P (rigoureuse, mathématique),
I une méthode de preuve de correction (logique de Hoare par exemple),
I des règles de preuve pour faire des preuves rigoureuses, mathématiques : un
calcul.

Master CILS: Preuve, analyse statique et vérification runtime, 12

 Limitations de la vérification formelle

I pas de notion absolue de correction

La correction est toujours relative à une spécification donnée
I Difficile et coûteux d’écrire des spécifications formelles
En pratique, on ne spécifie pas formellement toutes les fonctionnalités mais
les propriétés de sûreté comme la bonne formation des données (accès hors
des bornes, déréférencement du pointeur null, etc.), l’absence d’exceptions
non détectées, les parties critiques du logiciel etc.
I Coûteux également de faire des preuves (mais on gagne sur le temps de test)

Master CILS: Preuve, analyse statique et vérification runtime, 13

 Limitations de la vérification formelle

I Il existe des propriétés difficiles ou impossibles à spécifier

ressources comme le temps et la mémoire (possible) le comportement de
l’utilisateur, l’environnement en général.
I Des programmes vérifiés formellement peuvent planter à l’exécution
• bugs dans le compilateur (→ vérification du compilateur C Compcert)
• bugs dans l’environnement d’exécution ( → vérification NICTA d’un
micro-kernel SEL4)
• bugs dans le matériel (→ preuve de hardware Intel par ex.)

Master CILS: Preuve, analyse statique et vérification runtime, 14

 Le test et la preuve sont
complémentaires

Master CILS: Preuve, analyse statique et vérification runtime, 15

Spécifications

Spécifications

Master CILS: Preuve, analyse statique et vérification runtime, 16

Spécifications

Conception par contrat

Idée : transférer la notion de contrat entre partenaires commerciaux aux
ingénieurs logiciel
I Qu’est-ce qu’un contrat
Un accord contraignant qui précise explicitement les obligations et les
bénéfices
I En ingénierie logicielle ? (une interface)
Fournisseur (implémenteur), en C, une procédure, en Java, une classe ou une méthode
Client Une procédure ou un objet appelant, voire un utilisateur humain (e.g. pour
main())
Contrat Un ensemble de clauses ensures/requires qui définissent les obligations
mutuelles du client et de l’implémenteur

Master CILS: Preuve, analyse statique et vérification runtime, 17

Spécifications

Exemple
La fonction racine carrée sur les entiers
/* @ requires a est un entier positif
* ensures l ’ entier retourne est la racine carree de a */
int root ( int a ) {
int i = 0;
int k = 1;
int sum = 1;
while ( sum <= a ) {
k = k +2;
i = i +1;
sum = sum + k ;
}
return i ;
}
Master CILS: Preuve, analyse statique et vérification runtime, 18
Spécifications

Formellement
Langage de spécification ACSL
/* @ requires a >= 0;
* ensures \ result *\ result <= a && (\ result +1)*(\ result +1) > a ; *
int root ( int a ) {
int i = 0;
int k = 1;
int sum = 1;
while ( sum <= a ) {
k = k +2;
i = i +1;
sum = sum + k ;
}
return i ;
}
Master CILS: Preuve, analyse statique et vérification runtime, 19
Spécifications

Exercice

Maximum de deux entiers

/* @ requires ?
* ensures ? */
int max ( int a , int b ) {
if ( a <= b )
return b ;
else
return a ;
}

Master CILS: Preuve, analyse statique et vérification runtime, 20

Spécifications

Plus d’expressivité
Indice maximum dans un tableau
/* @ requires sizeof ( a ) > 0;
ensures
\ forall int i ;
(0 <= i && i < sizeof ( a ))
== > a [ i ] <= a [\ result ]; */
int indice_max ( int a []) {
int i ;
int r = 0;
for ( i = 1; i < sizeof ( a ); i ++)
if ( a [ i ] > a [ r ]) r = i ;
return r ;
}

Master CILS: Preuve, analyse statique et vérification runtime, 21

Spécifications

Logique du premier ordre

Notation
math. ACSL Sémantique
> \true toujours vrai
⊥ \false toujours faux
¬A !A non A
A∧B A && B A et B
A∨B A || B A ou B
A⇒B A ==> B A implique B
∀x : i. A \forall i x; A pour tout x de type i, on a A
∃x : i. A \exists i x; A il existe un x de type i tel que A

Master CILS: Preuve, analyse statique et vérification runtime, 22

Spécifications

Exercices

Donner des spécifications aux fonctions suivantes :

int remainder ( int a , int b );
/* reste de la division euclidienne
de a par b */

int maxarray ( int a []);

/* retourne la valeur maximum du tableau a */

Master CILS: Preuve, analyse statique et vérification runtime, 23

Spécifications

Tri
int [] sort ( int a []);
/* tri du tableau a */

Master CILS: Preuve, analyse statique et vérification runtime, 24

Spécifications

Tri
int [] sort ( int a []);
/* tri du tableau a */
Tableau résultant trié :
ensures \ forall int i , j ;
0 <= i < j < sizeof ( a ) == > \ result [ i ] <= result [ j ];

Master CILS: Preuve, analyse statique et vérification runtime, 25

Spécifications

Tri
int [] sort ( int a []);
/* tri du tableau a */
Tableau résultant trié :
ensures \ forall int i , j ;
0 <= i < j < sizeof ( a ) == > \ result [ i ] <= result [ j ];
Tableau résultant permutation du tableau initial :
ensures sizeof (\ result ) == \ sizeof ( a ) &&
\ forall int i ; 0 <= i < sizeof ( a ) == >
\ exists int j ; 0 <= j < sizeof ( a ) &&
a [ i ] == \ result [ j ];
Est-ce assez ?
Master CILS: Preuve, analyse statique et vérification runtime, 26
Spécifications

Tri (cont.)

Non, [2; 1; 1] et [1; 2; 2].

Il faut que le nombre d’occurrences soient les mêmes : nouveau prédicat nbocc à
définir, puis
ensures \ forall int v ;
nbocc (a , v ) == nbocc (\ result , v );

Master CILS: Preuve, analyse statique et vérification runtime, 27

Spécifications

Tri en place

void sort ( int a []);

/* tri du tableau a en place */
Utilisation de \old pour accéder à la valeur avant la fonction.
ensures \ forall int i , j ;
0 <= i < j < sizeof ( a ) == > a [ i ] <= a [ j ];
ensures \ forall int v ;
nbocc (\ old ( a ) , v ) == nbocc (a , v );

Master CILS: Preuve, analyse statique et vérification runtime, 28

Logique de Hoare, Weakest Precondition

Logique de Hoare, Weakest Precondition

Master CILS: Preuve, analyse statique et vérification runtime, 29

Logique de Hoare, Weakest Precondition

Comment démontrer les spécifications ?

On donne au programme une sémantique

I L’état du système est abstrait par les propriétés logiques qu’il satisfait

I L’exécution des pas du programme modifie la validité de ses propriétés

On vérifie ensuite que les postconditions (ensures) sont bien impliquées par les
préconditions (requires) via l’exécution du programme.

Master CILS: Preuve, analyse statique et vérification runtime, 30

Logique de Hoare, Weakest Precondition

Logique de Hoare

Définie par Hoare (inventeur de QuickSort) en 1969

Pour les langages impératifs. Pour ce cours, C restreint à :
I Seulement des variables entières, pas de pointeurs

I Affectation x = e;

I Séquence { i1 ... in }

I Conditionnelle if (c) i1 else i2

I Boucle while (c) i

I Instruction vide ; (permet de ne pas avoir de else)

Master CILS: Preuve, analyse statique et vérification runtime, 31

Logique de Hoare, Weakest Precondition

Langages des assertions

L’état du système est décrit par des propositions de la logique du premier ordre
avec arithmétique
I P ::= b | P ∧ P | P ∨ P | ¬P | P ⇒ P | ∀x. P | ∃x. P

I b peut être n’importe quelle expression arithmétique du langage, mais sans

appel de fonction
I les variables du programme et celles de la logique sont identifiées

I implicitement, les variables prennent des valeurs entières

Exemple :
∀z. x ≤ z ⇒ y + 2 = z

Master CILS: Preuve, analyse statique et vérification runtime, 32

Logique de Hoare, Weakest Precondition

Triplet de Hoare

{P}c{Q} avec P et Q des assertions logiques et c un programme

I P : précondition
I Q : postcondition
I si x est une variable du programme, dans P et Q
x représente la valeur de x à ce point du programme

Lire : si la propriété P est vraie avant l’exécution de c et si l’exécution termine,

alors la propriété Q est vraie après l’exécution de c
(Correction partielle, pas de preuve de terminaison)

Master CILS: Preuve, analyse statique et vérification runtime, 33

Logique de Hoare, Weakest Precondition

Exemple

{x = n ∧ n > 0} y = 1; while (x != 1) { y = y * x; x = x - 1; }
{y = n! ∧ n > 0}

Ici, n est une variable logique, elle permet de se référer à la valeur de x au début
du programme

Master CILS: Preuve, analyse statique et vérification runtime, 34

Logique de Hoare, Weakest Precondition

Validité des triplets de Hoare

Tous les triplets de Hoare ne sont pas valides.
Intuitivement, on veut que {P}c{Q} soit valide si quand P est vrai avant
d’exécuter le programme, alors Q est vrai après l’exécution.

Exemple de triplets valides :

I {⊥}x = 5;{>}

I {x = y}x = x + 3;{x = y + 3}

I {x > 0}x = 2 * x;{x > −2}

I {x = a}if (x < 0) x = -x; else ;{x = |a|}

Mais {x < 0}x = x - 3{x > 0} n’est pas valide

Master CILS: Preuve, analyse statique et vérification runtime, 35

Logique de Hoare, Weakest Precondition

Logique de Hoare : les règles d’inférence

La validité des jugements est définie par induction sur le programme

Ensemble de règles de déduction (règles d’inférence) sur les triplets
I Les règles s’utilisent comme des règles d’inférence de logique.
F1 . . . Fk
F0
Ici les Fi sont des triplets de Hoare.
I Une règle exprime coment déduire un triplet (dénominateur) à partir
d’autres triplets (ceux du numérateur)

Master CILS: Preuve, analyse statique et vérification runtime, 36

Logique de Hoare, Weakest Precondition

Logique de Hoare : les règles d’inférence

I Pour montrer qu’un triplet F0 est dérivable, on doit construire un arbre de

dérivation de racine F0 en appliquant les règles d’inférence.

F1 F2 F4
F3 F5
F6
F0
I 1 règle par construction du langage + 2 règles logiques

Master CILS: Preuve, analyse statique et vérification runtime, 37

Logique de Hoare, Weakest Precondition

Skip

Pour toute proposition P :

skip
{P};{P}

; ne change pas l’état, si P est vraie avant, P est vraie après

Master CILS: Preuve, analyse statique et vérification runtime, 38

Logique de Hoare, Weakest Precondition

Séquence

{P}c1 {Q} {Q}c2 {R}

seq
{P}{c1 c2 }{R}

{c1 c2 } exécute c1 puis c2

Exemple :
{x > 2}x = x + 1;{x > 3} {x > 3}x = x + 2;{x > 5}
seq
{x > 2}{ x = x + 1; x = x + 2; }{x > 5}

Master CILS: Preuve, analyse statique et vérification runtime, 39

Logique de Hoare, Weakest Precondition

Affectation
aff
{[e/x]P}x = e;{P}

Rappel : [e/x]P est la formule P où toutes les occurrences libres de x ont été
substituées par e, par exemple [x + 1/x](x > 1) vaut x + 1 > 1
I L’affectation change l’état, il faut donc que la logique de Hoare reflète ce
changement
I De droite à gauche :
Pour que P soit vrai après l’exécution, il fallait que, pour un x remplacé par
sa nouvelle valeur, il soit vrai avant
Exemple : {x + 1 > 5}x = x + 1;{x > 5}

Master CILS: Preuve, analyse statique et vérification runtime, 40

Logique de Hoare, Weakest Precondition

Substitutions
[y/x]x =

Master CILS: Preuve, analyse statique et vérification runtime, 41

Logique de Hoare, Weakest Precondition

Substitutions
[y/x]x = y

Master CILS: Preuve, analyse statique et vérification runtime, 42

Logique de Hoare, Weakest Precondition

Substitutions
[y/x]x = y
[y/x]z =

Master CILS: Preuve, analyse statique et vérification runtime, 43

Logique de Hoare, Weakest Precondition

Substitutions
[y/x]x = y
[y/x]z = z

Master CILS: Preuve, analyse statique et vérification runtime, 44

Logique de Hoare, Weakest Precondition

Substitutions
[y/x]x = y
[y/x]z = z
[y/x]x > y =

Master CILS: Preuve, analyse statique et vérification runtime, 45

Logique de Hoare, Weakest Precondition

Substitutions
[y/x]x = y
[y/x]z = z
[y/x]x > y = y > y

Master CILS: Preuve, analyse statique et vérification runtime, 46

Logique de Hoare, Weakest Precondition

Substitutions
[y/x]x = y
[y/x]z = z
[y/x]x > y = y > y
[y/x](∀x, x mod 2 = 0 ⇒ x ∗ y = z) =

Master CILS: Preuve, analyse statique et vérification runtime, 47

Logique de Hoare, Weakest Precondition

Substitutions
[y/x]x = y
[y/x]z = z
[y/x]x > y = y > y
[y/x](∀x, x mod 2 = 0 ⇒ x ∗ y = z) =
∀x, x mod 2 = 0 ⇒ x ∗ y = z

Master CILS: Preuve, analyse statique et vérification runtime, 48

Logique de Hoare, Weakest Precondition

Substitutions
[y/x]x = y
[y/x]z = z
[y/x]x > y = y > y
[y/x](∀x, x mod 2 = 0 ⇒ x ∗ y = z) =
∀x, x mod 2 = 0 ⇒ x ∗ y = z
[y/x](∀z, z mod 2 = 0 ⇒ x ∗ x = z) =

Master CILS: Preuve, analyse statique et vérification runtime, 49

Logique de Hoare, Weakest Precondition

Substitutions
[y/x]x = y
[y/x]z = z
[y/x]x > y = y > y
[y/x](∀x, x mod 2 = 0 ⇒ x ∗ y = z) =
∀x, x mod 2 = 0 ⇒ x ∗ y = z
[y/x](∀z, z mod 2 = 0 ⇒ x ∗ x = z) =
∀z, z mod 2 = 0 ⇒ y ∗ y = z

Master CILS: Preuve, analyse statique et vérification runtime, 50

Logique de Hoare, Weakest Precondition

Substitutions
[y/x]x = y
[y/x]z = z
[y/x]x > y = y > y
[y/x](∀x, x mod 2 = 0 ⇒ x ∗ y = z) =
∀x, x mod 2 = 0 ⇒ x ∗ y = z
[y/x](∀z, z mod 2 = 0 ⇒ x ∗ x = z) =
∀z, z mod 2 = 0 ⇒ y ∗ y = z
[y/x](∀y, x mod 2 = 0 ⇒ x ∗ y = z) =

Master CILS: Preuve, analyse statique et vérification runtime, 51

Logique de Hoare, Weakest Precondition

Substitutions
[y/x]x = y
[y/x]z = z
[y/x]x > y = y > y
[y/x](∀x, x mod 2 = 0 ⇒ x ∗ y = z) =
∀x, x mod 2 = 0 ⇒ x ∗ y = z
[y/x](∀z, z mod 2 = 0 ⇒ x ∗ x = z) =
∀z, z mod 2 = 0 ⇒ y ∗ y = z
[y/x](∀y, x mod 2 = 0 ⇒ x ∗ y = z) =
renommage du y lié pour éviter la capture de y
[y/x](∀t, x mod 2 = 0 ⇒ x ∗ t = z) =

Master CILS: Preuve, analyse statique et vérification runtime, 52

Logique de Hoare, Weakest Precondition

Substitutions
[y/x]x = y
[y/x]z = z
[y/x]x > y = y > y
[y/x](∀x, x mod 2 = 0 ⇒ x ∗ y = z) =
∀x, x mod 2 = 0 ⇒ x ∗ y = z
[y/x](∀z, z mod 2 = 0 ⇒ x ∗ x = z) =
∀z, z mod 2 = 0 ⇒ y ∗ y = z
[y/x](∀y, x mod 2 = 0 ⇒ x ∗ y = z) =
renommage du y lié pour éviter la capture de y
[y/x](∀t, x mod 2 = 0 ⇒ x ∗ t = z) =
(∀t, y mod 2 = 0 ⇒ y ∗ t = z)
Master CILS: Preuve, analyse statique et vérification runtime, 53
Logique de Hoare, Weakest Precondition

Exemple

Soit le programme c suivant :

{ tmp = x ;
x = y;
y = tmp ; }
Montrer que {x = a ∧ y = b}c{y = a ∧ x = b} est valide

Master CILS: Preuve, analyse statique et vérification runtime, 54

Logique de Hoare, Weakest Precondition

Conditionnelle
{P ∧ b}c1{Q} {P ∧ ¬b}c2{Q}
if
{P}if (b) c1 else c2{Q}

I Quand la conditionnelle est exécutée, soit c1 soit c2 est exécuté

I Pour établir que Q est une post-condition, il faut donc que ce soit une
post-condition des deux branches
I De la même façon, P est une pré-condition des deux branches
I Dans la branche c1, on sait que la condition b est vraie, on peut donc
l’ajouter en pré-condition
I Similairement, on ajoute ¬b comme pré-condition de c2

Master CILS: Preuve, analyse statique et vérification runtime, 55

Logique de Hoare, Weakest Precondition

Utilisation
Prenons {x > 2}if (x>2) y = 1; else y = -1;{y > 0}
En utilisant la règle if, il faut donc montrer
{x > 2 ∧ x > 2}y = 1;{y > 0} et
{x > 2 ∧ ¬x > 2}y = -1;{y > 0}
ce que l’on peut simplifier en
{x > 2}y = 1;{y > 0} et
{⊥}y = -1;{y > 0}
Or à partir de la règle aff, on ne peut dériver que :
{1 > 0}y = 1;{y > 0} et
{−1 > 0}y = -1;{y > 0}
Les règles structurelles ne suffisent pas, il faut utiliser des règles logiques
Master CILS: Preuve, analyse statique et vérification runtime, 56
Logique de Hoare, Weakest Precondition

Conséquence gauche
Une condition P est dite plus forte qu’une condition Q si P ⇒ Q est valide
logiquement
Similairement, Q est dite plus faible que P.

P ⇒ P0 {P 0 }c{Q}
consG
{P}c{Q}

Il est correct de rendre une précondition plus spécifique (plus forte). Cette règle
permet de renforcer les préconditions.
Exemple :
x=4⇒x>2 {x > 2}x = x + 1;{x > 3}
consG
{x = 4}x = x + 1;{x > 3}

Master CILS: Preuve, analyse statique et vérification runtime, 57

Logique de Hoare, Weakest Precondition

Conséquence droite

De même, il est correct d’affaiblir une post-condition :

Q0 ⇒ Q {P}c{Q}’
consD
{P}c{Q}
Exemple :
x>3⇒x>1 {x > 2}x = x + 1;{x > 3}
consD
{x > 2}x = x + 1;{x > 1}

Master CILS: Preuve, analyse statique et vérification runtime, 58

Logique de Hoare, Weakest Precondition

Retour sur l’exemple

On a x > 2 ⇒ 1 > 0 donc à partir de {1 > 0}y = 1;{y > 0} on déduit

{x > 2}y = 1;{y > 0}
De même ⊥ ⇒ −1 > 0 donc à partir de {−1 > 0}y = −1;{y > 0} on déduit
{⊥}y = -1;{y > 0}
On peut donc finaliser la dérivation qui montre que
{x > 2}if (x>2) y = 1; else y = -1;{y > 0} est valide

Master CILS: Preuve, analyse statique et vérification runtime, 59

Logique de Hoare, Weakest Precondition

Boucle : intuition

On ne connaît a priori pas le nombre d’itération de la boucle

Idée :
I on considère une formule I qui sera vraie à chaque pas de la boucle

I I est appelé l’invariant de boucle

I il faut vérifier

• que I est bien valide en début de boucle

• que I est préservé lors de l’exécution de la boucle

Master CILS: Preuve, analyse statique et vérification runtime, 60

Logique de Hoare, Weakest Precondition

Boucle
{I ∧ b}c{I }
while
{I }while (b) c{I ∧ ¬b}

I I est appelé l’invariant de la boucle

I I est vrai à chaque tour de boucle (mais pas nécessairement au milieu d’un
tour)
I si la boucle s’arrête, la condition b est fausse et sa négation peut donc être
ajoutée en post-condition
I le corps de la boucle n’est exécuté que si la condition b est vraie, donc pour
vérifier que l’invariant est conservé après l’exécution de la boucle, on peut
ajouter b en précondition

Master CILS: Preuve, analyse statique et vérification runtime, 61

Logique de Hoare, Weakest Precondition

Exercice

Montrez que {x ≤ 0}while (x <= 5) x = x + 1;{x = 6} est valide.

Indication : vérifier que x ≤ 6 est un invariant de la boucle.

Master CILS: Preuve, analyse statique et vérification runtime, 62

Logique de Hoare, Weakest Precondition

Exercice
Soit c le programme :
{ i = 0;
s = 0;
while ( i != n ) {
i = i + 1;
s = s + 2 * i - 1; } }
Vérifier que s = i ∗ i est un invariant de la boucle.
Montrer que {>}c{s = n ∗ n} est valide (la somme des n premiers nombres
impairs est égale à n 2 ).

Master CILS: Preuve, analyse statique et vérification runtime, 63

Logique de Hoare, Weakest Precondition

Exercice

1. Montrer que pour tout P et tout c, le triplet de Hoare {P}c{>} est valide.

2. Montrer que pour tout P, Q et tout c, le triplet de Hoare

{P}while (1) c{Q} est valide.

Master CILS: Preuve, analyse statique et vérification runtime, 64

Logique de Hoare, Weakest Precondition

Automatisme

La logique de Hoare fournit un cadre général dans lequel on peut montrer la

correction des programmes.
En pratique, comment l’utiliser ?
I Quelles règles appliquer quand ?

I Comment prouver les implications des règles de conséquence ?

Master CILS: Preuve, analyse statique et vérification runtime, 65

Logique de Hoare, Weakest Precondition

Non-déterminisme

Étant donné un triplet de Hoare, pour essayer de montrer sa validité, on a

plusieurs choix :
I Appliquer la règle correspondant à la syntaxe du programme
I Appliquer une règle de conséquence

Master CILS: Preuve, analyse statique et vérification runtime, 66

Logique de Hoare, Weakest Precondition

Non-déterminisme
Étant donné un triplet de Hoare, pour essayer de montrer sa validité, on a
plusieurs choix :
I Appliquer la règle correspondant à la syntaxe du programme
• Comment trouver la propriété intermédiaire pour la séquence ?
{P}c1 {Q} {Q}c2 {R}
seq
{P}{c1 c2 }{R}
• Comment trouver l’invariant pour les boucles ?
{I ∧ b}c{I }
while
{I }while (b) c{I ∧ ¬b}
I Appliquer une règle de conséquence

Master CILS: Preuve, analyse statique et vérification runtime, 67

Logique de Hoare, Weakest Precondition

Non-déterminisme
Étant donné un triplet de Hoare, pour essayer de montrer sa validité, on a
plusieurs choix :
I Appliquer la règle correspondant à la syntaxe du programme
I Appliquer une règle de conséquence
• Gauche ou droite ?
• Comment trouver la bonne précondition plus forte, resp. la bonne
postcondition plus faible ?
P ⇒ P0 {P 0 }c{Q}
consG
{P}c{Q}
• Comment prouver P ⇒ P ? 0

Master CILS: Preuve, analyse statique et vérification runtime, 68

Logique de Hoare, Weakest Precondition

Plus faible précondition (Weakest precondition)

Définition
Soit c un programme et Q une formule, on note WP(c, Q) la plus faible
précondition telle que si c se termine, alors c se termine dans un état satisfaisant
Q.
Autrement dit :
I C’est une précondition qui mène à Q :
{WP(c, Q)}c{Q} est valide
I c’est la plus faible de celles-ci :
si {P}c{Q} est valide, alors P ⇒ WP(c, Q)
Théorème (Correction partielle avec WP)
Pour montrer {P}c{Q}, il suffit de montrer P ⇒ WP(c, Q).
Master CILS: Preuve, analyse statique et vérification runtime, 69
Logique de Hoare, Weakest Precondition

Calcul de WP

Sans les boucles, WP peut être calculée automatiquement :

I WP(;, Q) = Q

I WP(x = a;, Q) = [a/x]Q

I WP({c1 c2}, Q) = WP(c1, WP(c2, Q))
I WP(if (b) c1 else c2, Q) = (b ⇒ WP(c1, Q)) ∧ (¬b ⇒ WP(c2, Q))

Master CILS: Preuve, analyse statique et vérification runtime, 70

Logique de Hoare, Weakest Precondition

Exercice

Calculer :
I WP({x = x + 1; y = y - 1;}, x > y)
!
if (x > y) x = x - y;
I WP , (x > 0 ∧ y > 0)
else y = y - x;

Montrer en utilisant WP que

if (x % 2 == 0) x = x + 2;
{x = n} {x > n ∧ pair(x)}
else x = x + 1;

Master CILS: Preuve, analyse statique et vérification runtime, 71

Logique de Hoare, Weakest Precondition

Cas de la boucle
WP(while (b) c, Q) = pas de formule simple !

En effet while (b) c est (sémantiquement) équivalent à

if (b) { c; while (b) c } else {}
Donc WP(while (b) c, Q) =
(b ⇒ WP(c, WP(while (b) c, Q))) ∧ (¬b ⇒ Q)
Équation récursive pas toujours possible à calculer

On approxime WP par un prédicat plus simple à calculer et utilisable

automatiquement :
la condition de vérification

Master CILS: Preuve, analyse statique et vérification runtime, 72

Logique de Hoare, Weakest Precondition

Condition de vérification

On part d’un programme annoté :

I invariant de boucle

I spécification des fonctions

On note VC(c, Q) la condition de vérification de c pour l’assertion Q

La différence avec WP est qu’on utilise les annotations pour calculer VC

Master CILS: Preuve, analyse statique et vérification runtime, 73

Logique de Hoare, Weakest Precondition

Calcul de VC
I VC(;, Q) = Q
I VC(x = a;, Q) = [a/x]Q
I VC({c1 c2}, Q) = VC(c1, VC(c2, Q))
I VC(if (b) c1 else c2, Q) = (b ⇒ VC(c1, Q)) ∧ (¬b ⇒ VC(c2, Q))
IVC(while (b) c //@invariant I , Q) =
I ∧ Preserv ∧ Final (l’invariant est vérifié en début de boucle)
où
Preserv = ∀x1 , . . . , xm . I ∧ b ⇒ VC(c, I )
(l’invariant est préservé par une itération)
Final = ∀x1 , . . . , xm . ¬b ∧ I ⇒ Q
(la postcondition est satisfaite lorsque la boucle se termine)
x1 . . . xm sont les variables modifiées dans c
Master CILS: Preuve, analyse statique et vérification runtime, 74
Logique de Hoare, Weakest Precondition

Exemple
On reprend la factorielle :
{x = n ∧ n > 0}{ y = 1; while (x != 1) { y = y * x; x = x - 1; } }
{y = n! ∧ n > 0}
On prend comme invariant Inv = (y ∗ x! = n! ∧ x > 0 ∧ n > 0)
On a VC(fact, y = n! ∧ n > 0) =
1 ∗ x! = n! ∧ x > 0 ∧ n > 0
 
∧ ∀xy. (Inv ∧ x 6= 1) ⇒ (y ∗ x ∗ (x − 1)! = n! ∧ x − 1 > 0 ∧ n > 0)
 
∧ ∀xy. (x = 1 ∧ Inv) ⇒ (y = n! ∧ n > 0)
On peut “facilement” montrer que x = n ∧ n > 0 ⇒ VC(fact, y = n! ∧ n > 0)

Master CILS: Preuve, analyse statique et vérification runtime, 75

Logique de Hoare, Weakest Precondition

Correction des conditions de vérification

Lemme
Si {P}c{Q} est valide et R ne contient pas de variable libre modifiée par c, alors
{P ∧ R}c{Q ∧ R} est valide.
Théorème
{VC(c, Q)}c{Q} est valide.
Preuve : par induction sur c

Théorème
Si P ⇒ VC(c, Q) alors {P}c{Q} est valide.
Preuve : condG appliqué au théorème précédent.

Master CILS: Preuve, analyse statique et vérification runtime, 76

Logique de Hoare, Weakest Precondition

Génération de conditions de vérification

Grâce aux programmes annotés et à VC, on obtient une méthode réaliste pour
faire de la preuve de programmes impératifs :
I Écrire un programme contenant les invariants des boucles et éventuellement
des assertions à certains point du programme difficiles pour la preuve ;
I Transmettre ce code annoté à un outil qui engendre les conditions de
vérification (exemple : plugin WP de Frama-C, cf. TP) ;
I Prouver ces conditions de vérification, de préférence avec un prouveur
automatique (alt-ergo, Z3, Vampire, . . .) ou interactif (Coq, Isabelle, . . .)

Master CILS: Preuve, analyse statique et vérification runtime, 77

Frama-C et WP

Frama-C et WP

Master CILS: Preuve, analyse statique et vérification runtime, 78

Frama-C et WP

Frama-C
I A framework for modular analysis of C code
I Frama-C : plateforme développé par le CEA et INRIA pour la vérification de
programmes C (analyse statique, preuve déductive . . . )
I http://frama-c.com, distribué sous LGPL (Fluorine v3 en juin 2013)
I Noyau construit sur CIL (Necula et al., Berkeley)
I ACSL langage d’annotations
I Plateforme extensible :
• Collaboration d’analyseurs sur un même code
• Communication entre les plugins via les annotations ACSL
• Ajout facile de nouveaux plugins

Master CILS: Preuve, analyse statique et vérification runtime, 79

Frama-C et WP

included in main distribution

Ecosystème des plugins distributed externally

Value Analysis
Jessie WP
Aoraï
Agen

Specification Generation
Abstract Interpretation Deductive Verification Mthread

Concurrency
Formal Methods
Executable-ACSL

Code Transformation Frama-C Plug-Ins

Dynamic Analysis PathCrawler

Spare code
Semantic constant folding SANTE
Browsing of unfamiliar code
Slicing

Scope & Data-flow browsing

Metrics computation Variable occurrences

Impact Analysis

Crédits : Kosmatov, Signoles

Master CILS: Preuve, analyse statique et vérification runtime, 80
Frama-C et WP

Main plugins of Frama-C ?

I Value analysis Static verification of C code using Abstract Interpretation

techniques
I WP
Static verification of C code using Weakest Precondition calculus
Jessie, a similar tool
I A lot of other plugins useful in specific cases
InOut (computation of outputs from inputs), Metrics (analyze code
complexity), Aorai (temporal verification), PathCrawler (test generation),
Spare code (remove spare code), ...

Master CILS: Preuve, analyse statique et vérification runtime, 81

Frama-C et WP

Contrat de fonctions : les principes

Objectif : spécification de programmes/fonctions impératifs
Approche : donner des propriétés sur les fonctions
I la pré-condition est supposée vraie à l’entrée dans la fonctions (assurée par
l’appelant de la fonction)
I la post-condition doit être vraie à la sortie de la fonction (assurée par la
fonction si elle termines)
I rien n’est garanti si la pré-condition n’est pas satisfaite
I terminaison peut être garantie ou non (correction totale vs correction
partielle)

Master CILS: Preuve, analyse statique et vérification runtime, 82

Frama-C et WP

Annotations en ACSL
requires introduit une pré-condition
requires n>=0;
\result représente le résultat de la fonction
ensures introduit une post-condition
ensures \result>=0;
assigns précise les (locations mémoire des) variables
que la fonction a le droit de modifier
en dehors de ses variables locales
assigns \nothing ;
loop invariant invariant de boucle
loop variant variant
loop assigns spécifie les variables modifiées par la boucle

Master CILS: Preuve, analyse statique et vérification runtime, 83

Frama-C et WP

Validité des emplacements mémoire

\valid précise la validité des emplacements-mémoire
\valid(p) : validité de *p
\valid(p+(x..y)) : validité de *(p+x) .. *(p+y)
Ce prédicat peut s’utiliser dans un contrat ou toute assertion (invariant de
boucle)

Master CILS: Preuve, analyse statique et vérification runtime, 84

Frama-C et WP

Spécification par cas, behaviors

Pour spécifier plusieurs cas possibles (behaviors)
Dans chaque behavior : la clause assumes détermine dans quel cas un behavior
s’applique. La clause ensures spécise le comportement dans ce cas.
On peut aussi avoir une post-condition qui s’applique à tous les cas.

/* @ requires -100 <= x <= 100;

assigns \ nothing ;
behavior pos : assumes x >= 0;
ensures \ result == x;
behavior neg : assumes x < 0;
ensures \ result == -x; */

Master CILS: Preuve, analyse statique et vérification runtime, 85

Frama-C et WP

Behaviors (cont.)

I complete behaviors : les comportements décrits couvrent tous les cas

I disjoint behaviors : les comportements ne se recouvrent pas.

Ces deux clauses générent des obligations de preuve.

Master CILS: Preuve, analyse statique et vérification runtime, 86

Frama-C et WP

Interface graphique

Master CILS: Preuve, analyse statique et vérification runtime, 87

Frama-C et WP

Interface textuelle

frama-c -wp getMin.c

ou
frama-c -wp getMin.c -wp-prover XX
avec XX ∈ {z3, cvc3, simplify, coq ..} = ensemble des prouveurs disponibles.

Master CILS: Preuve, analyse statique et vérification runtime, 88

Frama-C et WP

frama-c -wp find.c -wp-prover cvc3

[kernel] preprocessing with "gcc -C -E -I. find.c"

[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[wp] 9 goals scheduled
[wp] [Qed] Goal typed_find_loop_inv_established : Valid
[wp] [Qed] Goal typed_find_loop_assign : Valid
[wp] [Qed] Goal typed_find_loop_term_decrease : Valid
[wp] [Cvc3] Goal typed_find_complete_not_found_found : Valid (20ms)
[wp] [Qed] Goal typed_find_loop_term_positive : Valid
[wp] [Cvc3] Goal typed_find_loop_inv_preserved : Valid (20ms)
[wp] [Cvc3] Goal typed_find_disjoint_not_found_found : Valid (20ms)
[wp] [Cvc3] Goal typed_find_found_post : Valid (Qed:4ms) (20ms)
[wp] [Cvc3] Goal typed_find_not_found_post : Valid (720ms)
Master CILS: Preuve, analyse statique et vérification runtime, 89
Frama-C et WP

Un exemple : getMin
Spec informelle : Calculer le plus petit élément d’un tableau non vide
/* @ r e qu i r e s \ valid ( t +(0.. n -1)) && n > 0;
ensures \ forall integer i ; 0 <= i < n == > \ result <= t [ i ];
*/
int getMin ( int t [] , int n ) {
int res = t [0];
/* @ loop i n v a r i a n t 1 <= i <= n &&
(\ forall integer j ; 0 <= j < i == > res <= t [ j ]);
loop assigns res ;
loop variant n - i ;
*/
for ( int i = 1; i < n ; i ++)
if ( t [ i ] < res ) res = t [ i ];
return res ;
}

WP : OK

Master CILS: Preuve, analyse statique et vérification runtime, 90

Frama-C et WP

Mais la spécification n’est pas complète ...

/* @ requires \ valid ( t +(0.. n -1)) && n > 0;
ensures \ forall integer i ; 0 <=i < n == > \ result <= t [ i ];
*/
int getMin_wrong ( int t [] , int n ) {
int res = t [0];
/* @ loop invariant 1 <= i <= n &&
(\ forall integer j ; 0 <= j < i == > res <= t [ j ]);
loop assigns res ;
loop variant n - i ;
*/
for ( int i = 1; i < n ; i ++)
if ( t [ i ] < res ) res = t [ i ];
return ( res -1);
}

WP : OK
Master CILS: Preuve, analyse statique et vérification runtime, 91
Frama-C et WP

/* @ r eq u i r e s \ valid ( t +(0.. n -1)) && n > 0;

ensures \ forall integer i ; 0 <= i < n == > \ result <= t [ i ];
- - - > ensures \ exists integer k ; 0 <= k < n && \ result == t [ k ];
*/
int getMin ( int t [] , int n ) {
int res = t [0];
/* @ loop i n v a r i a n t 1 <= i <= n &&
(\ forall integer j ; 0 <= j < i == > res <= t [ j ]);
--> loop i n v a r i a n t
\ exists integer k ; 0 <= k < i && res == t [ k ];
loop assigns res ;
loop variant n - i ;
*/
for ( int i = 1; i < n ; i ++)
if ( t [ i ] < res ) res = t [ i ];
return res ;
}

WP : OK Attention à ce que l’on prouve ...

Master CILS: Preuve, analyse statique et vérification runtime, 92

Frama-C et WP

Les entiers : C et ACSL

ACSL utilise des entiers mathématiques (integer) alors qu’à l’exécution C utilise
des entiers machine (int)
On peut utiliser les entiers bornés si besoin.
On peut aussi vérifier les overflows (RTE - runtime error).

Master CILS: Preuve, analyse statique et vérification runtime, 93