Fecha: Viernes 1º de agosto de 2014
Hora: 11:30
Lugar: Sala de Posgrados, Instituto de Computación, Facultad de Ingeniería
Título de la tesis: "Formal analysis of security models for mobile devices, virtualization platforms, and domain name systems" (Análisis formal de modelos de seguridad para dispositivos móviles, plataformas de virtualización y sistemas de nombres de dominio)
Director Académico y Director de Tesis: Dr. Gustavo Betarte (Instituto de Computación, Facultad de Ingeniería, UdelaR / PEDECIBA Informática)
Tribunal:
- Dra. Tamara Rezk (INRIA Sophia Antipolis-Mediterranée, France) - Revisora -
- Dr. Nazareno Aguirre (Departamento de Computación, Facultad de Ciencias Exactas, Físicoquímicas y Naturales, Universidad Nacional de Río Cuarto, Argentina) - Revisor -
- Dra. Ana Bove (Department of Computing Science and Engineering, Chalmers University of Technology, Sweden / PEDECIBA Informática)
- Dr. Álvaro Martín (Instituto de Computación, Facultad de Ingeniería, UdelaR / PEDECIBA Informática) - Presidente del Tribunal -
- Dr. Eduardo Grampín (Instituto de Computación, Facultad de Ingeniería, UdelaR / PEDECIBA Informática)
Abstract
In this thesis we investigate the security of security-critical applications, i.e. applications in which a failure may produce consequences that are unacceptable. We consider three areas: mobile devices, virtualization platforms, and domain name systems.The Java Micro Edition platform denes the Mobile Information Device Prole (MIDP) to facilitate the development of applications for mobile devices, like cell phones and PDAs. In this work we first study and compare formally several variants of the security model specified by MIDP to access sensitive resources of a mobile device.Hypervisors allow multiple guest operating systems to run on shared hardware, and off er a compelling means of improving the security and the flexibility of software systems. In this thesis we present a formalization of an idealized model of a hypervisor, and we establish (formally) that the hypervisor ensures strong isolation properties between the diff erent operating systems, and guarantees that requests from guest operating systems are eventually attended. We show also that virtualized platforms are transparent, i.e. a guest operating system cannot distinguish whether it executes alone or together with other guest operating systems on the platform.The Domain Name System Security Extensions (DNSSEC) is a suite of specifications that provides origin authentication and integrity assurance services for DNS data. We finally present a minimalistic specification of a DNSSEC model which provides the grounds needed to formally state and verify security properties concerning the chain of trust of the DNSSEC tree.We develop all our formalizations in the Calculus of Inductive Constructions --formal language that combines a higher-order logic and a richly-typed functional programming language-- using the Coq proof assistant.
Keywords: Formal modelling, Security properties, Coq proof assistant, JME-MIDP, Virtualization, DNSSEC.
Resumen
En esta tesis investigamos la seguridad de aplicaciones de seguridad críticas, es decir aplicaciones en las cuales una falla podría producir consecuencias inaceptables. Consideramos tres áreas: dispositivos móviles, plataformas de virtualización y sistemas de nombres de dominio.La plataforma Java Micro Edition define el Perfil para Dispositivos de Información Móviles (MIDP) para facilitar el desarrollo de aplicaciones para dispositivos móviles, como teléfonos celulares y asistentes digitales personales. En este trabajo primero estudiamos y comparamos formalmente diversas variantes del modelo de seguridad especificado por MIDP para acceder a recursos sensibles de un dispositivo móvil.Los hipervisores permiten que múltiples sistemas operativos se ejecuten en un hardware compartido y ofrecen un medio para establecer mejoras de seguridad y flexibilidad de sistemas de software. En esta tesis formalizamos un modelo de hipervisor y establecemos (formalmente) que el hipervisor asegura propiedades de aislamiento entre los diferentes sistemas operativos de la plataforma, y que las solicitudes de estos sistemas son atendidas siempre. Demostramos también que las plataformas virtualizadas son transparentes, es decir, que un sistema operativo no puede distinguir si ejecuta sólo en la plataforma o si lo hace junto con otros sistemas operativos.Las Extensiones de Seguridad para el Sistema de Nombres de Dominio (DNSSEC) constituyen un conjunto de especificaciones que proporcionan servicios de aseguramiento de autenticación e integridad de origen de datos DNS. Finalmente, presentamos una especificación minimalista de un modelo de DNSSEC que proporciona los fundamentos necesarios para formalmente establecer y verificar propiedades de seguridad relacionadas con la cadena de confianza del árbol de DNSSEC.Desarrollamos todas nuestras formalizaciones en el Cálculo de Construcciones Inductivas ---lenguaje formal que combina una lógica de orden superior y un lenguaje de programación funcional tipado--- utilizando el asistente de pruebas Coq.
Palabras clave: Modelos formales, Propiedades de seguridad, Asistente de pruebas Coq, JME-MIDP, Virtualización, DNSSEC.