💻 computer science

A Modular Framework for Stack-Heap and Value Abstractions (Extended Version)

Cet article propose et formalise un cadre de mémoire modulaire et paramétrique basé sur l'interprétation abstraite qui sépare les analyses de valeurs et de mémoire en domaines abstraits distincts, permettant une analyse statique saine de divers langages de programmation et de leurs comportements variables de pile et de tas afin de détecter des erreurs d'exécution critiques.

Auteurs originaux : Giacomo Boldini, Luca Negrini, Luca Olivieri, Pietro Ferrara

Publié 2026-07-20

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Giacomo Boldini, Luca Negrini, Luca Olivieri, Pietro Ferrara

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Le sac à dos invisible et le casier magique

Imaginez que vous écrivez une histoire pour un ordinateur. Pour raconter l'histoire, l'ordinateur a besoin d'un endroit pour garder ses notes, ses personnages et ses rebondissements. Dans le monde de la programmation, cela s'appelle la mémoire. Mais les ordinateurs ne possèdent pas simplement un grand carnet ; ils ont deux types de stockage très différents. L'un est comme un sac à dos (la « pile » ou stack) qui contient des objets temporaires dont vous avez besoin immédiatement, comme les variables locales d'une fonction. Vous y mettez des choses, vous les en sortez, et quand vous avez terminé le chapitre, le sac à dos est vidé. L'autre est comme un casier magique (le « tas » ou heap) où vous pouvez stocker des choses pour toujours, ou du moins jusqu'à ce que vous décidiez de les jeter. C'est là que vivent les objets complexes, comme une liste d'amis ou une immense base de données.

Le problème est que les ordinateurs sont incroyablement littéraux. Si vous dites à un ordinateur de mettre un livre dans un casier qui n'existe pas, ou si vous essayez de sortir un livre d'un casier que vous avez déjà vidé, toute l'histoire s'effondre. C'est ce qu'on appelle un « bug », et cela peut créer des failles de sécurité par lesquelles des méchants pourraient s'introduire. Pour empêcher cela, les informaticiens utilisent l'analyse statique. Considérez cela comme un éditeur super intelligent qui lit votre histoire avant de la publier, en essayant de prédire toutes les façons possibles dont l'intrigue pourrait mal tourner. Cet éditeur doit comprendre non seulement ce que sont les nombres (les valeurs), mais aussi où ils se cachent dans les sacs à dos et les casiers (la mémoire). Pendant des années, les éditeurs étaient doués pour vérifier les nombres ou vérifier la mémoire, mais rarement les deux en même temps sans s'embrouiller.

La boîte à outils modulaire pour les histoires d'ordinateurs

Dans cet article, les auteurs, une équipe de l'Université Ca' Foscari de Venise, proposent une nouvelle façon de construire ces éditeurs super intelligents. Ils appellent cela un Cadre Modulaire pour les Abstractions de Pile-Tas et de Valeur. Au lieu de construire un éditeur unique et rigide qui essaie de tout faire, ils ont construit une boîte à outils flexible où différentes parties peuvent être échangées comme des briques Lego.

L'idée centrale est une astuce ingénieuse appelée « État Divisé » (Split State). Imaginez que vous organisez une chambre en désordre. Au lieu d'essayer de suivre chaque chaussette et chaque livre dans une seule et immense liste, vous décidez de diviser la chambre en deux zones : la « Zone de Valeur » (où vous suivez les nombres et les données) et la « Zone de Mémoire » (où vous suivez les emplacements et les adresses). Les auteurs prouvent mathématiquement que vous pouvez séparer ces deux zones sans perdre d'information. C'est comme si deux personnes différentes géraient la chambre : l'une ne se soucie que de ce que sont les objets (une chaussette rouge, un livre bleu), et l'autre ne se soucie que de leur emplacement (sur l'étagère, dans le tiroir). Ils communiquent entre eux à l'aide d'un ensemble spécial d'« identifiants de mémoire » — comme des étiquettes de nom — afin de rester synchronisés.

L'article formalise cette idée en utilisant un petit langage de programmation imaginaire appelé µLL (qui est une version simplifiée de C ou C++). Ils montrent qu'en séparant le « quoi » du « où », vous pouvez mélanger et assortir différents types d'éditeurs. Par exemple, vous pourriez utiliser un éditeur simple qui vérifie uniquement si les nombres sont positifs, et l'associer à un éditeur complexe qui suit les déplacements des pointeurs (l'équivalent numérique de « allez à ce casier »). Ou encore, vous pourriez remplacer l'éditeur par un plus puissant qui suit les plages de nombres. Le cadre garantit que, peu importe les deux éditeurs que vous choisissez, ils fonctionneront ensemble correctement et ne manqueront aucune erreur.

Les auteurs démontrent cela en construisant deux exemples spécifiques : l'un qui suit des plages de nombres simples (comme « ce nombre est compris entre 1 et 10 ») et un autre qui suit l'endroit où les pointeurs pointent (comme « cette variable pointe vers le casier étiqueté 'A' »). Ils montrent que lorsque ces deux éléments travaillent ensemble, ils peuvent détecter des bugs subtils impliquant à la fois des nombres et des emplacements mémoire, tels qu'un programme qui écrase accidentellement un bloc de mémoire parce qu'un compteur est devenu trop élevé.

Crucialement, l'article s'oppose à l'ancienne méthode, où les éditeurs étaient souvent codés en dur pour gérer des types de données spécifiques ou nécessitaient des annotations manuelles de la part du programmeur. Les auteurs démontrent que leur approche est paramétrique, ce qui signifie qu'elle ne se soucie pas de savoir quel éditeur spécifique vous utilisez pour les valeurs ou la mémoire, tant qu'ils respectent les règles de leur interface. Ils prouvent mathématiquement que ce système est sûr (sound), ce qui signifie que si leur cadre dit qu'un programme est sûr, il l'est réellement (il ne manquera pas de bug), même s'il arrive parfois qu'il dise qu'un programme pourrait être dangereux alors qu'il est parfaitement correct (une « fausse alerte », ce qui est préférable à un plantage).

L'article ne prétend pas avoir résolu tous les problèmes du monde de la programmation. Il ne dit pas que son cadre est le plus rapide ou le plus précis pour chaque langage. Au lieu de cela, il fournit une base solide et prouvée — un « cadre modulaire » — qui permet aux chercheurs et aux développeurs de construire de meilleurs outils, plus adaptables, pour vérifier le code. C'est un plan pour construire un filet de sécurité plus intelligent et plus flexible pour les logiciels qui font tourner notre monde.

Résumé Technique : Un Cadre Modulaire pour les Abstractions de Pile-Tas et de Valeur

Énoncé du Problème
L'analyse statique de programmes avancée nécessite un raisonnement précis sur la sémantique de la mémoire, en particulier l'interaction entre les allocations de pile (statiques) et de tas (dynamiques), ainsi que la manière dont elles affectent les valeurs du programme. Dans des langages comme le C et le C++, la gestion manuelle de la mémoire introduit des risques tels que les dépassements de tampon (buffer overflows), les erreurs d'utilisation après libération (use-after-free) et les exceptions de pointeurs nuls. À l'inverse, les langages comme Java et Python utilisent la collecte de déchets automatique, mais les comportements de mémoire sous-jacents varient néanmoins de manière significative.

Un défi critique dans l'analyse statique est que l'analyse de la mémoire (suivi des pointeurs, des alias et des structures) et l'analyse de valeur (suivi des propriétés numériques, des constantes et des intervalles) se sont historiquement développées de manière orthogonale. Bien que la combinaison de ces analyses soit connue pour être essentielle à l'obtention de résultats significatifs, les approches existantes manquent souvent de généralité. Certains outils prétraitent les programmes pour remplacer les accès au tas par des variables symboliques, tandis que d'autres reposent sur des extensions manuelles ou des spécifications de structures de données spécifiques. Il manque des cadres véritablement génériques et entièrement automatiques capables de supporter divers modèles de mémoire (du C aux langages orientés objet) et permettant de choisir et de combiner les domaines de valeur et de mémoire de manière indépendante sans nécessiter d'annotations fournies par l'utilisateur.

Méthodologie
Les auteurs proposent un cadre générique et paramétrique basé sur la théorie de l'interprétation abstraite. L'innovation centrale est une abstraction d'état scindée qui sépare formellement l'état du programme en deux composants modulaires : un composant de valeur ( $\nu$ ) et un composant de mémoire ( $\mu$ ).

Langage Formel ( $\mu$ LL) : Le cadre est défini sur $\mu$ LL, un petit langage impératif étendant $\mu$ JS avec des pointeurs explicites, des opérations d'adressage, de déréférencement, d'accès aux champs et d'allocation de tas. Ce langage sert de modèle pour les comportements de mémoire de type C++.
Construction de l'État Scindé : Les auteurs définissent une transformation de l'état concret vers l'état scindé qui est un isomorphisme de Galois. Contra la différence avec les travaux précédents qui établissaient une connexion de Galois (ce qui peut introduire de l'imprécision), cette approche garantit une application bijective entre l'état concret (cartes de pile et de tas) et l'état scindé.
- Le Composant de Valeur ( $\nu$ ) stocke les valeurs primitives et les valeurs de champs.
- Le Composant de Mémoire ( $\mu$ ) stocke les adresses mémoire et les relations de pointeurs.
- Les objets sont « éclatés » en mappages de champs plats, où chaque champ est stocké soit dans le composant de valeur, soit dans le composant de mémoire, selon son type (primitif vs adresse).
Interaction Modulaire : Le cadre définit une interface légère par laquelle le domaine de valeur ( $V^\sharp$ $V^{♯}$ ) et le domaine de mémoire ( $M^\sharp$ $M^{♯}$ ) coopèrent :
- Identifiants de Mémoire (MemID) : Noms abstraits représentant des emplacements mémoire concrets.
- Substitutions : Lorsque le domaine de mémoire réorganise les emplacements (par exemple, en fusionnant ou en divisant des nœuds), il communique ces changements au domaine de valeur via des substitutions, assurant ainsi la cohérence.
- Opérations : Le cadre spécifie un ensemble d'opérations requises pour chaque domaine (par exemple, assign, assume, pointsTo, access, fresh) qui gèrent le flux d'informations. Le domaine de valeur gère l'arithmétique et la logique booléenne, tandis que le domaine de mémoire gère la structure des pointeurs et l'allocation.
Correction (Soundness) : La correction de l'analyse combinée est garantie par la correction des domaines individuels et la justesse de leur interaction via le mécanisme de substitution. Le cadre prouve que si les domaines individuels satisfont des conditions locales spécifiques (C1–C2 et M1–M6), l'analyse sémantique combinée est correcte par rapport aux sémantiques concrètes.

Contributions Clés
Le document présente quatre contributions techniques principales :

Sémantique Opérationnelle Formelle : Une sémantique pour $\mu$ LL qui modélise à la fois la pile et le tas, supportant l'allocation dynamique, l'aliasing de pointeurs et les structures de données complexes.
Abstraction d'État Scindé : Une reformulation de l'état concret en tant qu'isomorphisme de Galois qui sépare l'information de valeur et d'adresse sans perte de précision. Cela permet aux analyses de valeur et de mémoire d'opérer sur des sous-composants distincts et bien définis de l'état.
Cadre Abstrait Paramétrique : Une architecture modulaire où les domaines de valeur et de mémoire interagissent via une interface légère et un mécanisme de substitution. Cette conception supporte une large gamme de modèles de mémoire (y compris la manipulation diverse du C) et permet de coupler n'importe quel domaine de valeur compatible avec n'importe quel domaine de mémoire compatible.
Instanciations Concrètes : Les auteurs démontrent l'applicabilité de leur cadre en l'instanciant avec des domaines numériques non relationnels (par exemple, Intervalles, Signe, Propagation de Constantes) pour les valeurs et une analyse de type Andersen pour la mémoire.

Résultats et Évaluation
Le document ne présente pas de bancs d'essai empiriques à grande échelle mais fournit une validation théorique et des exemples illustratifs :

Démonstration de la Modularité : Un programme d'exemple impliquant une allocation de tas et des mises à jour conditionnelles montre que le remplacement du domaine de valeur (par exemple, de la Propagation de Constantes aux Intervalles ou aux Ensembles de Constantes) modifie la précision des résultats tout en laissant le domaine de mémoire et la logique centrale du cadre inchangés.
Traçage d'Interaction : Les auteurs tracent l'exécution d'un programme riche en pointeurs (basé sur un benchmark SV-COMP) pour démontrer comment le domaine de mémoire suit les alias de pointeurs (par exemple, tail et x pointant vers la même structure) tandis que le domaine de valeur suit les données stockées à ces emplacements.
Comportement de Convergence : Dans un exemple combiné impliquant un compteur et des champs de tas, les auteurs montrent comment le domaine de mémoire atteint un point fixe indépendamment du comportement de convergence du domaine de valeur (par exemple, le domaine des intervalles nécessitant un élargissement alors que le domaine du signe ne le nécessite pas), soulignant la nature à la fois indépendante et coopérative de l'état scindé.

Signification
Les auteurs affirment que ce travail constitue une fondation flexible pour la construction d'analyses statiques adaptables à différents langages de programmation et exigences d'analyse. En découplant le raisonnement sur la mémoire et sur la valeur, le cadre :

Améliore la Réutilisabilité : Les domaines abstraits existants peuvent être intégrés au cadre avec une adaptation minimale à une interface commune.
Améliore la Précision : Il permet de suivre l'information de valeur sur les emplacements mémoire (par exemple, la valeur d'un champ dans un objet du tas) d'une manière qui n'est pas possible avec de simples produits cartésiens ou des analyses isolées.
Assure une Correction Compositionnelle : Le cadre garantit que si les composants individuels sont corrects, la combinaison est correcte par construction, éliminant ainsi le besoin de prouver à nouveau la correction pour chaque nouvelle combinaison de domaines.

Les auteurs positionnent ce travail comme une extension de cadres précédents (spécifiquement Ferrara [19,18] et Negrini [34]), l'améliorant par le support d'arbitraires références, d'accès dynamiques aux champs, et en imposant un isomorphisme de Galois pour éliminer la perte de précision lors de la transformation de l'état scindé. Les travaux futurs prévoient l'intégration de ce cadre dans la plateforme d'analyse statique LiSA pour supporter des langages tels que C, C++, Rust et LLVM-IR.

Le sac à dos invisible et le casier magique

La boîte à outils modulaire pour les histoires d'ordinateurs

Articles similaires