Examinando por Autor "Luna, Carlos D."
Mostrando 1 - 4 de 4
Resultados por página
Opciones de ordenación
Ítem Acceso Abierto Análisis de modelos de memoria en plataformas de virtualización. Formalización de un prototipo funcional de plataforma con Cache y Tlb(Facultad de Ciencias Exactas, Ingeniería y Agrimensura. Universidad Nacional de Rosario, 2012-04-13) Chimento, Jesús Mauricio M.; Luna, Carlos D.La virtualización es una técnica que se utiliza para correr múltiples sistemas operativos en una sola máquina física, pero creando la ilusión de que en realidad cada uno de estos sistemas operativos corre dentro de una Máquina Virtual diferente. El Monitor de Máquinas Virtuales es el encargado de administrar los recursos compartidos por los sistemas operativos que corren en las Maquinas Virtuales de manera que todos se puedan ejecutar adecuadamente. En particular, el acceso y uso de la Memoria Principal (i.e. Memoria RAM) es un aspecto crítico que el Monitor de Máquinas Virtuales debe controlar. En este trabajo se presenta un modelo formal idealizado de un Monitor de Máquinas Virtuales, sobre el cual se demuestran propiedades que garantizan el uso correcto de las acciones provistas por dicho Monitor a los distintos sistemas operativos virtualizados y el correcto acceso y uso de la Memoria Principal por parte de estos sistemas operativos. Además, se utiliza el asistente de pruebas de Coq para las demostraciones y posterior extracción de una versión ejecutable del modelo.Ítem Acceso Abierto Descripción y Análisis Formal del Modelo de Seguridad de Android(Facultad de Ciencias Exactas, Ingeniería y Agrimensura. Universidad Nacional de Rosario, 2014-08-22) Romano, Agustín Vicente; Luna, Carlos D.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 lo que una falla en la seguridad de dicha plataforma afectaría una gran cantidad de usuarios. Este elevado número de víctimas potenciales alienta a los creadores de aplicaciones maliciosas a elegir a Android como objetivo de sus ataques. Es por esto que el análisis y fortalecimiento de su modelo de seguridad se ha convertido en una tarea importante que despierta el interés de numerosos investigadores. El objetivo de este trabajo es realizar un análisis exhaustivo del modelo de seguridad implementado por Android. Para ello se realiza un estado del arte en el tema, considerando los trabajos más relevantes hasta el momento, y se compara dicho modelo con el implementado en los dispositivos móviles Java (JME-MIDP). Asimismo, se presenta una especificación formal que comprende distintos aspectos sobre la seguridad en Android, poniendo atención, principalmente, en el mecanismo de delegación de permisos y en la interacción con el framework de aplicaciones para realizar llamadas al sistema. Dicha especificación está desarrollada con el asistente de pruebas Coq, que es utilizado para demostrar formalmente diferentes propiedades sobre el modelo de seguridad representado.Ítem Acceso Abierto Especificación Formal del Modelo DNSSEC en el Cálculo de Construcciones Inductivas(Facultad de Ciencias Exactas, Ingeniería y Agrimensura. Universidad Nacional de Rosario, 2011-09-29) Bazán, Ezequiel; Luna, Carlos D.Con el crecimiento de aplicaciones desarrolladas en base al uso de nombres de dominio, la autenticidad en los datos dentro de DNS (Domain Name System) se ha tornado crítica, haciendo que información falsa dentro del sistema pueda llevar a problemas inesperados y potencialmente peligrosos. Para proveer extensiones de seguridad al protocolo DNS, la IETF (Internet Engineer Task Force) desarroll o DNSSEC (DNS SECurity Extensions). El presente trabajo provee una especificación formal de DNSSEC, utilizando el Cálculo de Construcciones Inductivas (CCI) y COQ como asistente de pruebas. El enfoque propuesto aborda principalmente el análisis de integridad de la cadena de confianza que se genera a lo largo del árbol DNSSEC, así como también la posibilidad de que se produzca algún tipo de contaminación de caché por suplantación de datos. La formalización en el CCI permitió realizar un análisis riguroso de la especificación propuesta. Se logró demostrar que la semántica de los comandos que se ejecutan dentro del sistema conservan invariante la validez del estado, lo cual garantiza que el sistema no puede transicionar a un estado que no represente un posible estado DNSSEC. Sin embargo, también pudo detectarse una inconsistencia en los datos dentro de la cadena de confianza al ejecutarse el rollover de una llave de zona, ya que puede suceder el caso en que los datos almacenados en el caché de un servidor discrepen de los datos verdaderamente publicados.Ítem Acceso Abierto Un Framework para el Análisis Formal de Modelos de Control de Acceso para Dispositivos Móviles Interactivos(Facultad de Ciencias Exactas, Ingenieria y Agrimensura. Universidad Nacional de Rosario, 2009-04) Crespo, Juan Manuel; Luna, Carlos D.; Betarte, GustavoLos dispositivos portátiles tales como teléfonos celulares y asistentes personales de datos, permiten almacenar información confidencial y establecer comunicaciones con entidades externas. Generalmente, los usuarios pueden descargar e instalar nuevas aplicaciones de fuentes no confiables, que conviven junto con las instaladas por el fabricante del dispositivo o proveedor de servicios de comunicación. Ante este escenario, es importante garantizar la confidencialidad e integridad de los datos almacenados, así como la disponibilidad del servicio, aún cuando una aplicación maliciosa trate de hacer uso indebido de las funciones del dispositivo. La plataforma Java Micro Edition (JME), una tecnología para desarrollo de software Java, provee el estándar Mobile Information Device Profile (MIDP) que facilita el desarrollo de aplicaciones y especifica un modelo de seguridad para el acceso controlado a recursos sensibles del dispositivo. El modelo está construido sobre la noción de dominio de protección, que puede ser concebido como un conjunto de permisos. Un modelo alternativo ha sido propuesto, que extiende los permisos presentes en MIDP, introduciendo la noción de multiplicidad, y flexibilizando la forma en la que el usuario puede conceder a las aplicaciones que son utilizadas en el dispositivo, accesos a los recursos del mismo. Esta tesina presenta un framework, formalizado utilizando el asistente de pruebas Coq, adecuado para la definición y comparación formal de políticas de control de acceso que pueden ser aplicadas por variantes de esos modelos de seguridad y para el análisis y prueba de propiedades de seguridad que éstas satisfacen. Las pruebas de algunas de estas propiedades son dadas y discutidas en el trabajo. Además, se provee una generalización que abstrae el concepto de modelo de control de accesos y se define un concepto de generalidad que permite compararlos formalmente.