nathan-luevano/silicaValidation différentielle exhaustive de tous les 4,3 milliards d'encodages d'instructions AArch64.
Une cartographie complète des divergences entre les décodeurs AArch64 et l'architecture.
Silica parcourt la totalité des 4 294 967 296 mots d'instruction A64 possibles, compare Capstone, LLVM et Unicorn avec la spécification lisible par machine d'Arm, et transforme les différences en preuves reproductibles.
Qu'un désassembleur déclare « valide » est facile. Savoir s'il a raison est plus difficile. La plupart des tests différentiels peuvent révéler que des outils sont en désaccord, mais ils ne peuvent pas identifier la bonne réponse sans un oracle indépendant. Silica utilise la publication XML d'Arm comme cet oracle.
A64 rend possible une expérience inhabituellement exhaustive : les instructions font exactement 32 bits de large, donc l'espace d'encodage entier est fini et praticable à énumérer. Silica tire parti de cette propriété. Les résultats de validité ci-dessous ne sont pas une estimation ni une campagne de fuzzing ; chaque mot possible a été vérifié.
Ces résultats utilisent ISA_A64_xml_A_profile-2026-06_mc (Armv9.6-A). Le balayage a été
divisé en 256 fragments vérifiés indépendamment couvrant les 2³² encodages.
| Résultat | Nombre | Part de l'espace total |
|---|---|---|
| Alloué par la spécification Arm | 1 799 435 776 | 41,9 % |
| Non alloué par la spécification Arm | 2 495 531 520 | 58,1 % |
| Désaccords de validité trouvés | 723 801 678 | 16,9 % |
| Reproducteurs minimaux prêts pour l'amont | 10 | — |
Concordance avec la spécification sur la validité d'un encodage :
| Décodeur | Concordance | Visuel |
|---|---|---|
| Capstone | 84,8 % | █████████████████████████░░░░░ |
| LLVM | 87,6 % | ██████████████████████████░░░░ |
| Unicorn | 88,3 % | ██████████████████████████░░░░ |
Le large écart de validité a des causes identifiables. Unicorn teste la validité en
exécutant une instruction et en observant les pièges, tandis que les autres oracles décodent
sans exécution. Un petit nombre de régions sont également affectées par des conditions
UNDEFINED au moment du décodage que l'oracle de spécification compilé n'évalue pas.
Silica consigne ces limitations au lieu de les lisser hors du résultat.
Comparer les mnémoniques et opérandes rendus est bien plus coûteux que d'enregistrer un bit de validité. Silica évalue donc le texte sur un échantillon déterministe de 1 000 000 de mots tirés de 1 266 064 016 candidats où les quatre oracles considèrent l'encodage comme valide. Il s'agit d'un résultat échantillonné, délibérément tenu séparé des chiffres de validité exhaustifs.
| Classification au sein de l'échantillon | Enregistrements | Part |
|---|---|---|
| Rendu des opérandes différent | 862 648 | 86,3 % |
| Normalisation à examiner | 137 352 | 13,7 % |
L'échantillon est utile pour localiser le travail de normalisation et de présentation ; il ne prétend pas couvrir de manière exhaustive chaque rendu textuel.
Le moteur de balayage produit un vaste jeu de données de recherche. silica-scope est l'application terminale compagnon qui rend ce jeu de données accessible. Elle ouvre un répertoire d'artefacts Silica terminé et vous permet de parcourir les métriques principales, inspecter la carte d'encodage en 256 fragments, filtrer les désaccords, rechercher n'importe quel mot de 32 bits et lire les reproducteurs prêts à être signalés.
Installez-la depuis PyPI avec Python 3.11 ou plus récent :
pipx install silica-scope
Puis lancez-la depuis un checkout de Silica ou pointez-la vers un répertoire d'artefacts :
silica-scope
silica-scope /path/to/silica/artifacts
silica-scope --report
silica-scope est un lecteur en Python pur sans dépendances de décodeur natif. Elle
ne lance pas le balayage exhaustif et gère avec souplesse le plus petit ensemble d'artefacts
publié du dépôt. Consultez le guide du lecteur terminal
pour les panneaux, les commandes clavier et les options de découverte des artefacts.
flowchart LR
XML["Arm XML specification"] --> SPEC["compiled spec oracle"]
SPEC --> SWEEP["parallel 32-bit sweep"]
CAP["Capstone"] --> SWEEP
LLVM["LLVM"] --> SWEEP
UNI["Unicorn"] --> SWEEP
SWEEP --> MAP["validity bitmaps"]
MAP --> DIFF["exhaustive XOR comparison"]
DIFF --> CORPUS["classified disagreement corpus"]
CORPUS --> OUT["metrics · reproducers · result hash"]Le chemin à haut volume est écrit en Rust et appelle chaque décodeur en cours de processus. Il stocke un bit par encodage et par oracle, ce qui garde la comparaison exhaustive compacte et fait du désaccord une opération directe sur les bitmaps. Les plantages sont bisectés jusqu'au mot d'instruction exact.
Python gère la compilation de la spécification, la normalisation, le reporting et la couche de vérification indépendante. Les schémas d'artefacts, les règles d'échantillonnage et les limitations connues sont documentés dans docs/formats.md.
Créez l'environnement épinglé et vérifiez que les entrées locales requises sont disponibles :
micromamba create -y -p ./.venv -f environment.yml
micromamba run -p ./.venv silica doctor
La spécification XML d'Arm n'est pas vendue avec le projet en raison de sa licence. silica doctor
signale où Silica s'attend à la trouver et tout autre prérequis manquant.
Pour exécuter le pipeline complet depuis un checkout préparé :
make all
Il s'agit d'un balayage complet des 2³², pas d'un test de fumée rapide. Il produit l'oracle compilé, les enregistrements de fragments, les bitmaps de validité, le corpus de désaccords, les métriques publiées, les reproducteurs et un hash de résultat SHA-256 stable.
Sept vérificateurs indépendants recalculent les affirmations du projet à partir des artefacts bruts. Ils ne font pas confiance à un résumé généré, et chaque vérificateur dispose d'un fixture prouvant qu'il détecte le défaut contre lequel il protège. Il n'y a aucun état ignoré ou provisoire.
micromamba run -p ./.venv silica verify
Des versions de décodeurs épinglées et un hash de résultat recalculé à neuf rendent les exécutions séparées comparables. Les objectifs de vérification et leur statut actuel sont consignés dans GOALS.yml.
Silica couvre actuellement le décodage A64 de base et Advanced SIMD. SVE, SVE2, SME, A32/T32, RISC-V, les allers-retours d'assembleur et les tests d'exécution généraux sont hors du périmètre de l'étude v1.
L'inspiration la plus proche est Sandsifter, qui explore l'espace d'instructions à longueur variable de x86. Silica applique le même esprit de scepticisme systématique à AArch64, où les encodages à largeur fixe et une spécification indépendante permettent une comparaison complète et arbitrée.
Apache 2.0 — voir LICENSE