Levantando Modelos de Micro-Atualização do RTL para Análise de Segurança Formal

Ataques de execução de hardware exploram interações microarquitetônicas sutis para vazar dados secretos. Embora verificar programas quanto à existência de tais ataques seja essencial, a verificação de software em relação à implementação completa de hardware não é escalável. A verificação usando modelos formais abstratos do hardware pode ajudar a fornecer fortes garantias de segurança enquanto aproveita a abstração para alcançar escalabilidade. No entanto, escrever modelos abstratos precisos é tedioso e propenso a erros. Portanto, precisamos de técnicas para gerar modelos que possibilitem uma análise de segurança sólida, mas escalável, automaticamente.