La société Amazon et l'organisation Rust Foundation ont présenté une initiative visant à améliorer la sécurité de la bibliothèque standard du langage Rust. L'objectif déclaré est de vérifier la fiabilité et la sécurité des fonctionnalités utilisant le mot-clé « unsafe », qui permet des opérations potentiellement dangereuses sur la mémoire, telles que la déréférencement de pointeurs, la modification de variables statiques et l'accès à des bibliothèques externes en C/C++. Il est noté que la bibliothèque standard de Rust compte actuellement environ 35 000 fonctions, dont 7 500 contiennent des blocs de code exécutés dans un contexte « unsafe ». Au cours des trois dernières années, 57 problèmes de fonctionnement ont été identifiés dans la bibliothèque, dont 20 ont été classés comme vulnérabilités.
Le travail de vérification de la bibliothèque est organisé sous la forme d'un concours, dans lequel les participants se voient proposer diverses tâches liées à la réalisation de vérifications spécifiques pour confirmer le fonctionnement sécurisé de la mémoire dans les bibliothèques Rust ou le développement d'outils pour automatiser de telles vérifications. L'achèvement réussi de l'objectif de vérification (fournir une preuve formelle de fiabilité) implique une récompense. Un dépôt a été créé pour réaliser des expériences et publier les résultats, qui est un fork du dépôt standard de Rust.
Actuellement, 13 tâches ont été proposées. Par exemple, l'une des tâches consiste à vérifier la sécurité de l'utilisation de pointeurs bruts dans les fonctions du module core::ptr et à fournir une preuve formelle de la correction des opérations sur les pointeurs. Pour la vérification, des outils existants tels que Aeneas, Kani, Gillian, Verus et Creusot peuvent être utilisés, ou de nouveaux peuvent être proposés. Exemples de tâches réalisées.
Source : opennet.ru
