Compilation abstraite et synthèse d'invariants basée sur des domaines numériques paramétrés

07-09-2017
Người thuyết trình : Franck Védrine (CEA)
Depuis plusieurs années, le CEA List développe à travers le logiciel Fluctuat des analyses statiques de code numérique offrant les garanties des analyses par interprétation abstraite pour la précision des calculs. Les analyses ayant le plus le pertinence en terme de retour utilisateur sont celles où les domaines et les erreurs numériques sont modélisées par des formes affines ou zonotopes.
Ces analyses couvrent exhaustivement tous les chemins d'exécution et donnent des résultats précis et rapides pour les composants numériques et certains codes de librairie. Dans cet exposé, nous présenterons deux techniques récentes qui permettent d'améliorer les temps d'analyse tout en conservant la finesse de ces diagnostics formels, même en présence de tests instables.
La première technique complémente l'interprétation abstraite de Fluctuat par une compilation abstraite réalisée en deux temps: un plugin de Frama-C transforme le code d'origine en lui rajoutant des points de synchronisations. La librairie float_diagnosis permet ensuite d'instrumenter le code "à la CADNA" de manière à obtenir le diagnostic de précision en exécutant le code instrumenté. Cette technique, couplée avec des scénarios d'analyse fins, permet d'améliorer les temps d'analyse de Fluctuat d'un facteur conséquent sur les codes numériques de plusieurs milliers de lignes de code.
La seconde technique est basée sur des techniques d'accélérations spécifiques aux zonotopes pour améliorer l'atteinte d'un point fixe dans les analyses par interprétation abstraite. Elle synthétise des invariants linéaires inductifs en utilisant une méthode de variation des constantes. Elle se révèle être complète sur la famille des filtres linéaires convergents. Sur la plupart des filtres linéaires testés, elle fournit un invariant en quelques dizaines de cycles d'apprentissage avant de fournir un invariant linéaire 1-inductif. Ce résultat est à comparer avec les résultats de Fluctuat qui requièrent plusieurs milliers cycles pour fournir un invariant k-inductif éventuellement moins précis avec k souvent supérieur à plusieurs centaines.