Ataques Spectre y Defensas
26 Mayo 2021 - https://meet.google.com/qeh-kntz-som
Fecha: 26/05/2021 11 hs.
Título: Ataques Spectre y Defensas
Expositor: Tamara Rezk (INRIA Sophia Antipolis-Méditerranée)
Meet: https://meet.google.com/qeh-kntz-som
Resumen:
El año 2018, la revelación de espectros en los procesadores convirtieron a algunos investigadores de seguridad en caza-fantasmas.
Aunque parezca fantasía, estos espectros, llamados ataques Spectre en inglés, son bien reales y pueden causar graves problemas
a la hora de proteger la confidencialidad de la información.
Los espectros son rastros de secretos que pueden dejar los programas al ejecutarse en procesadores modernos con el uso de un mecanismo de hardware conocido como ejecución especulativa.
Los rastros son explotados por los atacantes oportunistas para recuperar los secretos, por ejemplo las claves de criptografía usadas por librerías.
En esta charla, les contaré un poco más en detalle sobre los espectros, algunas defensas, cómo modelarlos utilizando semántica formal y cómo diseñar métodos para detectarlos (o cazarlos!) en software.
Mini Bio:
Tamara Rezk es directora de investigación en Inria Sophia-Antipolis Méditerranée, Francia, en dónde trabaja desde 2007. Su tema principal de investigación es la seguridad de programas y sistemas. Sus intereses incluyen análisis de programas para detectar violaciones de seguridad, seguridad de la Web, verificación de propiedades de seguridad en compiladores, y formalización de ataques y defensas conocidos.
Entre 2006 y 2007 Tamara hizo un postdoc en el Joint-Lab de Microsoft Research e Inria en el tema de verificación de protocolos criptográficos generados automáticamente por compilador.
En noviembre 2006, Tamara recibió un PhD de la Universidad de Nice Sophia-Antipolis. Su tesis fue supervisada por Gilles Barthe y el sujeto de su tesis fue la verificación de propiedades de confidencialidad en código móvil.
En 2002, Tamara recibió el título de Licenciada en Ciencias de la Computación de FaMAF, Universidad Nacional de Córdoba. Su tesina fue supervisada por Javier Blanco y el sujeto fue la verificación de programas con punteros usando la lógica de separación.