La seguridad web depende mayoritariamente del protocolo HTTPS. A pesar de la «S» para la seguridad en «HTTPS», este protocolo está lejos de ser perfectamente seguro aunque casi la mitad de todo el tráfico web pasa a través de él.
En un documento presentado en el USENIX Security Symposium en Vancouver, Bryan Parno, profesor asociado de Ciencias de la Computación y Ingeniería Eléctrica e Informática, y un equipo de investigadores demostraron una nueva herramienta de programación llamada «Vale: Verifiying High-Performance Cryptographic Asembly Code» que permite que el código criptográfico de alto rendimiento sea verificable y seguro.
El equipo demostró su enfoque de verificación en varios componentes criptográficos del ecosistema HTTPS.
El ecosistema HTTPS ha visto una larga y algo deprimente serie de errores, según Parno, con un ciclo continuo: error, pánico, arreglo. Error, pánico, arreglo. El problema según este experto es que el software de hoy viene con pocas, o ninguna, garantía de seguridad. Tradicionalmente, los vendedores toman conciencia de las vulnerabilidades después de que ocurre un ataque, y luego emiten un parche que corrige ese ataque en particular.
Código verificado y rápido
La herramienta “Vale” fue una de las primeras demostraciones de código verificado que se está ejecutando tan rápido, o más rápido, que el código no verificado. Por verificado quieren decir que en realidad tiene una prueba matemática formal de que todo el código que compone estos componentes HTTPS realmente cumple con algunas especificaciones de seguridad de alto nivel.
Una de las principales razones por las que los sitios web han sido resistentes al uso de código verificado en HTTPS es que, hasta ahora, la mayoría del código verificado se ha comportado significativamente más lento que el código no verificado. Las transferencias de datos más lentas entre el sitio web y el usuario se traducen en una experiencia de menor calidad.
Además de demostrar que los componentes criptográficos eran correctos, el equipo demostró el éxito de su sistema de verificación para demostrar resistencia a dos de los tipos más populares de ataques de canal lateral: los ataques de tiempo, en el que un adversario utiliza el tiempo de espera entre solicitar y recibir para deducir información sobre la clave de cifrado y los ataques de acceso a la memoria en los que un adversario supervisa los accesos de memoria de una víctima en un entorno de cómputo compartido para deducir una clave de cifrado.
Fuente: Carnegie Mellon University
