Flashcards: Analyse avancée de la sécurité et preuve de programmes — 24 cards

Analyse de liveness — définition ?

Détermine si une variable influence une observation future.

Affectation morte — quand ?

Quand x ∉ Lo après l'affectation.

Code mort — élimination ?

Suppression d'instructions inutiles sans changer le comportement.

Boucle while — invariant ?

Calculé par point fixe jusqu'à stabilité.

Variable live — influence ?

Peut affecter une observation future.

Initialisation Java — problème ?

Variables non initialisées détectées par sur-approximation.

Analyse en arrière — rôle ?

Ajoute obs(T) pour variables bien initialisées.

Analyse en avant — rôle ?

Vérifie que variables utilisées sont initialisées.

Null pointer — domaine ?

Modélise nullité pour détection d'erreurs.

Invariant boucle — propriété ?

Vrai à l'entrée, conservé, garantit la postcondition.

Variables bien initialisées — définition ?

Ne sont pas live-in à l'entrée.

Boucle while — condition de sortie ?

Croiser invariant avec ¬C pour raffiner l'état.

Code mort — impact ?

Optimise sans changer le comportement observable.

Initialisation Java — problème indécidable ?

Oui, sur-approximation conservative nécessaire.

Nullité — assertion ?

Croise nullité avec domaine abstrait.

CFG — syntaxe ?

pc:=PC1; assume; Kk; Bk; branches conditionnelles.

CFG — état abstrait ?

Associe chaque PC à L ou G(p').

CFG — règle branchement ?

Test inutile si LA(p1)=LA(p2) et C morte.

Itération CFG — but ?

Atteindre stabilité des états jusqu'au point fixe.

Domaine pointeurs — représentation ?

(Z,N) : Z=F si non NULL, N=F si NULL.

Déréférencement — règle ?

Vert si p ≠ NULL certain, rouge si NULL certain.

Assertions nullité — croisement ?

Avec couples (Z,N), intersection pour compatibilité.

Prove WP — objectif ?

Vérifier invariants, pré/postconditions, terminaison.

Vulnérabilités C classiques ?

Débordements, comportements indéfinis, UAF, injections.