Résumé technique : Analyse quantitative de l'impact des correctifs symboliques

Énoncé du problème

La vérification d'équivalence traditionnelle classe les programmes comme étant soit équivalents, soit non équivalents. Cette classification binaire est insuffisante pour l'analyse de l'impact des correctifs, où la version corrigée est censée être non équivalente au code original (vulnérable) afin de remédier à une vulnérabilité. Bien que la non-équivalence soit attendue, le défi critique réside dans la détermination sous quelles conditions les programmes diffèrent et quel pourcentage du domaine d'entrée est affecté.

Les approches actuelles échouent souvent à distinguer un « bon » correctif qui résout une vulnérabilité tout en préservant la fonctionnalité pour la plupart des entrées, d'un « mauvais » correctif qui restreint excessivement les entrées (par exemple, en codant en dur des valeurs sûres ou en rejetant toutes les entrées), introduisant ainsi une non-équivalence sur une portion significativement plus grande du domaine d'entrée. Il manque des techniques pour quantifier formellement cette divergence comportementale.

Méthodologie

Les auteurs proposent l'Analyse Quantitative d'Équivalence Partielle, un cadre qui affine la non-équivalence en mesurant l'étendue de la divergence comportementale à travers le domaine d'entrée. La méthodologie se compose de trois composants principaux :

1. Formalisation de l'équivalence partielle

L'article définit un programme $P$ comme une fonction totale d'un domaine d'entrée $D_{IP}$ vers un domaine de sortie $D_{OP}$. Étant donné deux programmes $P_1$ (original) et $P_2$ (corrigé) partageant le même domaine d'entrée :

• Ensemble d'équivalence ($D_{eq}$) : L'ensemble des entrées où $P_1(\vec{I}) = P_2(\vec{I})$.
• Ensemble de non-équivalence ($D_{neq}$) : L'ensemble des entrées où $P_1(\vec{I}) \neq P_2(\vec{I})$.
• Surface d'impact du correctif : Définie comme $D_{neq}$. L'objectif est de calculer la condition d'équivalence ($F_{eq}$) et le pourcentage du domaine d'entrée où $D_{eq}$ est vérifié.

2. Analyse symbolique et résumé

L'approche utilise une exécution symbolique étendue pour générer des résumés symboliques ($S_P$) pour les deux programmes. Un résumé symbolique est une formule logique représentant la relation entre les entrées et les sorties pour tous les chemins d'exécution.

• Algorithme 1 (EqChecker) : Classe les programmes comme Équivalents ($T_{eq}$), Totalement Non Équivalents ($T_{neq}$), ou Partiellement Équivalents ($P_{eq}$) en vérifiant la satisfiabilité de $S_1 \Leftrightarrow S_2$ et $S_1 \land S_2$.

3. Techniques quantitatives (Heuristiques de recherche par intervalles)

Pour quantifier efficacement la taille de $D_{eq}$ et $D_{neq}$ dans les domaines numériques, les auteurs proposent une heuristique de recherche par intervalles. Cela évite l'ingérabilité computationnelle de l'énumération de toutes les entrées ou l'utilisation de comptage de modèles coûteux pour les grands domaines.

• Recherche par intervalles relationnelle (Algorithme 2) : Divise récursivement le domaine d'entrée en sous-domaines (en divisant les intervalles par deux) et vérifie l'équivalence ou la non-équivalence totale au sein de ces sous-domaines. Elle capture les conditions relationnelles entre plusieurs variables mais présente une complexité exponentielle $O((2^N)^{LIMIT})$.
• Recherche par intervalles itérative (Algorithme 3) : Traite un paramètre d'entrée à la fois pour améliorer l'évolutivité, réduisant la complexité à $O(N \times 2^{LIMIT})$. Cependant, elle ne peut pas capturer les contraintes relationnelles entre les variables.
• Recherche par intervalles itérative prioritaire (Algorithme 5) : Divise les domaines avec une priorité vers zéro (partitions négative, zéro, positive), basée sur l'intuition que les programmes sont plus susceptibles d'être équivalents pour des valeurs absolues plus petites.
• Recherche par intervalles combinée (Algorithme 6) : Intègre les approches itérative et prioritaire, sélectionnant la meilleure borne inférieure d'équivalence pour chaque paramètre d'entrée afin de fournir une analyse robuste.

4. Comparaisons avec des références

Les auteurs comparent leur approche de recherche par intervalles à :

• Comptage de modèles énumératif : Trouver itérativement des solutions satisfaisantes via des solveurs SMT.
• Projection et comptage de modèles : Utiliser l'élimination de quantificateurs et des outils de comptage de modèles (SearchMC, Ganak, qCoral, ABC) pour calculer les pourcentages d'équivalence.

Contributions clés

1. Formalisation : L'article formalise le concept d'équivalence partielle et de surface d'impact du correctif, étendant l'analyse d'équivalence pour inclure les conditions d'équivalence/non-équivalence et leurs pourcentages correspondants.
2. Développement de technique : Il propose une technique basée sur la recherche par intervalles spécifiquement conçue pour l'analyse quantitative efficace des domaines d'entrée numériques, fournissant une borne inférieure sûre sur l'équivalence.
3. Analyse de l'impact des correctifs : La technique est appliquée pour évaluer l'impact des correctifs, distinguant les correctifs qui affectent minimalement le domaine d'entrée (bons correctifs) de ceux qui restreignent excessivement les entrées (mauvais correctifs).
4. Évaluation sur des benchmarks : L'approche est évaluée sur :
   • PatchBench : 90 correctifs CVE provenant de Linux, Qemu et FFmpeg.
   • JulietBench : 50 programmes avec des correctifs bons et mauvais (incluant des correctifs mauvais générés par des LLM).
   • EqBench : 47 programmes C, où l'outil a identifié 5 cas étiquetés à tort comme « équivalents » en raison de débordements d'entiers.

Résultats expérimentaux

• Différenciation des correctifs : Dans le jeu de données JulietBench, les mauvais correctifs ont présenté une surface d'impact moyenne de 96,65 %, tandis que les bons correctifs n'ont affecté que 29,03 % du domaine d'entrée.
• Variabilité réelle : Dans PatchBench, 36,25 % des correctifs étaient non équivalents pour plus de 90 % du domaine d'entrée, tandis que 20 % affectaient moins de 10 %. Cela met en évidence une variance significative dans les impacts réels des correctifs.
• Précision et efficacité :
  • L'approche de Recherche par intervalles combinée a atteint une précision de 81,8 % sur PatchBench et de 95,2 % sur EqBench pour produire des résultats d'équivalence exacts (avec une vérité terrain connue), surpassant la méthode suivante de 30,7 %.
  • Elle a fourni une approximation plus proche de la vérité terrain que les approches de comptage de modèles, avec un écart moyen environ 29,4 % inférieur à celui de la deuxième meilleure approche.
  • Temps d'exécution : RangeSearch a fonctionné environ 8 fois plus vite que SearchMC sur PatchBench et 2 fois plus vite sur EqBench.
• Résultats EqBench : L'analyse a identifié 5 cas dans EqBench étiquetés à tort comme équivalents ; l'outil les a correctement identifiés comme partiellement équivalents en raison de conditions de débordement d'entiers.

Importance et affirmations

L'article affirme que l'Analyse Quantitative d'Équivalence Partielle caractérise et quantifie efficacement l'impact des correctifs, offrant un aperçu plus raffiné que la vérification d'équivalence binaire.

• Implications pour la sécurité : Elle aide à identifier les correctifs qui peuvent nécessiter une attention supplémentaire (par exemple, ceux affectant de grandes portions du domaine d'entrée) et distingue les correctifs sécurisés qui préservent la fonctionnalité de ceux qui brisent des hypothèses existantes ou des pipelines CI/CD en restreignant excessivement les entrées.
• Contribution méthodologique : Ce travail introduit une nouvelle heuristique de recherche par intervalles qui équilibre l'évolutivité et la précision, abordant les limites des techniques existantes d'exécution symbolique et de comptage de modèles dans le contexte de l'analyse de l'impact des correctifs.
• Limites : Les auteurs reconnaissent que l'approche repose sur une exécution symbolique différentielle ; si des résumés symboliques ne peuvent pas être générés, l'analyse ne peut pas se poursuivre. De plus, les heuristiques de recherche par intervalles actuelles sont centrées sur les domaines numériques, bien que les auteurs notent un potentiel d'extension à d'autres domaines (par exemple, les chaînes de caractères).

Les auteurs ne prétendent pas résoudre tous les problèmes d'analyse des correctifs, mais affirment que leur approche quantitative fournit une couche de granularité nécessaire pour comprendre les conséquences comportementales des correctifs logiciels.