Please use this identifier to cite or link to this item:
https://hdl.handle.net/20.500.12008/2909
How to cite
Title: | Formal analysis of security models for mobile devices, virtualization platforms and domain name systems |
Authors: | Luna, Carlos |
Obtained title: | Doctor en Informática |
University or service that grants the title: | Universidad de la República (Uruguay). Facultad de Ingeniería. Instituto de Computación – PEDECIBA |
Tutor: | Betarte, Gustavo |
Type: | Tesis de doctorado |
Keywords: | Modelos formales, Prioridades de seguridad, Asistente de pruebas Coq, JME-MIDP, Virtualización, DNSSEC |
Issue Date: | 2014 |
Abstract: | En esta tesis investigamos la seguridad de aplicaciones de seguridad criticas, es decir aplicaciones en las cuales una falla podria producir consecuencias inaceptables. Consideramos tres areas: dispositivos moviles, plataformas de virtualizacion y sistemas de nombres de dominio. La plataforma Java Micro Edition define el Perfil para Dispositivos de Informacion Moviles (MIDP) para facilitar el desarrollo de aplicaciones para dispositivos moviles, como telefonos 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 movil. Los hipervisores permiten que multiples 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 tambien que las plataformas virtualizadas son transparentes, es decir, que un sistema operativo no puede distinguir si ejecuta solo 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 autenticacion e integridad de origen de datos DNS. Finalmente, presentamos una especificaci´on 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 arbol de DNSSEC. Desarrollamos todas nuestras formalizaciones en el C´alculo de Construccione |
Publisher: | UR. FI-INCO, |
Citation: | LUNA, C. "Formal analysis of security models for mobile devices, virtualization platforms and domain name systems". Tesis de doctorado, Universidad de la República (Uruguay). Facultad de Ingeniería. Instituto de Computación – PEDECIBA, 2014. |
License: | Licencia Creative Commons Atribución – No Comercial – Sin Derivadas (CC BY-NC-ND 4.0) |
Appears in Collections: | Tesis de posgrado - Instituto de Computación |
Files in This Item:
File | Description | Size | Format | ||
---|---|---|---|---|---|
tesisd-luna.pdf | 932,93 kB | Adobe PDF | View/Open |
This item is licensed under a Creative Commons License