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.

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.