• Medientyp: E-Book; Sonstige Veröffentlichung; Elektronische Hochschulschrift
  • Titel: Vérification d'isolation de fautes logicielle ; Verifying Software Fault Isolation
  • Beteiligte: Lepiller, Julien [VerfasserIn]
  • Erschienen: theses.fr, 2019-12-11
  • Sprache: Englisch
  • Schlagwörter: Interprétation abstraite ; Sémantique ; SFI ; Semantics ; Weak Memory Models ; Verification ; Abstract Interpretation ; Modèles mémoire faibles ; Vérification
  • Entstehung:
  • Anmerkungen: Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
  • Beschreibung: 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 ...
  • Zugangsstatus: Freier Zugang