Université de Rennes 1 Vérification d'isolation de fautes logicielle Verifying Software Fault Isolation VérificationSFISémantiqueInterprétation abstraiteModèles mémoire faibles VerificationSFISemanticsAbstract InterpretationWeak Memory Models Logiciels -- Vérification Nous sommes habitués à utiliser des ordinateurs sur lesquels coopèrent des programmes d'origines diverses. Chacun de ces programmes a besoin d'accéder à de la mémoire vive pour fonctionner correctement, mais il ne faudrait pas qu'un programme accède ou modifie la mémoire d'un autre programme. Si cela ce produisait, les programmes ne pourraient plus faire confiance à la mémoire et pourraient se comporter de manière erratique. Les programmeurs n'ont pourtant pas besoin de se mettre d'accord à l'avance sur les zones mémoire qu'ils pourront ou non utiliser. Le matériel s'occupe d'allouer des zones de mémoire distinctes pour chaque programme. Tout cela est transparent pour le programmeur. Un programme malveillant ne pourrait d'ailleurs pas non plus accéder ou modifier la mémoire d'un autre programme pour l'attaquer directement. Mais il existe une catégorie de programmes qui ne bénéficient pas de cette protection : les modules qui étendent les fonctionnalités d'autres programmes, comme un module complémentaire de navigateur. Cette thèse repose sur une technique d'isolation de faute logicielle, et non matérielle et en propose deux sémantiques, l'une parallèle et pas l'autre, ainsi qu'un analyseur statique basé sur l'interprétation abstraite. Elle présente aussi une preuve de correction de l'analyseur. We are used to use computers on which programs from diverse origins are installed and running at the same time. Each of these programs need to access memory for proper operation, but none of them should access or modify the memory of another. If this happened, programs would not be able to trust their memory and could start behaving erratically. Still, programmers do not need to coordinate and agree in advance on what parts of the memory they are allowed to use or not. Hardware takes care of allocating distinct memory zones for each program. This is completely transparent to the programmer. A malware cannot access or modify the memory of another program to attack it directly either. However, there exists a category of programs that do not benefit from this protection: modules that extend the features of other programs, such as plugins in a web browser. This thesis is based on a software (and not hardware) fault isolation technique, and proposes two semantics for it, single-threaded and multi-threaded, as well as a static analyzer based on abstract interpretation. We also present a proof of correctness for the analyzer. Electronic Thesis or DissertationText en application/pdf1 : 2110 Kohttps://ged.univ-rennes1.fr/nuxeo/site/esupversions/e2ba19bf-1a0a-4f5d-ba9f-e0da2e900c33 Lepiller Julien 1993-03-09 FR 243016069 julien-these@lepiller.eu 2019REN1S067 http://www.theses.fr/2019REN1S067 2019-12-11 Informatique Universite de Rennes 1thesis.degree.grantor_1 02778715X Doctorat non ouiJensenThomasintervenant_1059884959 MATHSTICecoleDoctorale_1 204770424 Universite Bretagne LoirepartenaireRecherche_1 191639044 IRISA partenaireRecherche_2 026386909 ddc:004 JensenThomasUniversite de Rennes 1Sciences et technologie, medecine, pharmacie, odontologie, droit, economie, gestion, philosophieMATHSTICÉcole doctorale Mathématiques et sciences et technologies de l'information et de la communication (Rennes)Universite Bretagne Loire Communaute des etablissements d enseignement superieur et de recherche (ComuE) IRISA ASCII PDF 2160258