Formalización

En los últimos años se ha observado un marcado incremento en el número de dispositivos móviles que tienen a Android como sistema operativo. Por este motivo, una falla en la seguridad de dicha plataforma afectaría a una gran cantidad de usuarios de distintas formas, por ejemplo, dejando expuesta información sensible guardada en el dispositivo. Este elevado número de víctimas potenciales alientan a los creadores de aplicaciones maliciosas a elegir a Android como objetivo de sus ataques.

Continuar leyendo

Hacia la especificación y verificación formal de algoritmos criptográficos: Mini-AES certificado

en grado

May 5, 2017

El algoritmo de encriptación de información AES (Advanced Encryption Standard) es un estándar internacional ampliamente utilizado tanto por gobiernos como comercialmente; por lo tanto resulta de importancia crítica garantizar el correcto comportamiento de sus distintas implementaciones. Existe una versión simplificada del algoritmo, llamada Mini-AES, que fue creada con fines académicos, pero sin perder la esencia de su funcionamiento y sus propiedades criptográficas. En este trabajo se define un lenguaje de programación imperativa, se implementa Mini-AES sobre el mismo, y se demuestra formalmente que su comportamiento es el deseado, esto es, que los procedimientos de encriptar y desencriptar son inversos.

Continuar leyendo

Formally verified countermeasures against cache based attacks in virtualization platforms

en investigacion

May 5, 2017

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

Prueba formal de algoritmos de firma digital y sus implementaciones usando asistentes de pruebas

en grado

May 5, 2017

La criptografía juega un papel fundamental en el desarrollo de software seguro. Sin embargo, la tarea de diseñar primitivas criptográficas correctas y forzar su correcto uso en la práctica ha sido una tarea extremadamente difícil. La historia de la criptografía está llena de ejemplos de primitivas y protocolos inseguros de amplio uso general. Varios formalismos se han presentado en la literatura para probar con lápiz y papel la correctitud de primitivas criptográficas.

Continuar leyendo

Especificacion y verificacion formal de modelos de virtualizacion

en grado

May 5, 2017

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

VirtualCert

en investigación

April 4, 2017

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

Razonando sobre la seguridad de Android

Hacia la especificación y verificación formal de algoritmos criptográficos: Mini-AES certificado

Formally verified countermeasures against cache based attacks in virtualization platforms

Prueba formal de algoritmos de firma digital y sus implementaciones usando asistentes de pruebas

Especificacion y verificacion formal de modelos de virtualizacion

VirtualCert

Buscar

Categorias

Palabras clave