PR28 INCYBER Preuve d’intégrité avec Frama C MetAcsl

Frama-C est un outil d’analyse de programmes C, muni d’un langage de spécifications formelles ACSL, dans lequel on peut décrire les propriétés attendues du code, sous la forme de contrats de fonction et d’assertions logiques. Ce type d’annotations est bien adapté pour décrire des propriétés fonctionnelles du programme, c’est à dire intuitivement que le programme calcule bien ce qu’on attend de lui. En revanche, d’autres classes de propriétés sont difficilement exprimables en ACSL, exigeant un encodage complexe et donc source potentielle d’erreur dans la spécification elle-même. C’est typiquement le cas pour des propriétés de sécurité comme l’intégrité ou la confidentialité du contenu de locations mémoire du programme, qui demanderaient en théorie d’ajouter des assertions pour chaque accès en écriture (respectivement en lecture), ce qui devient rapidement rédhibitoire.

Allez à la source