Formal analysis of security models for mobile devices, virtualization platforms, and domain name systems
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.
Razonando sobre la seguridad de Android
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. Es por ello 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. Este trabajo propone realizar un análisis formal exhaustivo del modelo de seguridad instrumentado por Android, considerando especificaciones e implementaciones existentes, y teniendo en cuenta trabajos previos en el área.
Especificación e implementación de un prototipo certificado del sistema de permisos de Android
La vasta cantidad de dispositivos móviles ejecutando Android y las facilidades de distribución de software de terceros que ofrece hacen de este sistema operativo un objetivo tentador para ciberdelincuentes, cuyas acciones tienen el potencial de afectar a miles de millones de personas. Esta situación ha puesto a Android bajo la lupa de los investigadores, quienes pretenden poner a prueba la robustez de su sistema de seguridad y minimizar los vectores de ataque. En este trabajo se extiende un modelo preexistente del sistema de seguridad de Android para considerar los cambios introducidos en su versión 6.0 y especificar el comportamiento del sistema frente a la ejecución de operaciones erróneas. También se presenta un programa que implementa tal modelo y se demuestra formalmente su corrección. Además se postulan y demuestran propiedades de seguridad sobre el modelo y el código ejecutable referidos. Finalmente se explica la manera en que la implementación certificada puede utilizarse a modo de oráculo de referencia para verificar la corrección de una plataforma real, y cómo permitiría la posterior programación de un monitor de seguridad capaz de supervisar una plataforma en tiempo real.
Enhancing web application attack detection using machine learning
A pesar de todos los esfuerzos de la comunidad de seguridad, por ejemplo, ini- ciativas como el OWASP Top 10, es un hecho conocido que las aplicaciones web están permanentemente expuestas a ataques que explotan sus vulnerabilidades. Algunas de estas vulnerabilidades solo se pueden descubrir como resultado de un proceso de ensayo y error realizado por un atacante. La identificación y determinación del com- portamiento de un usuario utilizando técnicas de detección de ataques se vuelven cruciales. Estas técnicas ayudan en aspectos tales como evitar que los atacantes iden- tifiquen/verifiquen con éxito la existencia de vulnerabilidades en las aplicaciones, así como minimizar el número de falsos positivos (actividad no maliciosa identi- ficada como tal). Una alternativa tecnológica para realizar análisis de ataques en tiempo real es el uso de un firewall de aplicaciones web (WAF por su siglas en in- glés). Estos sistemas interceptan e inspeccionan el tráfico entre el servidor web y sus clientes, buscando ataques en el contenido de la comunicación. La mayoría de los WAF funcionan mediante el uso de un conjunto de reglas estáticas definidas para identificar ataques.
Offloading de servicios criptográficos hacia la tarjeta SIM en smartphones
Los smartphones están omnipresentes en la vida cotidiana de las personas como herramientas de comunicación, entretenimiento y trabajo. Las pantallas táctiles y una variedad de sensores ofrecen una experiencia superior y hacen que las aplicaciones sean cada vez más diversas, complejas y demanden más recursos. A pesar de su continua evolución y mejoras, los dispositivos móviles aún están limitados en duración de batería, poder de procesamiento, capacidad de almacenamiento y ancho de banda de red. Computation offloading se destaca entre los esfuerzos para ampliar las capacidades del dispositivo y combatir la creciente brecha entre demanda y disponibilidad de recursos. Como toda tecnología popular, los smartphones son blancos atractivos para atacantes maliciosos. Generalmente almacenan datos privados y se utilizan cada vez más para actividades sensibles como banca en línea o pagos móviles. Si bien computation offloading presenta nuevos desafíos al proteger esos activos, es muy poco común tomar seguridad y privacidad como los principales objetivos de optimización de dicha técnica. La seguridad del SO móvil depende fuertemente de la criptografía. Los servicios criptográficos por hardware y software disponibles suelen estar diseñados para resistir ataques de software, protección insuficiente cuando se pierde el control físico sobre el dispositivo. Los elementos seguros, en cambio, incluyen un conjunto de protecciones que los hacen físicamente resistentes a la manipulación. Este trabajo propone una técnica de computation offloading que prioriza mejorar las capacidades de seguridad de los teléfonos móviles descargando operaciones criptográficas a la SIM, único elemento seguro universalmente presente en los mismos. Nuestras contribuciones incluyen una arquitectura para esta técnica, un prototipo de prueba de concepto desarrollado bajo Android y los resultados de una evaluación de desempeño que estudia tiempos de ejecución y consumo de batería. A pesar de algunas limitaciones, nuestro enfoque demuestra ser una alternativa válida para mejorar la seguridad en cualquier smartphone.
Constructing privacy aware blockchain solutions: Design guidelines and threat analysis techniques
Blockchain es una tecnología incipiente que ofrece muchas fortalezas en comparación con los sistemas tradicionales, como la descentralización, la transparencia y la trazabilidad. Sin embargo, si se va a utilizar esta tecnología para el procesamiento de datos personales, se deben identificar mecanismos complementarios que brinden soporte a los sistemas de construcción que cumplan con los requisitos de seguridad y protección de datos. En este trabajo estudiamos la integración de capacidades de soluciones offchain en soluciones basadas en blockchain, moviendo datos u operaciones computacionales fuera de blockchain. Adicionalmente, desarrollamos un análisis exhaustivo del reglamento europeo y uruguayo de protección de datos personales y discutimos las debilidades y fortalezas, en cuanto a los requisitos de seguridad y privacidad que establece dicho reglamento, de las soluciones construidas con tecnología blockchain. En base a este análisis, presentamos un marco metodológico para el diseño de soluciones basadas en tecnología blockchain, pensando en la privacidad. También presentamos un enfoque sistemático para realizar un análisis de amenazas a la seguridad y la privacidad de este tipo de soluciones. Finalmente, ilustramos el uso de las herramientas metodológicas propuestas, presentando y discutiendo tanto el diseño como la evaluación de seguridad y privacidad de un sistema que brinda servicios para manejar, almacenar y validar certificados académicos digitales.
Web Application Attacks Detection Using Deep Learning
En esta tesis se explora el uso de técnicas de aprendizaje profundo para mejorar el rendimiento de Web Application Firewalls (WAFs por su siglas en ingl ́és). Dichos sistemas son utilizados para detectar y prevenir ataques a aplicaciones web. Normalmente un WAF inspecciona las solicitudes del Protocolo de Transferencia de Hipertexto (HTTP) que se intercambian entre el cliente y el servidor, con el objetivo de detectar ataques y bloquear potenciales amenazas. En el enfoque que se propone, modelamos el problema como un caso supervisado de una clase y construimos un extractor de características (features) utilizando una técnica de aprendizaje profundo. Concretamente, tratamos las solicitudes HTTP como texto y entrenamos un modelo de lenguaje profundo con una arquitectura basada en un tipo de redes neuronales que se denominan Transformers. El uso de modelos de lenguaje previamente entrenados ha producido mejoras significativas en un conjunto diverso de tareas de Procesamiento de Lenguaje Natural (PLN) porque son capaces de realizar aprendizaje por transferencia. En nuestro enfoque utilizamos el modelo previamente entrenado como un extractor de características para mapear las solicitudes HTTP en vectores numéricos. Luego, estos vectores se utilizan para entrenar un clasificador de una clase. También utilizamos una métrica de evaluación establecida para definir un punto operativo (de forma automática) para el modelo de una clase. Los resultados experimentales muestran que el enfoque propuesto supera a aquellos obtenidos con ModSecurity, un WAF ampliamente utilizado. La capacidad de detección de ataques de ModSecurity depende fuertemente de la aplicación de reglas configuradas con el Core Rule Set (CRS) de OWASP, el conjunto de reglas más ampliamente utilizadas para la prevención de ataques a aplicaciones Web. Una de las principales ventajas de nuestro enfoque es que no se requiere la participación de un experto en seguridad para el proceso de extracción de características.
A Formal Analysis of the Mimblewimble Cryptocurrency Protocol with a Security Approach
Una criptomoneda es una moneda digital que puede ser intercambiada por bienes y servicios. Las criptomonedas utilizan cadena de bloques (blockchains) públicas donde las transacciones se encuentran duplicadas y distribuidas en los nodos de una red de computadoras. Este mecanismo descentralizado es concebido para lograr confiabilidad en una red compuesta por nodos no fiables. La privacidad, el anonimato y la seguridad se han vuelto cruciales en este contexto. Por esta razón, los enfoques formales y matemáticos han ganado popularidad con el fin de garantizar la corrección de las implementaciones. Mimblewimble es una criptomoneda orientada a la privacidad con propiedades de seguridad y escalabilidad que la distingue de otras criptomonedas. En agosto de 2016, un usuario anónimo, bajo el seudónimo de Tom Elvis Jedusor (nombre en francés de Voldemort en la saga de Harry Potter), publicó un archivo de texto en el canal de chat IRC donde explicaba las bases de este nuevo protocolo. Mimblewimble está basado en Criptografía de Curvas Elípticas lo que permite verificar la validez de las transacciones sin revelar información alguna sobre el monto y las partes involucradas. Mimblewimble combina transacciones confidenciales y las técnicas de CoinJoin y cut-through para alcanzar mayor nivel de privacidad, seguridad y escalabilidad. En esta tesis, presentamos y discutimos estas propiedades de seguridad y describimos un enfoque basado en la verificación de modelos para alcanzar la certificación de la corrección de las implementaciones del protocolo. En particular, proponemos un modelo idealizado que es clave en el proceso de verificación descrito. Los principales componentes de nuestro modelo idealizado son las transacciones, los bloques y la cadena. Luego, identificamos y describimos precisamente las condiciones que nuestro modelo debe cumplir para asegurar la verificaciones de propiedades de seguridad relevantes de Mimblewimble. Además, analizamos el estado actual de sus dos más importantes implementaciones, Grin y Beam. Finalmente, presentamos conexiones detalladas entre nuestro modelo y las implementaciones en relación a la estructura de Mimblewimble y sus propiedades de seguridad.
Detection and classification of privacy leaks enabled by third-party trackers in COVID-19 mobile applications
SDesde 2019, el mundo ha vivido una pandemia sin precedentes en nuestra actual era tecnológica. Los gobiernos y otras organizaciones de alto perfil dedicaron esfuerzos especiales a desarrollar y patrocinar aplicaciones móviles que, si bien variaban en sus objetivos, intentaban ayudar a contener la propagación de COVID-19 y permitir que las personas tuvieran la mejor calidad de vida posible. Sin embargo, si bien las bibliotecas de terceros y su impacto en la privacidad del usuario ya se han estudiado anteriormente, especialmente las consideradas rastreadores, estas han encontrado su camino en aplicaciones COVID-19 respaldadas por organizaciones de alto perfil. Por rastreadores consideramos bibliotecas de terceros incluidas en aplicaciones para ofrecer ciertas funcionalidades que, además, recopilan información sobre la aplicación, el dispositivo y su uso, y la envían a sus servidores. La investigación para esta tesis encontró que 402 de las 595 aplicaciones estudiadas contenían al menos un rastreador. Además, se confirmó que se transfirió información sensible a los servidores de los rastreadores, lo que potencialmente revela el estado de salud de los usuarios de la aplicación. Por otro lado, la evidencia indica que los gobiernos pueden mejorar sus evaluaciones de impacto de protección de datos y la divulgación que hacen en sus políticas de privacidad; esto último también aplica a los rastreadores. Finalmente, se presenta SAPITO, una herramienta de código abierto fácil de usar. Basada en el conocimiento y las lecciones aprendidas durante esta investigación, fue creada con el objetivo de ayudar a los equipos de privacidad e investigadores a detectar automáticamente fugas de datos al analizar bibliotecas de terceros en aplicaciones Android.