Un nouvel outil automatise la vérification formelle des logiciels système
La vérification formelle des systèmes, qui prouve mathématiquement que le code est sécurisé en toutes circonstances, est une technologie relativement nouvelle. Les logiciels deviennent de plus en plus complexes et difficiles à maîtriser à l’aide des techniques de test de logiciels traditionnelles. Rendre les logiciels corrects, sûrs et sécurisés devient encore plus critique à mesure que l’utilisation de techniques d’IA générative telles que ChatGPT pour écrire automatiquement des programmes augmente. En fait, des vérifications seront encore plus nécessaires pour garantir que les programmes générés automatiquement sont corrects.
Des travaux récents dirigés par les professeurs Ronghui Gu et Jason Nieh ont introduit un nouvel outil, Spoq, qui réduit considérablement les efforts complexes que les utilisateurs doivent déployer pour vérifier les logiciels du monde réel et permet de vérifier le code des systèmes C existants sans modifications.
La vérification formelle offre une approche systématique et rigoureuse de la vérification des logiciels et du matériel, contribuant à garantir que les systèmes se comportent correctement et répondent aux spécifications prévues. Avec Spoq, de nombreux aspects de la vérification formelle peuvent être automatisés, réduisant considérablement les efforts de preuve manuelle pour la vérification. Le document a été présenté lors du 17e Symposium USENIX sur la conception et la mise en œuvre des systèmes d’exploitation (OSDI), le 12 juillet 2023.
Le logiciel système constitue la base logicielle de notre infrastructure informatique. Les logiciels système modernes sont volumineux, complexes et imparfaits, et comportent des vulnérabilités qui peuvent être exploitées pour compromettre la sécurité d’un système. La vérification formelle offre une solution potentielle à ce problème en prouvant mathématiquement que le logiciel système peut fournir des garanties de sécurité critiques. Malheureusement, cela reste trop difficile et demande trop d’efforts humains pour être appliqué dans la pratique.
Les outils précédents développés par les équipes de Nieh et Gu introduisaient des techniques de vérification pour rendre possibles certaines preuves qui n’auraient pas pu être faites auparavant. La principale caractéristique de Spoq est qu’il automatise les parties fastidieuses et chronophages de nombreuses preuves. « Spoq peut générer des résultats en une heure environ, au lieu de le faire manuellement, ce qui peut prendre des mois, voire des années, pour vérifier formellement un système », explique Xupeng Li, auteur principal de l’article et titulaire d’un doctorat. étudiant avec Nieh et Gu.
Au cours des prochains mois, le laboratoire s’efforcera de rendre Spoq open source afin que la vérification formelle puisse être largement déployée pour sécuriser les fondations logicielles de notre infrastructure informatique.
L’étude s’intitule « Spoq : mise à l’échelle de la vérification des systèmes vérifiables par machine en Coq ».
