Direction de recherche : Antoine MINÉ

Analyse Statique Incrémentale pour la Vérification de Programmes

Frama-C est une plateforme d'analyse de code C composée d'un ensemble d'analyseurs. Frama-C peut garantir qu'un programme C vérifie sa spécification formelle à travers différentes techniques comme l'interprétation abstraite, le calcul de plus faible précondition ou la vérification d'assertion à l'exécution. Au sein de Frama-C, Eva est un plugin dédié à l'inférence automatique de propriété des programmes C et permet de trouver toutes les valeurs possibles de chaque variable ou encore les relations arithmétiques entre les variables. Le but premier de cette analyse est de prouver l'absence d'erreur à l'exécution (ex: les débordements arithmétiques, les accès mémoires invalides, n'importe quel autre comportement indéfini du C, ...). Il est également utilisée pour conduire de l'audit de code et comme support pour d'autres analyses. Il réalise une interprétation abstraite du programme qui a l'avantage d'être à la fois complètement automatique (aucune interaction avec l'utilisateur n'est nécessaire pendant l'analyse) et de passer à l'échelle. Dans un contexte industriel, il est souvent requis de réaliser ces analyses de manière incrémentale. Il y a deux cas d'utilisation (non exclusifs) d'une analyse incrémentale. 1. Pendant le développement d'un logiciel critique, des analyses peuvent être conduites pour détecter d'éventuels problèmes le plus tôt possible ou pour s'assurer que le logiciel sera facilement validé par ce genre d'analyses dès que la phase de validation débutera. La validation continue du logiciel nécessite un grand nombre d'analyses à exécuter entre chaque modification et le temps de calcul cumulé pourrait rendre la méthodologie impraticable. Dans ce contexte, il est également possible d'analyser les différences sémantiques impliquées par chaque modification. 2. Postérieurement au développement initial, une procédure de certification généralement réalisée par une équipe différente peut reposer sur une analyse complétée. Bien que cela ne requiert qu'une seule analyse, les expériences passées montrent qu'une telle analyse doit être finement réglée pour aboutir. En pratique, ce paramétrage est fait de manière incrémentale en ajustant les paramètres à chaque itération jusqu'à ce que l'outil parvienne à prouver l'absence d'erreur à l'exécution. Le coût de ce processus est d'un ordre de grandeur plus grand que le coût d'une analyse et risque d'être rédhibitoire. Il est crucial dans les deux scenarios que les analyses ultérieures coûtent considérablement moins que la première. Cependant la réutilisation de résultats précédents en interprétation abstraite est toujours un problème ouvert. Le but de ce sujet est d'explorer des solutions à ce problème et de les valider en les implantant dans la plateforme Frama-C. En particulier, cela inclut de la recherche sur - la catégorisation des changements dans le code source ou dans les paramètres de l'analyse et de leurs impacts sur l'analyse; - la conception de résumés d'analyse de fonction ou de fragments de code qui puissent être stockés sur disque et adéquat à la réutilisation; - la réutilisation d'invariants de boucle précédemment inférés pour accélérer la convergence des analyses postérieures; - la conception de stratégies d'itération plus adaptées à l'analyse incrémentale, en particulier dans le cas de la réutilisation de résumés ou d'invariants. Les solutions proposées seront implantées dans Eva mais devraient être suffisamment générales pour pouvoir être facilement adaptées à d'autres outils comme Mopsa et EACSL.

Publications 2024

• 2024
  • M. Razafintsialonina, D. Bühler, A. Miné, V. Perrelle, J. Signoles : “Réutilisations de caches et d’invariants pour l’analyse statique incrémentale”, 35^es Journées Francophones des Langages Applicatifs (JFLA 2024), Saint-Jacut-de-la-Mer, France (2024)