Los ataques Spectre y Meltdown en los microprocesadores modernos representan una nueva clase de ataques que han sido difíciles de abordar. Subrayan vulnerabilidades en el diseño de hardware que han pasado desapercibidas durante años. Esto muestra la debilidad del proceso de verificación y las prácticas de diseño de vanguardia. Estos ataques son independientes del sistema operativo y no explotan vulnerabilidades de software. Además, violan todas las suposiciones de seguridad garantizadas por los procedimientos estándar de seguridad (por ejemplo, el aislamiento del espacio de direcciones) y, como resultado, cualquier mecanismo de seguridad construido sobre estas garantías. Estas vulnerabilidades permiten al atacante recuperar datos filtrados sin acceder directamente al secreto. De hecho, hacen uso de canales encubiertos, que son mecanismos de comunicación oculta que transmiten información sensible sin ningún flujo de información visible entre la parte maliciosa y la víctima. La causa raíz de este tipo de ataques de canal lateral radica en la ejecución especulativa y fuera de orden de las microarquitecturas modernas de alto rendimiento. Dado que los procesadores modernos son difíciles de verificar con técnicas estándar de verificación formal, presentamos una metodología que muestra cómo transformar un modelo realista de un procesador especulativo y fuera de orden en uno abstracto. Siguiendo enfoques relacionados de verificación formal, simplificamos el modelo bajo consideración mediante pasos de abstracción y refinamiento. También presentamos un enfoque para verificar formalmente el modelo abstracto utilizando un verificador de modelos estándar. Se introduce el flujo teórico, basado en resultados de verificación formal establecidos, y se proporciona un esquema de prueba de solidez y corrección. Finalmente, demostramos la viabilidad de nuestro enfoque, aplicándolo en una arquitectura de procesador inspirada en DLX RISC con segmentación de tuberías. Mostramos resultados experimentales preliminares para respaldar nuestra afirmación, realizando Verificación de Modelo Acotada con un verificador de modelos de vanguardia.