nathan-luevano/silicaValidación diferencial exhaustiva de todas las codificaciones de instrucciones AArch64 de 4.3B.
Un mapa completo de dónde los decodificadores AArch64 discrepan de la arquitectura.
Silica recorre cada una de las 4.294.967.296 posibles palabras de instrucción A64, compara Capstone, LLVM y Unicorn con la especificación legible por máquina de Arm, y convierte las diferencias en evidencia reproducible.
Que un desensamblador diga "válido" es fácil. Saber si tiene razón es más difícil. La mayoría de las pruebas diferenciales pueden revelar que las herramientas discrepan, pero no pueden identificar la respuesta correcta sin un oráculo independiente. Silica usa la versión XML de Arm como ese oráculo.
A64 hace posible un experimento inusualmente exhaustivo: las instrucciones tienen exactamente 32 bits de ancho, por lo que todo el espacio de codificación es finito y práctico de enumerar. Silica aprovecha esa propiedad. Los resultados de validez a continuación no son una estimación ni una campaña de fuzzing; se comprobó cada palabra posible.
Estos resultados usan ISA_A64_xml_A_profile-2026-06_mc (Armv9.6-A). El barrido se
dividió en 256 fragmentos verificados de forma independiente que cubren las 2³² codificaciones.
| Resultado | Recuento | Proporción del espacio total |
|---|---|---|
| Asignadas por la especificación de Arm | 1.799.435.776 | 41,9% |
| No asignadas por la especificación de Arm | 2.495.531.520 | 58,1% |
| Discrepancias de validez encontradas | 723.801.678 | 16,9% |
| Reproducciones mínimas listas para upstream | 10 | — |
Concordancia con la especificación sobre si una codificación es válida:
| Decodificador | Concordancia | Visual |
|---|---|---|
| Capstone | 84,8% | █████████████████████████░░░░░ |
| LLVM | 87,6% | ██████████████████████████░░░░ |
| Unicorn | 88,3% | ██████████████████████████░░░░ |
La gran brecha de validez tiene causas identificables. Unicorn comprueba la validez
ejecutando una instrucción y observando las trampas, mientras que los otros oráculos decodifican
sin ejecución. Un pequeño número de regiones también se ve afectado por condiciones
UNDEFINED en tiempo de decodificación que el oráculo de especificación compilado no evalúa.
Silica registra estas limitaciones en lugar de suavizarlas en el resultado.
Comparar mnemónicos y operandos renderizados es mucho más costoso que registrar un bit de validez. Por lo tanto, Silica evalúa el texto sobre una muestra determinista de 1.000.000 de palabras extraídas de 1.266.064.016 candidatas donde los cuatro oráculos consideran válida la codificación. Este es un resultado muestreado y se mantiene deliberadamente separado de las cifras exhaustivas de validez.
| Clasificación dentro de la muestra | Registros | Proporción |
|---|---|---|
| El renderizado de operandos difiere | 862.648 | 86,3% |
| La normalización necesita revisión | 137.352 | 13,7% |
La muestra es útil para localizar trabajo de normalización y presentación; no pretende una cobertura exhaustiva de todos los renderizados textuales.
El motor de barrido produce un gran conjunto de datos de investigación. silica-scope es la aplicación de terminal complementaria para hacer accesible ese conjunto de datos. Abre un directorio de artefactos de Silica terminado y te permite explorar las métricas principales, inspeccionar el mapa de codificación de 256 fragmentos, filtrar discrepancias, buscar cualquier palabra de 32 bits y leer las reproducciones listas para presentación.
Instálalo desde PyPI con Python 3.11 o superior:
pipx install silica-scope
Luego ejecútalo desde un checkout de Silica o apúntalo a un directorio de artefactos:
silica-scope
silica-scope /path/to/silica/artifacts
silica-scope --report
silica-scope es un lector de Python puro sin dependencias de decodificadores nativos. No
lanza el barrido exhaustivo y maneja con elegancia el conjunto de artefactos publicados más pequeño del repositorio.
Consulta la guía del lector de terminal
para conocer los paneles, los controles de teclado y las opciones de descubrimiento de artefactos.
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"]La ruta de alto volumen está escrita en Rust y llama a cada decodificador en proceso. Almacena un bit por codificación por oráculo, lo que mantiene compacta la comparación exhaustiva y hace que la discrepancia sea una operación directa de mapas de bits. Los fallos se bisecan hasta la palabra de instrucción exacta.
Python se encarga de la compilación de la especificación, la normalización, la generación de informes y la capa de verificación independiente. Los esquemas de artefactos, las reglas de muestreo y las limitaciones conocidas están documentados en docs/formats.md.
Crea el entorno fijado y comprueba que las entradas locales requeridas estén disponibles:
micromamba create -y -p ./.venv -f environment.yml
micromamba run -p ./.venv silica doctor
La especificación XML de Arm no se incluye en el repositorio debido a su licencia. silica doctor
informa dónde espera Silica encontrarla y cualquier otro requisito previo faltante.
Para ejecutar el pipeline completo desde un checkout preparado:
make all
Este es un barrido completo de 2³², no una prueba rápida de humo. Produce el oráculo compilado, los registros de fragmentos, los mapas de bits de validez, el corpus de discrepancias, las métricas publicadas, las reproducciones y un hash de resultado SHA-256 estable.
Siete verificadores independientes recalculan las afirmaciones del proyecto a partir de artefactos sin procesar. No confían en un resumen generado, y cada verificador tiene un fixture que demuestra que detecta el defecto contra el que protege. No hay ningún estado omitido o provisional.
micromamba run -p ./.venv silica verify
Las versiones fijadas de los decodificadores y un hash de resultado recalculado recientemente hacen que ejecuciones separadas sean comparables. Los objetivos de verificación y su estado actual se registran en GOALS.yml.
Silica actualmente cubre la decodificación de A64 base y Advanced SIMD. SVE, SVE2, SME, A32/T32, RISC-V, los ciclos de ida y vuelta del ensamblador y las pruebas generales de ejecución quedan fuera del estudio v1.
La inspiración más cercana es Sandsifter, que explora el espacio de instrucciones de longitud variable de x86. Silica aplica el mismo espíritu de escepticismo sistemático a AArch64, donde las codificaciones de ancho fijo y una especificación independiente permiten una comparación completa y adjudicada.
Apache 2.0 — consulta LICENSE