CIRCUS: Analyser et Sécuriser des Programmes Rust
En collectant, stockant, et échangeant des données personnelles et sensibles sur Internet, tous les logiciels modernes sont critiques en matière de sécurité. Pour éviter de multiples vulnérabilités, un nombre croissant d’entreprises et d’agences gouvernementales préconisent l’utilisation de langages « safe », particulièrement le langage Rust. Cependant, le développement d’un projet en Rust ne suffit pas à atteindre les garanties nécessaires pour du logiciel critique: des attaques par déni de service dûes à des erreurs (panic) lors de l’exécution, des fonctionnalités implémentées incorrectement, voire des fautes dans la conception d’un système restent possibles.
Pour sortir de l’impasse, le projet CIRCUS préconise l’utilisation de vérification formelle, afin d’obtenir des preuves de sécurité et de correction vérifiées par des machines. Issu d’une collaboration entre l’équipe Prosecco d’Inria Paris et l’entreprise Cryspen, CIRCUS développe de nouveaux outils pour simplifier l’application de vérification formelle au langage Rust, et les applique particulièrement dans le cadre d’applications cryptographiques telles que le protocole TLS, largement utilisé pour sécuriser les communications Internet (HTTPS). Dans cette présentation, nous présenterons les bénéfices de la vérification formelle, différents outils développés dans le cadre de CIRCUS, ainsi que leur application à Bertie, une réimplémentation minimale de TLS, avec des preuves formelles de sécurité et de correction fonctionnelle.
Lien pour assister en visio
