Soutenance de thèse Virgile Robles

Spécifier et vérifier des exigences de haut-niveau sur des programmes importants: application à la sécurité des programmes C

Bien que les logiciels continuent de se complexifier et que la cyber-sécurité soit en train de devenir un enjeu majeur d'une société où l'automatisation est maintenant la norme, la spécification et la vérification d'exigences haut niveau (comme des propriétés de sécurité, telles que l'intégrité des données ou la confidentialité) sur des logiciels de taille importante reste un défi pour l'industrie. Cependants, de telles exigences haut niveau représentent la majeure partie des cahiers des charges écrits et compris par les ingénieurs, et il est nécessaire de faciliter leur utilisation des méthodes formelles.

Cette thèse présente un cadre formel pour les exigences de haut niveau appelé les meta-propriétés, décrites pour un langage de programmation abstrait, et centrées sur les propriétés liées aux manipulations de la mémoire et les invariants globaux. Ce cadre formel est appliqué au langage C avec HILARE, une extension d'ACSL (un langage de spécification formel pour les programmes C), qui permet la spécification d'exigences haut niveau sur des programmes C de grande taille avec facilité.

Des techniques de vérification pour HILARE, basées sur la génération d'assertions locales et la réutilisation des analyseurs de Frama-C existants (Wp, EVA, E-ACSL), sont présentées et implantées dans le greffon MetAcsl pour Frama-C. Une méthodologie complète pour l'évaluation des propriétés de grands programmes est détaillée, articulant les méta-propriétés, les techniques de vérification et les particularités du C. Cette méthodologie est illustrée par un large ensemble d'exemples et de propriétés de sécurité, et est en particulier appliquée à un cas d'étude complexe impliquant le chargeur d'amorçage de Wookey, un périphérique de stockage USB sécurisé.

Enfin, nous explorons une autre manière de vérifier qu'une exigence de haut niveau est vérifiée par un programme en le déduisant d'autres exigences déjà prouvées, en décrivant un système de déduction formel prouvé en Why3/Coq et instancié en Prolog pour être intégré dans MetAcsl.