La sécurisation de l'Internet du futur avec TLS 1.3 – SafeTLS

TLS/SSL (version actuelle TLS 1.2) est un des 3 principaux protocoles garantissant la sécurité des réseaux informatiques avec SSH et IPSec. Malgré son rôle central pour le e-commerce, la navigation Internet, les email, la VoIP et le fait que presque toutes les requêtes de connexion et de recherche dans les navigateurs l'utilisent, ce protocole présente toujours des failles de sécurité dans sa conception. Pour éviter les attaques récentes, comme FREAK, LogJam, 3Shake, SLOTH, ou DROWN, une nouvelle version, TLS 1.3, est en cours de définition. Notre projet, SafeTLS, s'intéresse, de 3 manières différentes, à la sécurité de TLS 1.3 et TLS 1.2 comme ils sont (seront) utilisés:

(1) en fournissant une meilleure compréhension des preuves de sécurité de la mise en accord de clé de TLS 1.3 et 1.2. Le premier aspect concernera la formalisation et les preuves de propriétés de privacy atteintes par la nouvelle version TLS 1.3; le second s'intéressera à la sécurité des canaux sécurisés contre les menaces de surveillance de masse, dans lesquelles un adversaire puissant, appelé Big Brother cherche à apprendre des informations en modifiant les implémentations. Un autre objectif de nos travaux s'intéresse à la dégradation de sécurité de TLS utilisés dans des infrastructures avec un intermédiaire. Ces infrastructures sont, notamment, très utilisées aujourd'hui pour accélérer les communications. Finalement, on souhaite estimer et fournir de nouvelles primitives pour TLS et D-TLS, en étudiant les candidats de la compétition CAESAR sur le chiffrement authentifié et les courbes elliptiques adaptées pour ces protocoles suite à la méfiance vis-à-vis des courbes proposées par le NIST.

(2) en fournissant aux clients un outil qui détecte la qualité de chaque connexion TLS en temps réel. En particulier, les explications données au client doivent être compréhensibles et aussi courtes que possible, transformant cet outil en aide pour une utilisation plus sûre de la navigation internet. Un autre aspect de notre travail concerne les infrastructures intermédiaires qui sont en fait utilisées dans les connexions pour accélérer celles-ci, mais qui diminuent la sécurité. On remarque que ces infrastructures réduisent les temps de latence pour le client et la bande passante pour les serveurs, mais elles représentent un risque supplémentaire qu'il est important de communiquer aux utilisateurs. En effet, elles se substituent au serveur que le client cherche à connecter.

(3) en s'intéressant au problème de la sécurité des implémentations de TLS. On veut proposer une analyse de sécurité des implémentations disponibles de TLS 1.2 comme s2n, BoringSSL, et mbedTLS. En utilisant des outils de vérifications automatiques comme EasyCrypt, on veut formaliser et prouver la sécurité de TLS 1.3 handshake avec tous les modes opératoires, et ensuite utiliser les outils qui transforment les preuves EasyCrypt en code certifié, ce qui fournira un exemple d'implémentation sûre de TLS 1.3. Enfin, étudier la sécurité des implémentations contre les attaques par canaux auxiliaires.

En résumé, nos résultats présenteront: (1) des preuves de sécurités (utilisant des techniques de méthodes formelles et de sécurité prouvée), donnant des bornes inférieures sur la sécurité; (2) des résultats d'impossibilité et des bornes supérieures sur la sécurité contre la surveillance de masse et la dégradation avec des infrastructures intermédiaires; (3) l'application conçue pour estimer la qualité des connexions TLS en temps réel, qui sera open-source et disponible à tous les utilisateurs; (4) un code certifié correspondant à une implémentation sécurisée de TLS 1.3.