Departamento Ciencias de la Computación - FCEIA-ECEN-DCC

URI permanente para esta comunidad

https://rephip.unr.edu.ar/handle/2133/1817

Examinar

Examinando Departamento Ciencias de la Computación - FCEIA-ECEN-DCC por Materia "Android"

Mostrando 1 - 2 de 2
  • Miniatura
    ÍtemAcceso 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.
  • Miniatura
    ÍtemAcceso Abierto
    Formalización del protocolo de comunicación entre aplicaciones para dispositivos móviles Java
    (Facultad de Ciencias Exactas, Ingeniería y Agrimensura. Universidad Nacional de Rosario, 2013-10-25) Forte, José Armando; Luna, Carlos Daniel; Chimento, Mauricio
    En los últimos años se ha incrementado de manera significativa el uso de dispositivos móviles, tales como teléfonos celulares y smartphones. Este rápido crecimiento ha provocado que los usuarios integren el uso de aplicaciones en su rutina diaria. A su vez, este fenómeno ha generado grandes cambios a la hora de considerar la seguridad e integridad de la información que éstos manejan. En la Plataforma Java Micro Edition, el Perfil para Dispositivos de Información Móviles (MIDP) provee el ambiente de ejecución estándar para teléfonos móviles y asistentes de datos personales. La tercera y más reciente versión del perfil introduce, en particular, una nueva dimensión en el modelo de seguridad de MIDP: la seguridad a nivel de aplicación. En esta nueva versión las MIDlets que quieren compartir datos entre ellas utilizan un protocolo de comunicación denominado InterMIDlet Communication (IMC). El presente trabajo analiza formalmente el nuevo modelo de seguridad y formaliza este nuevo protocolo. Concretamente, el trabajo extiende una especificación formal desarrollada en el Cálculo de Construcciones Inductivas, usando el asistente de pruebas Coq. Se formalizan los eventos relacionados con el protocolo mencionado anteriormente, se demuestra que la extensión es conservativa y se analizan propiedades relevantes de seguridad relativas a la extensión. Finalmente, se refina la especificación junto con la extensión propuesta y se certifican en Coq dos algoritmos como implementaciones de los nuevos eventos.