La verification du bytecode est l'une des pieces maitresses de la securite de l'architecture JavaCard. Sa correction est souvent formulee en utilisant les notions de machine virtuelle defensive et de machine virtuelle offensive. La machine virtuelle defensive verifie la coherence des donnees manipulees pendant l'execution alors que la machine offensive ne fait pas de telles verifications. La correction est ainsi etablie en verifiant que l'execution de programmes qui ont passe avec succes la verification de bytecode, sur les deux machines, coincide. Dans cet ouvrage nous decrirons comment sont specifiees de telles machines virtuelles et comment sont definis de tels enonces de correction dans les assistants de preuve. Nous nous concentrerons en particulier sur le probleme de l'automatisation de la construction de machines virtuelles offensives et de verifieurs de bytecode a partir de machines virtuelles defensives.

Данное издание не является оригинальным. Книга печатается по технологии принт-он-деманд после получения заказа.