Évaluation de l’impact de fautes matérielles sur le logiciel par Model Checking,
Auteur(s): D. BASSOLE, Jean-Louis Lanet, and Axel Legay
Auteur(s) tagués: Didier BASSOLE ;
Résumé

La mutation de programme dû à un défaut d'environnement est susceptible de générer des problèmes de sécurité comme la non exécution de procédure de vérification, le saut de bloc d'instruction etc.. Pour les éradiquer il est nécessaire de comprendre les effets de ces perturbations sur le logiciel. Souvent les travaux explorent les effets au niveau d'un langage de haut niveau sans prendre en compte les effets des architectures matérielles sous-jacentes. Nous proposons de travailler au niveau du langage binaire en prenant en compte l'architecture matérielle. Nous modélisons à la fois l'unité centrale et le programme et nous définissons une transformation de l'état par mutation en fonction du modèle de faute défini.

Mots-clés

962
Enseignants
5577
Publications
49
Laboratoires
84
Projets