💻 computer science

From TinyGo to gc Compiler: Extending Zorya's Concolic Framework to Real-World Go Binaries

Ce document présente une extension du cadre d'exécution concolique Zorya pour prendre en charge les binaires Go multithreadés compilés avec le compilateur gc standard, permettant la détection de vulnérabilités réelles dans des projets de production tels que Kubernetes et Go-Ethereum en restaurant les états des threads, en neutralisant la préemption d'exécution et en employant une analyse de chemin par superposition.

Auteurs originaux : Karolina Gorna, Nicolas Iooss, Yannick Seurin, Rida Khatoun, Keith Makan

Publié 2026-05-06

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Karolina Gorna, Nicolas Iooss, Yannick Seurin, Rida Khatoun, Keith Makan

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

Imaginez que vous êtes inspecteur de sécurité chargé de repérer des pièges cachés dans une usine massive et complexe. Cette usine est un logiciel écrit en langage de programmation Go.

Pendant longtemps, les inspecteurs de sécurité disposaient d'un outil spécial appelé Zorya, excellent pour inspecter de petites usines simples (appelées « binaires TinyGo »). Mais les usines réelles utilisées par de grandes entreprises comme Kubernetes et Ethereum sont immenses, chaotiques et fonctionnent avec de nombreux ouvriers (threads) simultanément. L'ancien outil Zorya ne pouvait pas gérer ces grandes usines ; il se perdait dans le bruit et la complexité.

Cet article porte sur la mise à niveau de Zorya afin qu'il puisse enfin inspecter ces usines Go réelles et multi-ouvriers. Voici comment ils ont procédé, expliqué simplement :

1. Le Problème : L'« Usine Bondée »

Le compilateur Go standard (appelé gc) construit des logiciels qui démarrent toute une équipe d'ouvriers invisibles (threads du système d'exploitation) juste pour gérer le travail. Il dispose également d'un « régulateur de circulation » (le runtime) capable d'arrêter n'importe quel ouvrier à tout moment pour laisser passer quelqu'un d'autre en premier.

L'Ancien Outil : Zorya était utilisé pour inspecter des usines calmes à un seul ouvrier. Lorsqu'il tentait d'examiner des usines actives à plusieurs ouvriers, il ne parvenait pas à déterminer qui faisait quoi ni où se trouvaient les ouvriers.
L'Objectif : Rendre Zorya assez intelligent pour mettre le chaos en pause, prendre une photo instantanée de chaque ouvrier, puis inspecter soigneusement le travail sans se perdre.

2. La Solution : Trois Nouvelles Super-pouvoirs

Les auteurs ont donné à Zorya trois nouvelles astuces pour gérer les grandes usines :

Le « Snapshot Voyage dans le Temps » (Restauration des états des threads) :
Imaginez que l'usine fonctionne à pleine vitesse. Au lieu d'essayer d'observer les ouvriers se déplacer en temps réel (ce qui est trop rapide et confus), le nouveau Zorya appuie sur « pause », prend une photo haute définition des mains, des outils et de la position de chaque ouvrier, et l'enregistre. Lorsqu'il lance son inspection, il recharge ces photos pour savoir exactement où se trouvait chacun avant le début. Cela lui permet d'ignorer le chaos du « régulateur de circulation » et de se concentrer sur le code réel.
Le Miroir « Et Si » (Analyse de chemin par superposition) :
Habituellement, lorsqu'un ouvrier arrive à un carrefour, il choisit un chemin et le parcourt. L'autre chemin est ignoré.
- L'Ancienne Méthode : Zorya ne vérifiait que le chemin emprunté par l'ouvrier.
- La Nouvelle Méthode : Zorya crée un « miroir fantôme » de l'usine. Lorsque l'ouvrier choisit le chemin de gauche, Zorya envoie un « ouvrier fantôme » sur le chemin de droite pour quelques pas seulement. Il vérifie si ce chemin contient un piège (comme un trou dans le sol ou un outil cassé) sans réellement le parcourir. Si le fantôme trouve un piège, Zorya déclenche l'alarme. Cela s'appelle Copy-on-Write (copie lors de l'écriture) : il ne copie que les parties de l'usine touchées par le fantôme, économisant ainsi une énorme quantité d'énergie.
Le Détecteur de « Piège Silencieux » :
Certains pièges ne font pas de bruit (comme un plantage ou une panique). Par exemple, un nombre peut devenir si grand qu'il « fait le tour » et redevient petit, brisant silencieusement les mathématiques. D'autres outils manquent ces cas car ils ne recherchent que les plantages bruyants. Zorya utilise un cerveau mathématique ultra-intelligent (appelé résolveur SMT) pour faire les calculs dans sa tête. Il peut dire : « Hé, si ce nombre augmente, il brisera silencieusement les mathématiques », même si le programme ne plante pas.

3. Le Test : Repérage de Vrais Bugs

L'équipe a testé ce Zorya amélioré sur 11 failles de sécurité réelles découvertes dans des logiciels célèbres comme Kubernetes, Go-Ethereum et CoreDNS. Ils ont comparé Zorya à d'autres outils tels que les analyseurs statiques (qui lisent le code comme un correcteur grammatical), les fuzzers (qui projettent des données aléatoires sur le logiciel) et d'autres scanners de sécurité.

Les Résultats :

Zorya a trouvé 7 bugs sur 11.
La Victoire « Silencieuse » : L'un des bugs trouvés par Zorya était un « débordement d'entier silencieux ». C'était une erreur mathématique qui ne faisait pas planter le programme et ne déclenchait aucune alarme. Aucun autre outil n'a trouvé ce bug sauf si quelqu'un leur avait indiqué manuellement exactement quoi chercher. Zorya l'a trouvé automatiquement.
Le Compromis : Zorya est plus lent que les outils de « projection de données aléatoires » (fuzzers). Alors qu'un fuzzer peut trouver un plantage en quelques secondes, Zorya prend environ 16 minutes pour trouver un bug. Cependant, Zorya n'a pas besoin qu'un humain écrive un script de test spécifique pour chaque fonction ; il analyse directement le fichier binaire.

4. La Conclusion

Cet article montre que nous pouvons désormais utiliser des inspections avancées par « ouvriers fantômes » pour repérer des failles de sécurité profondes et cachées dans des logiciels Go complexes et multi-threads. Bien que cela prenne un peu plus de temps que d'autres méthodes, cela permet de trouver des bugs « silencieux » que les autres outils manquent complètement, rendant notre infrastructure numérique plus sûre.

En bref : Ils ont appris à un robot de sécurité comment mettre en pause une usine chaotique, prendre une photo instantanée des ouvriers et vérifier les chemins que personne d'autre ne parcourt, trouvant ainsi avec succès des pièges cachés qui étaient auparavant invisibles.

Résumé Technique : De TinyGo au compilateur gc : Étendre le Framework Concolique de Zorya aux Binaires Go du Monde Réel

Énoncé du Problème

L'analyse de sécurité des binaires Go compilés avec le compilateur gc standard reste un défi majeur. Contrairement aux binaires compilés avec TinyGo (qui produisent des exécutables monothread avec des environnements d'exécution minimaux), les binaires compilés avec gc utilisent un environnement d'exécution complexe qui gère les goroutines, la collecte de déchets et l'ordonnancement préemptif à travers plusieurs threads du système d'exploitation. Les outils d'exécution symbolique existants (par exemple, KLEE, angr, Radius2) sont principalement conçus pour C/C++ et reposent sur des représentations intermédiaires (IR) LLVM auxquelles Go ne se compile pas entièrement. De plus, ces outils échouent souvent à modéliser les mécanismes d'exécution spécifiques à Go, tels que la préemption coopérative/asynchrone, l'ordonnancement des goroutines et les fonctions VDSO mappées en mémoire, ce qui les rend inefficaces face aux binaires Go de production. Les itérations précédentes du framework Zorya étaient limitées aux binaires TinyGo, laissant un vide dans l'analyse des applications Go multithread du monde réel.

Méthodologie

L'article présente une extension de Zorya, un framework d'exécution concolique qui élève les binaires compilés vers la représentation intermédiaire P-Code de Ghidra. L'extension permet l'analyse des binaires multithread compilés avec gc grâce à trois mécanismes techniques principaux :

Restauration et Ordonnancement de l'État Multithread :
- Zorya restaure l'état de tous les threads du système d'exploitation à partir de dumps gdb lors de l'initialisation, capturant les états des registres, les bases de stockage local par thread (TLS) et les traces d'appel.
- Les threads sont classifiés (par exemple, thread principal, moniteur système, en attente) pour faciliter l'ordonnancement.
- Le framework neutralise la préemption d'exécution et adopte une politique d'ordonnancement « main-only » pour l'analyse en mode fonction, restreignant l'exécution concolique au thread principal afin d'éviter les interruptions par la collecte de déchets ou les moniteurs système. Cela permet une exploration continue des fonctions au niveau utilisateur.
Analyse de Chemin par Superposition avec Sémantique Copier-Écrire (CoW) :
- Pour faire face à l'explosion des chemins et raisonner sur les branches non prises sans cloner l'état complet (ce qui peut dépasser 1 Gio pour les binaires gc), Zorya implémente un mécanisme de superposition.
- Lorsqu'une branche conditionnelle implique des variables symboliques suivies, une superposition légère est créée pour le chemin non pris. Les lectures consultent d'abord la superposition, avec retour à l'état de base en cas d'échec ; les écritures vont exclusivement vers la superposition.
- Cette superposition exécute un nombre borné d'instructions (par défaut $N=15$ ) avant d'être jetée, permettant la détection de vulnérabilités sur des chemins non empruntés par la trace concrète.
Détection de Vulnérabilités via une Routine d'Analyse :
- Le framework exécute des instructions avec des valeurs concrètes (issues du dump gdb) et des expressions symboliques (gérées par le solveur SMT Z3).
- Une « Routine d'Analyse » vérifie la présence de motifs de vulnérabilité à chaque instruction, incluant les déréférencements de pointeurs nuls, les débordements d'entiers et les divisions par zéro.
- Pour les binaires gc, le système exploite à la fois l'exploration AST (pour localiser les appels explicites de panic) et l'exécution par superposition (pour détecter les vulnérabilités silencieuses qui ne déclenchent pas de panics d'exécution).

Contributions Clés

Extension aux Binaires gc : Le framework est étendu pour analyser les binaires multithread produits par le compilateur Go standard, comblant le fossé entre les outils de recherche et les logiciels Go de production.
Jeu de Données de Vulnérabilités Réelles : Les auteurs ont constitué un corpus de 11 vulnérabilités réelles issues de projets de production (incluant Kubernetes, Go-Ethereum et CoreDNS), complet avec des workflows de reproduction et des entrées déclencheuses.
Évaluation Comparative : Zorya a été évalué face à sept outils de l'état de l'art (trois analyseurs statiques, deux fuzzeurs et deux exécuteurs symboliques au niveau binaire).
Détection de Vulnérabilités Silencieuses : Le framework détecte avec succès des vulnérabilités qui ne déclenchent pas de panics d'exécution, spécifiquement les débordements d'entiers silencieux, sans nécessiter d'oracles écrits manuellement.

Résultats

L'évaluation a été menée sur 11 vulnérabilités réelles réparties en trois catégories : déréférencements de pointeurs nuls, débordements d'entiers et index hors limites.

Taux de Détection : Zorya a détecté 7 vulnérabilités sur 11.
- 4 ont été capturées par la Routine d'Analyse sur le chemin concret (emprunté).
- 3 ont été identifiées via la réachabilité de panic par AST sur la branche non prise.
- 2 découvertes secondaires ont été mises en évidence par l'exécution par superposition sur des chemins non empruntés (détectées dans la limite de profondeur de 15 instructions).
Détection Unique : Zorya était le seul outil à détecter un débordement d'entier silencieux dans la fonction memoryGasCost de Go-Ethereum (v1.6.0). Ce bug implique une multiplication qui déborde silencieusement dans l'arithmétique sans signe de Go, permettant à un attaquant d'allouer une mémoire massive pour un gaz quasi nul. Aucun autre outil évalué n'a trouvé ce bug sans un oracle écrit manuellement.
Comparaison des Outils :
- Analyseurs Statiques (staticcheck, gosec, nilaway) : Ont détecté 0 des 11 bugs. gosec a manqué les débordements arithmétiques de même type, et nilaway a échoué sur les packages Kubernetes en raison de problèmes de résolution de dépendances.
- Fuzzeurs (go test -fuzz, GoLibAFL) : Ont détecté 5 des 11 bugs (incluant kube-sm-2025, que Zorya a manqué en raison de l'épuisement des ressources lors de l'exécution symbolique de runtime.memmove). Les fuzzeurs étaient plus rapides (en moyenne ~0,18s à 7s) mais nécessitaient des harnesses écrits manuellement et manquaient les vulnérabilités silencieuses qui ne provoquent pas d'arrêt.
- Autres Exécuteurs Symboliques (BINSEC, SymQEMU) : Ont détecté 0 des 11 bugs, principalement en raison d'un manque de support pour les primitives d'exécution Go.
Performance : Zorya a nécessité en moyenne 16,5 minutes par détection, nettement plus lent que les fuzzeurs, mais fournit une trace d'exécution complète au niveau instruction et fonctionne entièrement automatiquement sans harnesses.

Importance et Revendications

L'article revendique que Zorya comble une lacune critique dans le paysage de la sécurité Go. Alors que les analyseurs statiques échouent à raisonner sur l'arithmétique et l'aliasing spécifiques au programme, et que les fuzzeurs nécessitent des harnesses manuels et manquent les bugs non plantants, Zorya offre une analyse binaire entièrement automatique capable de détecter des vulnérabilités silencieuses.

Les auteurs positionnent Zorya comme un outil combinant une exploration fine par superposition, une récupération d'état initial multithread et une détection de débordements silencieux spécifiquement pour les binaires Go. Le travail démontre que l'exécution concolique peut être adaptée à l'environnement d'exécution complexe et multithread du compilateur Go standard, permettant la détection de vulnérabilités (telles que les débordements d'entiers silencieux) invisibles pour les autres outils évalués. L'article conclut que, bien que Zorya soit plus lent que le fuzzing, sa capacité à fournir des traces d'instructions exactes et à détecter des bugs non plantants en fait un ajout précieux à la boîte à outils de l'ingénierie de sécurité logicielle.