Testing, Diagnosticabilidad y Verificación Formal de Seguridad y Funcionalidad en Implementaciones de Protocolos Criptográficos y Sistemas Distribuídos

En los últimos años, el mundo ha comenzado a utilizar más y más Internet para realizar tareas delicadas y complejas, como por ejemplo llevar a cabo transacciones electrónicas entre un vendedor y un comprador vía Internet. Sin lugar a dudas, el software encargado de llevar a cabo tal tarea, llamado protocolo criptográfico, debe ser completamente confiable y seguro. En este proyecto desarrollaremos métodos formales para verificar automáticamente protocolos criptográficos. En particular, se estudiara el análisis de protocolos de seguridad por medio de técnicas de model-checking en modelos de seguridad simbólicos con análisis automático utilizando herramientas dedicadas en modelos computacionales y luego se estudiaran metodologías de derivación automática de tests con el objetivo de testear implementaciones reales de dichos protocolos. Finalmente estudiaremos el análisis de protocolos de seguridad probabilísticos, como ser protocolos de voto electrónico y ruteo anónimo. Implementaremos una herramienta prototipo con dichos métodos formales que utilizaremos para evaluar nuestras técnicas. Mas concretamente, evaluaremos:

  1. La aplicación de nuestra herramienta en implementaciones de protocolos criptográficos de amplio uso, como ser el protocolo Transport Layer Security (TLS), utilizado en navegadores de internet para asegurar la comunicación.
  2. La aplicación de nuestra herramienta en protocolos propuestos pero aún no ampliamente utilizados, como ser el protocolo DNSSEC propuesto para asegurar las comunicaciones en servidores de nombre estandar DNS. Al utilizar nuestra herramienta podremos verificar e identificar problemas en forma temprana.
  3. La aplicación de nuestra herramienta para evaluar la diagnosticabilidad acotada de sistemas así también como en sistemas distribuidos con diferentes tipos de sincronización y de sistemas probabilísticos.
  4. Evaluaremos nuevas técnicas de testing para poder verificar que una implementación de cierto protocolo criptográfico se corresponde con su especificación formal. En este caso, podremos verificar la correspondencia de implementaciones actuales en forma de caja negra (por ejemplo, implementaciones de TLS como ser OpenSSL o Apache) con su modelo formal.
  5. Estudiaremos el análisis de protocolos de seguridad probabilísticos como ser el protocolo Crowds y Tor para ruteo anónimo.

Participantes

Ricardo Corin (Director)
Laura Brandán Briones (Co-directora)
Powered by Drupal