Aproximación, corrección e indecidibilidad

Fundamentos · Actualizado el 16 de agosto de 2026

Ningún analizador estático dice la verdad. Todos mienten, y la única pregunta que importa es en qué dirección. Este capítulo fija el vocabulario —sound, complete, sobreaproximación, falso positivo— que se usa a partir de aquí, y explica por qué la aproximación no es una limitación de las herramientas actuales sino un teorema.

2.1 La naturaleza de la aproximación

Una definición razonablemente precisa de la disciplina:

Las tres palabras clave son seguras, computables y aproximaciones. Ninguna sobra. Una aproximación que no sea computable es inútil por definición. Una que no sea segura es peor que inútil: engaña. Y tiene que ser aproximación, porque la respuesta exacta no es computable.

La imagen mental es esta. Existe una respuesta verdadera: el conjunto exacto de valores, o comportamientos, o estados, que el programa puede exhibir en ese punto. Ese conjunto no es calculable. Lo que el análisis calcula es un conjunto mayor, que contiene al verdadero y además algo de sobra:

   respuesta verdadera
   +---------------------+--------------------------+
   | { d1, ..., dn }     |  { dn+1, ..., dN }       |
   |                     |    /                     |
   |                     |   /                      |
   |                     |  /                       |
   +---------------------+-/------------------------+
   | { d1, ..., dn, ..., dn+m }                     |
   +------------------------------------------------+
   respuesta segura

La naturaleza de la aproximación: errar hacia el lado seguro. El conjunto calculado contiene el verdadero y algún elemento espurio de más.

Los elementos d₁ a d_n son los que realmente pueden ocurrir. Los que van de d_n+1 a d_N no ocurren nunca. El análisis devuelve d₁ a d_n+m: acierta con todos los verdaderos y se cuela con m espurios. El reto de ingeniería es que m sea pequeño sin que el análisis se vuelva impracticable —porque si el analizador devuelve siempre el conjunto entero {d₁, ..., d_N}, es formalmente seguro y absolutamente inútil.

2.2 Un ejemplo mínimo

Considérese este programa, donde S es un fragmento cualquiera que no contiene ninguna asignación a y:

read(x); (if x > 0 then y := 1 else (y := 2; S)); z := y

Pregunta: ¿qué valores de y pueden alcanzar la asignación z := y?

Intuitivamente, 1 o 2. Pero supóngase que S no termina nunca cuando x ≤ 0. Entonces la rama del else nunca llega al final, y el único valor que alcanza z := y es el 1. Es decir: la respuesta verdadera es {1}.

Ahora bien, decidir si S termina es indecidible. Así que un análisis realista no puede detectar esa situación, y responderá {1, 2}. Es una respuesta segura: contiene la verdadera. No es exacta, pero no engaña.

Obsérvese la asimetría. Si un análisis respondiera {1} sin poder demostrar que S diverge, estaría mintiendo por defecto: afirmaría que el 2 no llega, y un optimizador que se lo creyera podría eliminar la rama del else y cambiar el significado del programa. Responder de más es prudente; responder de menos es peligroso. En eso consiste «errar hacia el lado seguro».

En ingeniería inversa

Qué lado es el seguro depende de la pregunta

El párrafo anterior da por hecho que el lado seguro es «de más», pero eso sólo vale para preguntas del tipo ¿qué puede pasar?. Para preguntas del tipo ¿qué pasa siempre? el lado seguro es el contrario.

Ejemplo concreto en ingeniería inversa. «¿A qué direcciones puede saltar este jmp rax?» es una pregunta puede: la respuesta segura es un superconjunto, porque si falta un destino el CFG queda incompleto y el analista no ve código que sí se ejecuta. En cambio, «¿qué registros están garantizadamente muertos aquí?» es una pregunta siempre: la respuesta segura es un subconjunto, porque si sobra un registro se eliminará como muerto código que hacía falta.

Las dos familias se llaman análisis may y análisis must, y la diferencia se materializa en qué operación del retículo se usa al fusionar caminos: unión para may, intersección para must. El capítulo «6» lo formaliza. Cuando una herramienta de RE le enseñe un conjunto, la primera pregunta es siempre: ¿esto es un may o un must?

2.3 Soundness y completeness

Formalicemos. Sea P una propiedad de programas —«esta variable es constante», «este puntero no es nulo», «este registro está vivo»— y sea A un analizador que responde sí o no.

A es sound (correcto, a veces seguro) si todo lo que afirma es cierto en la dirección que le importa a la aplicación.
A es complete (completo) si detecta todos los casos en que la propiedad se da.

El problema es que «en la dirección que le importa a la aplicación» convierte la palabra sound en un término ambiguo, y es la fuente de la mitad de los malentendidos de esta disciplina. Concretémoslo con las dos aplicaciones más habituales.

Una herramienta de verificación busca demostrar la ausencia de errores. Se la llama sound si nunca se le escapa un error de los tipos que fue diseñada para detectar; a cambio, se le permite producir avisos espurios, llamados falsos positivos (false positives). Un verificador sound que avisa de 900 problemas de los cuales 3 son reales sigue siendo sound.

Una herramienta de pruebas automáticas busca encontrar errores reales. Se la llama sound si todo error que reporta es genuino; a cambio, se le permite que se le escapen errores, llamados falsos negativos (false negatives).

Son dos usos opuestos de la misma palabra. La forma de no perderse es olvidar el término y preguntar siempre: ¿qué lado del error garantiza esta herramienta que no comete?

	El análisis dice «sí»	El análisis dice «no/quizá»
La propiedad se cumple	verdadero positivo	falso negativo (se escapa)
La propiedad no se cumple	falso positivo (ruido)	verdadero negativo

Un análisis que sobreaproxima el conjunto de comportamientos elimina los falsos negativos y admite falsos positivos. Uno que infraaproxima hace lo contrario. Y un análisis exacto —sin ninguno de los dos— no existe, por el teorema de Rice.

Formalización

Corrección respecto de la semántica

La formulación precisa requiere fijar antes una semántica. Sea ⟦P⟧ ⊆ Σ el conjunto de estados alcanzables del programa P sobre el dominio concreto ℘(Σ), y sea L el dominio abstracto del análisis, con una función de concretización γ : L → ℘(Σ) que asigna a cada valor abstracto el conjunto de estados concretos que representa.

El resultado del análisis, a ∈ L, es correcto (sound) si

⟦P⟧ ⊆ γ(a)

y es completo si además γ(a) ⊆ ⟦P⟧, es decir, γ(a) = ⟦P⟧. Un análisis se dice óptimo dentro de su dominio abstracto si devuelve el menor a ∈ L que satisface la condición de corrección; nótese que eso no lo hace completo, porque el dominio abstracto puede sencillamente carecer de un elemento que describa ⟦P⟧ exactamente.

Esta distinción entre falta de completitud por el dominio y falta de completitud por el algoritmo es central y se desarrolla en el capítulo «21», junto con las conexiones de Galois que relacionan γ con su adjunta α.

2.4 La indecidibilidad no se reduce al problema de la parada

En el capítulo «1» se vio que decidir si una variable tiene valor constante permite decidir el problema de la parada. Podría pensarse que la parada es el único obstáculo, y que restringiéndonos a programas que siempre terminan tendríamos análisis exactos. No es así, y el resultado es notablemente fuerte:

Es imposible construir un análisis estático que decida si un programa dado puede fallar al ejecutarse, incluso si sólo se exige que funcione con programas que terminan con toda entrada. Dicho de otro modo: la aproximación es inevitable, no un efecto colateral de la no terminación.

Formalización

Demostración por diagonalización

Modelemos los programas como máquinas de Turing deterministas, y el fallo mediante un estado especial fail. Con una entrada dada, una máquina termina en su estado accept (intuitivamente, «sí»), en reject («no»), en fail (se ha violado la condición de corrección), o diverge. Una máquina es correcta si su estado fail es inalcanzable.

Supongamos que existe un programa P capaz de decidir si una máquina de Turing total dada es correcta. (Si la entrada no es total, la salida de P no está especificada: sólo le exigimos que acierte con las máquinas que siempre paran.) P termina en accept si y sólo si la máquina dada es correcta, y en reject en caso contrario.

Si P existe, podemos construir otra máquina M que toma la codificación e(T) de una máquina T y construye la codificación e(S_T) de una tercera máquina S_T definida así: S_T es esencialmente una máquina universal especializada en simular T sobre la entrada e(T). Sea w la entrada de S_T. Entonces S_T simula T sobre e(T) durante como mucho |w| movimientos. Si la simulación acaba en el estado accept de T, S_T pasa a su estado fail; se construye de modo que esa sea la única forma de alcanzarlo. Si la simulación no acaba en accept —porque se agotaron los |w| movimientos, o porque T llegó a reject o a fail— entonces S_T pasa a accept o a reject, da igual cuál.

Obsérvese que S_T nunca diverge, y que alcanza fail si y sólo si T acepta la entrada e(T) en como mucho |w| movimientos. Construido e(S_T), la máquina M se lo pasa a P; si P acepta, M acepta, y si P rechaza, M rechaza.

                         M
               +-------------------+       +-------+
     e(T) ---->| construir e(S_T)  |------>|   P   |----> accept
               |     desde e(T)    | e(S_T)|       |----> reject
               +-------------------+       +-------+

Preguntemos ahora: ¿acepta M la entrada e(M)? Es decir, ¿qué pasa con T = M?

Si M acepta e(M), entonces P aceptó e(S_T), luego S_T es correcta y su estado fail es inalcanzable: para toda entrada w, por larga que sea, S_T no llega a fail. Eso significa que T no acepta e(T). Pero T = M, lo que contradice que M acepte e(M).

Recíprocamente, si M rechaza e(M), entonces P rechazó e(S_T), luego el estado fail de S_T es alcanzable para alguna entrada v. Luego existe algún w tal que fail se alcanza en |w| pasos con la entrada v, luego T acepta e(T), y otra vez tenemos contradicción.

Por construcción M termina en accept o en reject con cualquier entrada, pero ninguna de las dos es posible con la entrada e(M). Conclusión: el analizador de corrección ideal P no puede existir. ∎

El corolario práctico, para quien hace ingeniería inversa, es que no hay ninguna herramienta futura que vaya a resolver esto. La imprecisión de Ghidra o de Hex-Rays no es un defecto de implementación que se arregle en la próxima versión: es la manifestación de un límite matemático. Lo que sí mejora versión a versión es el tamaño de m, el margen de sobra.

2.5 Por qué las herramientas reales mienten a propósito

Hasta aquí, la teoría. En la práctica ocurre algo que conviene saber: los analizadores de lenguajes reales recortan por lo sano, sacrificando la corrección para ganar precisión y rendimiento. Es una decisión de ingeniería consciente y muy extendida —el modelado de la reflexión en Java es el ejemplo canónico— y significa que la garantía formal del capítulo anterior no siempre se sostiene en el producto que uno tiene delante.

En el análisis de binarios los recortes son aún más agresivos, porque el modelo del que se parte es más pobre. La siguiente lista no es exhaustiva, pero cubre las suposiciones que rompen con más frecuencia:

Suposición habitual de la herramienta	Cuándo falla
El código no se automodifica	Empaquetadores, descifrado en tiempo de ejecución, JIT
Las instrucciones no se solapan	Ofuscación por desalineamiento; instrucciones que empiezan a mitad de otra
Las llamadas retornan a la instrucción siguiente	`call`/`pop` para obtener el PC, retornos manipulados, ROP
Se respeta el convenio de llamada	Código ensamblado a mano, funciones internas del compilador, tail calls
Todo salto indirecto va a un destino del binario	Punteros a función calculados, trampolines, hooking
Los datos y el código están separados	Constantes embebidas en el flujo de instrucciones (habitual en ARM)
La pila crece de forma disciplinada	`alloca` de tamaño variable, cambios de pila, corrutinas

En ingeniería inversa

Cómo detectar que su decompilador se ha rendido

Las herramientas no suelen anunciar cuándo dejan de ser correctas, pero dejan pistas. Un pseudocódigo con muchas variables sin usar y asignaciones aparentemente redundantes suele indicar que el análisis de alias se ha desbordado y ha optado por no propagar nada. Un switch que el decompilador no reconoce y deja como salto indirecto significa que el análisis de valores no acotó el índice. Cuando Hex-Rays inserta __asm o deja fragmentos sin decompilar, está declarando explícitamente su rendición; cuando muestra una llamada a sub_401000 con cero argumentos y usted ve que recibe tres, es que el análisis de convenio de llamada falló en silencio, y ese es el caso peligroso.

Regla práctica: desconfíe especialmente de los resultados negativos de una herramienta —«este puntero nunca es nulo», «este bloque es inalcanzable»— porque para afirmarlos hay que haber demostrado algo, y la mayoría de herramientas de RE no distinguen entre «he demostrado que no» y «no he encontrado que sí».

2.6 Precisión, coste y el retículo de compromisos

Si todos los análisis correctos sobreaproximan, la pregunta pasa a ser cuánto. Un análisis A₁ es más preciso que A₂ si para todo programa el resultado de A₁ está contenido en el de A₂. En términos del retículo de valores abstractos, a₁ ⊑ a₂: más abajo es más preciso.

Las cuatro palancas clásicas para ganar precisión, todas ellas con coste, son las que estructuran el bloque de análisis de flujo de datos:

Sensibilidad al flujo (flow sensitivity): distinguir el estado en cada punto del programa en lugar de calcular un único resumen por función. Es la diferencia entre saber que p es nulo en la línea 12 y saber que p es nulo en algún sitio.
Sensibilidad al contexto (context sensitivity): distinguir las distintas invocaciones de una misma función. Capítulo «10».
Sensibilidad al camino (path sensitivity): distinguir según qué condiciones se cumplieron para llegar a un punto. Capítulo «9».
Riqueza del dominio abstracto: pasar de signos a intervalos, de intervalos a poliedros. Capítulos «8» y «21».

Cada palanca multiplica el coste, y ninguna es gratis en precisión: es perfectamente posible diseñar un análisis sensible al contexto que sea menos preciso que uno insensible, si el dominio abstracto es pobre. La combinación es un arte, y el capítulo «21» da el marco para razonar sobre ella con rigor.

Formalización

Un análisis más preciso no es necesariamente mejor

Sea A un análisis de propagación de constantes sobre el retículo plano de enteros, y A' el mismo análisis pero con sensibilidad al camino. A' es al menos tan preciso como A en todo programa. Sin embargo, si el coste de A es lineal en el tamaño del programa y el de A' es exponencial en el número de condicionales, A' es inaplicable a un binario de tamaño real.

El criterio operativo no es la precisión absoluta sino la precisión alcanzable dentro de un presupuesto, y ese criterio no induce un orden total: dos análisis pueden ser incomparables porque cada uno es más preciso que el otro en distintas familias de programas. Por eso los analizadores industriales combinan varios análisis baratos en cascada en lugar de uno caro.

2.7 Lecturas

La corrección respecto de la semántica, que el recuadro de formalización solo enuncia, se desarrolla en el capítulo «21».

El teorema de Rice (1953) es la referencia canónica sobre indecidibilidad de propiedades semánticas. La distinción entre propiedades de seguridad (safety) y de viveza (liveness), que aquí se ha esquivado restringiéndonos a las primeras, se trata en la literatura de verificación de modelos.