Ly, Dara
[Author]
;
Orléans
[Contributor];
Loulergue, Frédéric
[Contributor]
Formalisation d'un vérificateur dynamique de propriétés mémoire pour programmes C ; Formalization of a Runtime Assertion Checker for Memory Properties of C Programs
You can manage bookmarks using lists, please log in to your user account for this.
Media type:
Text;
Electronic Thesis;
Still Image;
E-Book
Title:
Formalisation d'un vérificateur dynamique de propriétés mémoire pour programmes C ; Formalization of a Runtime Assertion Checker for Memory Properties of C Programs
Footnote:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Description:
La vérification d'assertions à l'exécution est une technique permettant de contrôler, lors de leur exécution, la conformité d'un programme vis-à-vis d'une spécification donnée sous forme d'annotations formelles : les assertions. Un procédé appelé instrumentation transforme les assertions en code exécutable, de manière à mettre en œuvre un moniteur en ligne pour le programme à vérifier. Le long de l'exécution du programme instrumenté, le moniteur contrôle la conformité du programme vis-à-vis des assertions, et, en cas de non-respect d'une assertion, met fin à l'exécution. Autrement, il laisse le comportement fonctionnel du programme inchangé. La complexité de mise en œuvre de l'instrumentation dépend largement des propriétés exprimables dans le langage d'annotation. Dans le cas de programmes en langage C, l'outil E-ACSL (greffon de Frama-C, une plateforme open-source d'analyse de code C), permet la vérification de propriétés relatives à l'état mémoire du programme, mais requiert pour cela une instrumentation complexe. La présente thèse est consacrée à la formalisation de cette instrumentation : il s'agit d'en donner une définition précise et d'étudier ses propriétés sémantiques. Nous proposons une modélisation du problème comme une traduction de programmes depuis un langage source, muni d'assertions logiques, vers un langage cible. Ce dernier est dépourvu d'assertions logiques, mais intègre une structure de données, appelée mémoire d'observation, dédiée au suivi des propriétés mémoire. Nous donnons une caractérisation axiomatique de la mémoire d'observation, et utilisons celle-ci pour définir la sémantique du langage cible de la transformation, dont nous montrons qu'elle est correcte vis-à-vis de la sémantique des langages concernés.Additionnellement, nous étudions l'optimisation de l'instrumentation par analyse de flot de données, technique mise en œuvre dans l'outil E-ACSL afin de réduire le surcoût en performance induit par l'instrumentation. L'analyse vise à déterminer un sous-ensemble d'emplacements mémoire ...