< Retour au sommaire

Soutenance de thèse de Virgile Robles

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

le

Lieu: Nano-Innov, Amphis 33/34

Suivre en visio

Avertissement

En raison des contraintes sanitaires, le nombre de places en présentiel est très restreint, merci de privilégier la visio.

Résumé

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é) reste un défi pour l’industrie, alors que les cahiers des charges en sont remplis. Cette thèse présente un cadre formel pour les exprimer appelé les méta-propriétés, décrites pour un langage dé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, 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, sont présentées et implantées dans le greffon MetAcsl pour Frama-C. Une méthodologie 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 cas d’étude complexe : le bootloader de Wookey, un périphérique de stockage chiffré. Enfin, nous explorons une autre manière de vérifier une exigence de haut niveau en la déduisant à partir d’autres, via un système formel prouvé en Why3 et intégré dans MetAcsl.

Jury