vérification formelle de la plate-forme JavaCard - Melo de Sousa, Simão
50,99 €
inkl. MwSt.
Versandkostenfrei*
Versandfertig in 6-10 Tagen
  • Broschiertes Buch

La vérification du bytecode est l'une des pièces maîtresses de la sécurité de l'architecture JavaCard. Sa correction est souvent formulée en utilisant les notions de machine virtuelle défensive et de machine virtuelle offensive. La machine virtuelle défensive vérifie la cohérence des données manipulées pendant l'exécution alors que la machine offensive ne fait pas de telles vérifications. La correction est ainsi établie en vérifiant que l'exécution de programmes qui ont passé avec succès la vérification de bytecode, sur les deux machines, coïncide. Dans cet ouvrage nous décrirons comment sont…mehr

Andere Kunden interessierten sich auch für
Produktbeschreibung
La vérification du bytecode est l'une des pièces maîtresses de la sécurité de l'architecture JavaCard. Sa correction est souvent formulée en utilisant les notions de machine virtuelle défensive et de machine virtuelle offensive. La machine virtuelle défensive vérifie la cohérence des données manipulées pendant l'exécution alors que la machine offensive ne fait pas de telles vérifications. La correction est ainsi établie en vérifiant que l'exécution de programmes qui ont passé avec succès la vérification de bytecode, sur les deux machines, coïncide. Dans cet ouvrage nous décrirons comment sont spécifiées de telles machines virtuelles et comment sont définis de tels énoncés de correction dans les assistants de preuve. Nous nous concentrerons en particulier sur le problème de l'automatisation de la construction de machines virtuelles offensives et de vérifieurs de bytecode à partir de machines virtuelles défensives.
Autorenporträt
Simão Melo de Sousa est professeur d'informatique à l'Universitéde Beira Interior (Portugal) où il enseigne dans le domaine de lala compilation, les fondements et les logiques de laprogrammation, les méthodes formelles et la sécurité.Docteur de l'INRIA Sophia-Antipolis/UNSA, il est expert enfiabilité et sécurité des systèmes informatiques.