Themida y CodeVirtualizer, desarrollados por Oreans Technology, son protectores comerciales que traducen código nativo a una máquina virtual interna con un juego de instrucciones propio, un esquema que también emplea VMProtect y que comparten vxlang, EagleVM, Covirt y BinProtect. Este artículo describe una técnica de desvirtualización estática aplicable a Themida, aunque extensible a la mayoría de ofuscadores basados en máquinas virtuales con ajustes menores.
La principal diferencia arquitectónica de Themida respecto a VMProtect es su soporte para virtualización anidada, posible porque el contexto y la pila virtual residen dentro del binario en lugar de en la pila nativa. El texto no profundiza en la arquitectura interna y se centra en el método de desvirtualización. El autor desaconseja mapear handlers de la VM a instrucciones x86 mediante patrones: cualquier cambio del proveedor en la disposición de los handlers, las tablas de opcodes o la lógica de despacho invalida silenciosamente la herramienta. Cuanto más dependa la implementación de detalles específicos de la VM, más frágil será.
La propuesta se basa en evaluación simbólica guiada. La idea central consiste en levantar las instrucciones nativas a una representación intermedia maleable e impulsar el lifting concretizando el flujo de control a medida que las optimizaciones resuelven destinos de bifurcación desconocidos. El motor empleado es BLARE2, mantenido por Back Engineering Labs, con soporte para AMD64 y ARM64, una IR en SSA propia, sistema de pases, optimizador, selector de instrucciones, asignador de registros y enlazador. Su diferencial frente a Triton o Remill es que BLARE2 puede bajar el IR optimizado a código nativo y reinsertarlo en el binario, produciendo una salida casi 1:1 con el original.
Al iniciar la evaluación simbólica, todos los registros y flags son simbólicos, salvo RSP, que recibe un valor concreto. Esta elección de diseño permite que la maquinaria existente de propagación de cargas y almacenes gestione los accesos a pila de forma automática. La limitación es que las funciones con asignaciones dinámicas en la pila, como alloca o VLAs, no se admiten: un caso poco frecuente en el código que suele terminar virtualizado.
Reducir por completo la virtualización de Themida o VMProtect no exige un conjunto exhaustivo de optimizaciones de compilador. En la práctica basta con un puñado de pases ejecutados hasta converger para colapsar todo el andamiaje de la VM. Dichos pases no son independientes: una carga de bytecode se promociona a constante en cuanto su dirección se concreta, lo que desencadena nuevas simplificaciones. El artículo prosigue con el detalle de cada pase y con el tratamiento del branching virtual y los VMEXIT, los únicos puntos donde resulta imprescindible cierto conocimiento específico de la VM.