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.