RPP : Preuve automatique de propriétés relationnelles par Self-Composition

Lionel Blatter (1, 2) , Nikolai Kosmatov (1, 2) , Pascale Le Gall (3) , Virgile Prévosto (1, 2)

1 LSL - Laboratoire Sûreté des Logiciels
2 DILS (CEA, LIST) - Département Ingénierie Logiciels et Systèmes
3 MICS - Mathématiques et Informatique pour la Complexité et les Systèmes

Contexte. Les méthodes de vérification déductive basées sur la logique de Hoare [7] fournissent une approche puissante pour prouver qu'une fonction respecte certaines propriétés. Elles sont généralement couplées à un langage permettant de spécifier formellement les propriétés attendues, en particulier sous forme de contrats de fonction. Un tel contrat comprend des pré-et des post-conditions décrivant respectivement les entrées attendues et le comportement exigé de la fonction. Problème. Cependant, toutes les propriétés qu'on peut vouloir établir sur un programme donné ne s'expriment pas facilement sous cette forme. En effet, un contrat de fonction décrit le déroulement d'une exécution d'une fonction donnée. Cependant, il est fréquent qu'on veuille parler d'une propriété relationnelle mettant en jeu l'exécution de plusieurs fonctions, ou comparer les résultats d'une même fonction sur différents paramètres. En particulier, des groupes de fonctions sont fréquemment liés par des spécifications algébriques [8] précisant leurs relations. Les contrats de fonction et les méthodes déductives classiques se prêtent mal à la spécification et à la vérification de telles propriétés. Des exemples de telles propriétés incluent : ∀x, y; x <= y => f (x) <= f (y) Decrypt(Crypt(M sg, P rivKey), P ubKey) = M sg On retrouve un sous ensemble des propriétés relationnelles dans le domaine du test, appelées propriétés métamorphique [6], liant plusieurs appels de la même fonction. Contributions. Afin de répondre a ce manque de support pour les propriétés relationnelles lors de la vérification à base de contrats, nous proposons le plugin FRAMA-C/RPP présenté dans [4]. L'outil réalise un ensemble de transformations automatiques à partir d'un langage de spécification capable d'exprimer des propriétés relationnelles. Le résultat des transformations permet de prouver des propriétés relationnelles et de les utiliser comme hypothèse dans d'autres preuves en utilisant des outils de vérification déductive standard.

Domaines: Génie logiciel [cs.SE]

Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prévosto. RPP : Preuve automatique de propriétés relationnelles par Self-Composition. Approches Formelles pour l'Assistance au Développement de Logiciels - AFADL, Jun 2018, Grenoble, France. ⟨cea-01835491⟩