From Specs to Apps: Verifying and Monitoring Models of Signal and WhatsApp
Este artículo cierra la brecha entre las especificaciones formales de los protocolos y las implementaciones del mundo real mediante el uso del monitor de tiempo de ejecución SpecMon para verificar que las ejecuciones observadas de WhatsApp Web y Signal Desktop se ajustan a modelos compatibles con Tamarin recientemente desarrollados, confirmando así las propiedades de seguridad y descubriendo diferencias no documentadas entre las aplicaciones.
Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo
En la era digital, miles de millones de personas dependen de las aplicaciones de mensajería para compartir sus pensamientos más privados, asegurar sus datos financieros y coordinar su vida diaria. Detrás de escena de estas aplicaciones se encuentra un conjunto complejo de reglas conocido como protocolo, que actúa como el plano de cómo los mensajes se bloquean, se envían y se desbloquean. El más famoso de estos planos es el protocolo Signal, un sistema diseñado para asegurar que incluso si un hacker intercepta un mensaje, no pueda leerlo. Durante años, los expertos en seguridad han utilizado poderosas herramientas informáticas para demostrar que este plano es matemáticamente sólido. Han demostrado que, si se siguen las reglas perfectamente, el sistema es inquebrantable. Sin embargo, un plano no es lo mismo que un edificio. El hecho de que un diseño parezca perfecto en papel no significa que el equipo de construcción haya seguido cada instrucción, utilizado los materiales adecuados o evitado errores accidentales al construir las paredes. En el mundo del software, la brecha entre el diseño teórico y el código real que se ejecuta en el teléfono de un usuario es donde suelen esconderse las vulnerabilidades.
Un equipo de investigadores del Centro CISPA Helmholtz para la Seguridad de la Información se propuso cerrar esta brecha. Querían saber si las versiones del mundo real del protocolo Signal, tal como se ejecutan dentro de las aplicaciones WhatsApp y Signal, realmente siguen las estrictas reglas que fueron diseñadas para obedecer. En lugar de intentar leer todo el código fuente de estas aplicaciones masivas —una tarea dificultada porque partes de ellas están ocultas o cerradas—, los investigadores construyeron un vigilante especializado. Este vigilante, llamado SpecMon, observa la aplicación mientras se ejecuta, escuchando cada conversación que tiene con la red y cada cálculo que realiza con sus claves de seguridad. Compara estas acciones en vivo contra el modelo teórico perfecto en tiempo real. Si la aplicación intenta tomar un atajo, saltarse un paso o utilizar un método diferente al permitido por el plano, el vigilante lanza una alarma.
Los investigadores aplicaron este método a dos aplicaciones importantes: Signal Desktop, que es abierta para que cualquiera la inspeccione, y WhatsApp Web, que es un sistema cerrado y propietario perteneciente a una enorme corporación. Para la aplicación Signal Desktop, partieron de un modelo matemático existente y altamente detallado del protocolo y añadieron los detalles específicos y desordenados que se encuentran en el software real, como la forma en que maneja nuevos tipos de cifrado diseñados para resistir futuras computadoras cuánticas. Para WhatsApp, tuvieron que trabajar hacia atrás. Partiendo de ningún modelo previo, observaron el comportamiento de la aplicación, registraron sus acciones y construyeron un nuevo plano personalizado desde cero que coincidiera exactamente con lo que el software estaba haciendo. Este fue un logro significativo, ya que marcó la primera vez que se derivó un modelo formal directamente de la implementación de la versión de WhatsApp de dicho protocolo.
Una vez que estos modelos estuvieron listos, los investigadores los pusieron a prueba. Ejecutaron miles de conversaciones simuladas, incluyendo escenarios donde los mensajes se retrasaban, se enviaban fuera de orden o donde la conexión de red se interrumpía. En cada caso, las aplicaciones se comportaron exactamente como los modelos predecían, confirmando que los mecanismos centrales de seguridad funcionaban correctamente. Los investigadores también inyectaron errores deliberadamente en el software para ver si su vigilante los detectaría. Hicieron que las aplicaciones reutilizaran claves de cifrado antiguas, se saltaran verificaciones de firma o filtraran datos secretos de formas inesperadas. El sistema detectó cada uno de estos fallos de seguridad, demostrando que la herramienta de monitoreo es lo suficientemente sensible como para detectar desviaciones peligrosas de las reglas.
Sin embargo, el monitoreo también reveló diferencias sutiles entre las dos aplicaciones que no eran inmediatamente obvias. Los investigadores encontraron que WhatsApp maneja los "recibos de lectura" —las notificaciones que indican al remitente que un mensaje ha sido visto— de manera diferente a como lo hace Signal. En Signal, estos recibos están envueltos en el mismo cifrado fuerte que los mensajes y participan en la actualización continua de las claves de seguridad. En WhatsApp, estos recibos se envían fuera de esa capa cifrada, lo que significa que no activan las mismas actualizaciones de seguridad. Aunque los investigadores no encontraron una forma de romper la seguridad de WhatsApp basándose en esta diferencia, señalaron que esto significa que la aplicación podría tardar más en recuperar su seguridad si una clave secreta fuera robada alguna vez. También confirmaron que WhatsApp aún no incluye ciertas funciones avanzadas de privacidad, como ocultar la identidad del remitente al servidor, que sí están presentes en la aplicación Signal.
El estudio demuestra que es posible observar software complejo del mundo real en acción y verificar que cumple con sus promesas de seguridad sin necesidad de ver cada línea de su código fuente. El proceso fue eficiente, tomando solo unas pocas semanas para configurarse y ejecutarse, y añadió muy poco retraso a la velocidad de las aplicaciones. Al crear un sistema donde el modelo teórico y el monitoreo en vivo comparten el mismo lenguaje, los investigadores han proporcionado una forma para que los desarrolladores y expertos en seguridad comprueben continuamente que sus aplicaciones se mantienen seguras a medida que evolucionan. Este enfoque ofrece un nuevo camino para construir confianza en las herramientas digitales que usamos todos los días, asegurando que los edificios en los que vivimos sean tan seguros como los planos con los que fueron construidos.
¿Ahogado en artículos de tu campo?
Recibe resúmenes diarios de los artículos más novedosos que coincidan con tus palabras clave de investigación — con resúmenes técnicos, en tu idioma.