Virtualización

Formally verified countermeasures against cache based attacks in virtualization platforms

Los ataques basados en el cache son una clase de ataques de canal lateral (side-channel) particularmente efectivos en entornos virtualizados o basados en la nube, donde han sido usados para recuperar claves secretas de implementaciones criptográficas. Un enfoque común para frustrar los ataques basados en cache es usar implementaciones de tiempo constante (constant-time), las cuales no tienen bifurcaciones basadas en secretos, y no realizan accesos a memoria que dependan de secretos.

Continuar leyendo

Especificacion y verificacion formal de modelos de virtualizacion

Este proyecto, que se enmarca en un proyecto de investigación más general, aborda el estudio del comportamiento de plataformas de computación virtuales. Concretamente, se focaliza en la especificación y verificación formal de determinadas propiedades de seguridad, que es deseable sean garantidas por plataformas de virtualización sobre las que son ejecutadas variedades de máquinas virtuales que ofician de hosts a sistemas operativos, sean estos confiables o no. En particular, interesa modelar formalmente la interacción de diferentes sistemas operativos ejecutando sobre una misma plataforma virtualizada y establecer cuáles son los mecanismos que garantizan determinadas propiedades de no interferencia, particularmente en relación a los datos manejados por los sistemas que ejecutan concurrentemente sobre esa plataforma.

Continuar leyendo

Design and Development of a Framework for IT-Security training

Este proyecto se encuentra motivado por el desarrollo de una herramienta que asista en la creación de laboratorios de seguridad informática, dichos laboratorios permiten a los estudiantes asimilar, mediante la práctica, los conceptos adquiridos en los cursos teóricos. Los diferentes laboratorios tratan temas como: criptografía aplicada, monitoreo de redes, seguridad en sistemas operativos, seguridad en aplicaciones, etc. La solución propuesta y desarrollada por los estudiantes debe poder generar ambientes de ensayos que emulen de manera fidedigna los ambientes de producción reales y en los cuales se puedan utilizar herramientas estándares del mercado (tanto sean ambientes Windows o Unix).

Continuar leyendo

VirtualCert

Abstract In this project we focus on the security of computer virtualization platforms. In particular, the main objective is to develop a formal idealized model of one such platform, establish non-interference security properties that should be guaranteed by the modeled control access mechanisms and to construct mathematical proofs, verified with the help of the Coq proof assistant, that those properties are verified by the model. The project has been partially funded by a grant Fondo Clemente Estable 2009 of the Uruguayan National research agency ANII and currently by a CSIC grant for R&D Projects - edition 2012.

Continuar leyendo