Por qué el análisis estático es el motor de la ingeniería inversa

El análisis estático de programas pretende responder automáticamente a preguntas sobre los comportamientos posibles de un programa, sin ejecutarlo. Esa definición, tal cual, describe también lo que hace un ingeniero inverso delante de un binario. Este capítulo explica por qué no es una coincidencia.

1.1 Tres comunidades, la misma pregunta

El análisis estático se lleva usando desde principios de los años sesenta en compiladores optimizadores. Más recientemente ha demostrado su utilidad en herramientas de búsqueda de errores y verificación, y en los entornos de desarrollo, para asistir al programador. Tres comunidades, tres motivaciones distintas, y en el fondo la misma operación: calcular una aproximación segura del conjunto de estados que el programa puede alcanzar.

El ingeniero inverso es la cuarta comunidad, y llegó la última. Su motivación es distinta —no quiere optimizar, ni verificar, ni autocompletar: quiere entender— pero el instrumento es idéntico. Cuando Hex-Rays decide que una variable local de la pila es un int con signo, está resolviendo un sistema de restricciones de tipos. Cuando Ghidra colapsa quince bloques básicos en un switch, está calculando dominadores y fronteras de dominancia. Cuando angr descarta una rama como inalcanzable, está haciendo propagación de constantes con sensibilidad al camino.

La diferencia práctica entre las cuatro comunidades no está en la teoría, sino en el punto de partida. El compilador parte de un árbol sintáctico con tipos, nombres y estructura de bloques. El ingeniero inverso parte de un vector de bytes.

1.2 Lo que el compilador destruye

Merece la pena hacer inventario, porque ese inventario es la lista de tareas de la ingeniería inversa, y cada línea de la lista se corresponde con un capítulo de los que siguen.

Tomemos un programa mínimo: el factorial. Lo escribiremos en el lenguaje WHILE, un lenguaje imperativo de juguete que usaremos repetidamente y que se define con precisión en el capítulo «3». Cada construcción elemental lleva una etiqueta (label) en superíndice, que identifica un punto del programa:

[y := x]¹;
[z := 1]²;
while [y > 1]³ do (
    [z := z * y]⁴;
    [y := y - 1]⁵
);
[y := 0]⁶

Al terminar, z contiene el factorial del valor inicial de x. La última asignación, [y := 0]6, no aporta nada al resultado: está ahí precisamente para tener un ejemplo de código muerto.

Compilemos esto a x86-64 con optimización moderada. Un resultado típico:

factorial:
        mov     eax, 1              ; z := 1
        cmp     edi, 1
        jle     .Ldone
.Lloop:
        imul    eax, edi            ; z := z * y
        dec     edi                 ; y := y - 1
        cmp     edi, 1
        jg      .Lloop
.Ldone:
        ret

Compárense los dos. En diez líneas de ensamblador se ha perdido lo siguiente:

• Los nombres. x, y y z ya no existen. Hay edi y eax, que además son el mismo almacenamiento reutilizado para cosas distintas en otros puntos del programa.
• La identidad de las variables. y y el parámetro x comparten registro: la asignación [y := x]1 se ha implementado como «no hacer nada». Dos variables del fuente son un solo registro en el binario, y sólo el análisis puede volver a separarlas. Esto es exactamente el problema que resuelve la forma SSA (capítulo «12»).
• La estructura de control. El while ha desaparecido. Lo que queda es un salto condicional hacia atrás y un test de guarda duplicado antes de entrar. Reconstruir el while a partir del grafo de saltos requiere análisis de dominadores y detección de bucles naturales (capítulo «4»).
• Los tipos. eax es 32 bits. ¿Con signo o sin signo? ¿Un entero, un booleano, un enum, el byte bajo de un puntero? El ensamblador no lo dice; sólo lo dice el uso que se hace del valor, y deducirlo es inferencia de tipos (capítulo «19»).
• El código muerto. [y := 0]6 no aparece en el binario. El compilador demostró que era código muerto —usando análisis de variables vivas, capítulo «6»— y lo eliminó.
• Las fronteras. Dónde empieza y acaba una función, qué es código y qué es dato, qué bloques pertenecen a qué función. En un binario con saltos indirectos, incluso esto es un resultado de análisis, no un hecho (capítulo «3»).

1.3 Las preguntas del optimizador

Los compiladores optimizadores —incluidos los compiladores JIT dentro de intérpretes— necesitan conocer muchas propiedades del programa que están compilando para generar código eficiente. Algunos ejemplos de esas propiedades:

• ¿Contiene el programa código muerto? Más concretamente, ¿es la función f inalcanzable desde main? Si lo es, se puede reducir el tamaño del código.
• ¿El valor de cierta expresión dentro de un bucle es el mismo en todas las iteraciones? Si lo es, la expresión puede sacarse fuera del bucle y evitar cálculos redundantes.
• ¿El valor de la variable x depende de la entrada del programa? Si no depende, puede precalcularse en tiempo de compilación.
• ¿Cuáles son las cotas inferior y superior de la variable entera x? La respuesta puede guiar la elección de la representación en tiempo de ejecución.
• ¿Apuntan p y q a estructuras de datos disjuntas en memoria? Eso puede habilitar el procesamiento en paralelo.

Obsérvese que las cinco preguntas tienen la misma forma: ¿es cierto que, en toda ejecución posible, ocurre P? Y en las cinco, una respuesta conservadora es útil: si el analizador no está seguro, el compilador simplemente no aplica la optimización y genera código correcto pero más lento.

1.4 Las preguntas del verificador

Las herramientas de análisis más exitosas diseñadas para detectar errores —o para verificar su ausencia— apuntan a propiedades de corrección genéricas, aplicables a la mayoría de programas escritos en un lenguaje dado. En lenguajes inseguros como C, esos errores llevan a veces a vulnerabilidades de seguridad críticas; en lenguajes más seguros como Java suelen ser menos graves, pero siguen provocando caídas. Ejemplos:

• ¿Existe alguna entrada que lleve a una desreferencia de puntero nulo, a una división por cero o a un desbordamiento aritmético?
• ¿Están todas las variables inicializadas antes de leerse?
• ¿Se accede siempre a los arrays dentro de sus límites?
• ¿Puede haber referencias colgantes, es decir, uso de punteros a memoria ya liberada?
• ¿Termina el programa con toda entrada?

Otras propiedades dependen de especificaciones que aporta el programador:

• ¿Se garantiza que todas las aserciones se cumplen?
• ¿Se llama siempre a hasNext antes de next, y a open antes de read? Muchas bibliotecas tienen propiedades de este tipo, llamadas de typestate.

Con el software web y móvil, las propiedades de flujo de información han pasado a ser importantísimas:

• ¿Pueden valores de entrada procedentes de usuarios no fiables llegar sin comprobación a operaciones del sistema de ficheros? Sería una violación de integridad.
• ¿Puede información secreta hacerse observable públicamente? Sería una violación de confidencialidad.

Estas dos últimas son, literalmente, el análisis de taint que se usa a diario en la búsqueda de vulnerabilidades sobre binarios. El capítulo «11» lo formaliza mediante el marco IFDS.

1.5 Las preguntas del ingeniero inverso

Ahora la lista que no aparece en ninguna de las tres fuentes. Cada pregunta típica de la ingeniería inversa es una instancia de un análisis clásico:

La tabla es, esencialmente, el índice de esta referencia leído desde el otro lado.

1.6 Los cuatro enfoques

Las técnicas de análisis estático se han desarrollado en comunidades distintas, con vocabularios distintos, y durante mucho tiempo pareció que eran cosas diferentes. El resultado que las unificó fue demostrar que son cuatro presentaciones del mismo contenido. Conviene tener el mapa desde el principio, aunque cada enfoque no se desarrolle hasta su capítulo.

Usaremos el factorial de la «sección 1.2 · Lo que el compilador destruye» y una pregunta concreta: para cada punto del programa, ¿qué asignaciones pueden haber determinado el valor actual de cada variable? Es el análisis de reaching definitions (definiciones que alcanzan), y es la base de la reconstrucción de dependencias de datos en cualquier decompilador.

El grafo de flujo del factorial:

        +-----------+
        | [y:=x]¹  |
        +-----+-----+
              |
              v
        +-----------+
        | [z:=1]²  |
        +-----+-----+
              |
              v
        +-----------+   no
   +--->| [y>1]³   |--------+
   |    +-----+-----+        |
   |          | si           v
   |          v        +-----------+
   |    +-----------+  | [y:=0]⁶  |
   |    | [z:=z*y]⁴|  +-----------+
   |    +-----+-----+
   |          |
   |          v
   |    +-----------+
   +----| [y:=y-1]⁵|
        +-----------+

Enfoque 1: análisis de flujo de datos (data flow analysis). Se plantea el programa como un grafo, se asocia a cada nodo una pareja de conjuntos —lo que entra y lo que sale— y se escribe un sistema de ecuaciones que los relaciona. Para el factorial, escribiendo RD por reaching definitions y representando cada definición como una pareja (variable, etiqueta):

La primera ecuación dice que a la entrada del test del bucle puede llegarse desde la inicialización o desde el final del cuerpo. La segunda dice que la asignación z := z*y mata (kill) todas las definiciones previas de z y genera (gen) una nueva. Resolviendo el sistema —doce ecuaciones para este programa— se obtiene la respuesta. El capítulo «6» desarrolla esto en general; el 7, cómo resolverlo eficientemente.

Enfoque 2: análisis basado en restricciones (constraint-based analysis). En lugar de igualdades, se extraen inclusiones:

Es la misma información, pero como sistema de restricciones que un solucionador genérico resuelve buscando la menor solución. La ventaja aparece cuando el flujo de control no se conoce de antemano —punteros a función, llamadas virtuales, closures— porque las restricciones pueden generarse sin haber construido antes el grafo. Es la vía natural para el análisis de flujo de control (capítulo «17») y el de punteros (capítulo «18»).

Enfoque 3: interpretación abstracta (abstract interpretation). En vez de partir de ecuaciones, se parte de la semántica del lenguaje y se la sustituye sistemáticamente por una semántica sobre valores abstractos, con una demostración de que la abstracción es correcta. Es el enfoque que responde a la pregunta «¿y cómo sé que mi análisis no miente?». Da la teoría de las funciones de abstracción α y concretización γ, de las conexiones de Galois, y de por qué widening funciona. Capítulo «21».

Enfoque 4: sistemas de tipos y efectos (type and effect systems). Se expresa la propiedad de interés como un sistema de tipos enriquecido y el análisis se convierte en inferencia de tipos. En lugar de recorrer un grafo, se derivan juicios de la forma Γ ⊢ S : τ & φ, donde φ describe los efectos que S puede provocar. Es el enfoque dominante en lenguajes funcionales, y el que subyace a los sistemas de recuperación de tipos de los decompiladores modernos. Capítulos «19» y «20».

1.7 La aproximación es inevitable

Hay que decirlo ya, aunque el capítulo «2» lo desarrolle: no existe el analizador perfecto. No por falta de ingenio, sino por un resultado de 1953. El teorema de Rice dice, informalmente, que toda pregunta interesante sobre el comportamiento de entrada/salida de programas escritos en un lenguaje Turing-completo es indecidible.

Esto se ve fácilmente en cualquier caso particular. Supongamos que existe un analizador que decide si una variable de un programa tiene valor constante en toda ejecución. Es decir, un programa A que toma como entrada un programa T, una de sus variables x y un valor k, y decide si el valor de x es siempre igual a k cuando se ejecuta T:

                    +------------------------------+
                    |  ¿Es el valor de la variable |----> si
    (T, x, k) ----->|  x siempre igual a k cuando  |
                    |  se ejecuta T ?              |----> no
                    +------------------------------+

Podríamos usar ese analizador para decidir también el problema de la parada, dándole como entrada el programa siguiente, donde TM(j) simula la j-ésima máquina de Turing sobre la entrada vacía:

x = 17; if (TM(j)) x = 18;

Aquí x tiene valor constante 17 si y sólo si la j-ésima máquina de Turing no para con la entrada vacía. Si el analizador hipotético A existiera, tendríamos un procedimiento de decisión para el problema de la parada, que se sabe imposible.

Esto parece desalentador, pero el resultado teórico no impide respuestas aproximadas. Aunque sea imposible construir un análisis que decida correctamente una propiedad para cualquier programa, sí es a menudo posible construir herramientas que den respuestas útiles para la mayoría de programas realistas. Como el analizador ideal no existe, siempre queda margen para construir aproximaciones más precisas: lo que se conoce jocosamente como el teorema del pleno empleo para los diseñadores de análisis estático.

El analizador realista tiene esta forma:

                    +------------------------------+
                    |  ¿Es el valor de la variable |----> si, con certeza
    (T, x, k) ----->|  x siempre igual a k cuando  |
                    |  se ejecuta T ?              |----> quizá, no lo sé
                    +------------------------------+

La solución trivial, por supuesto, es responder «quizá» siempre. De ahí que el reto de ingeniería sea responder «sí» tan a menudo como se pueda manteniendo un rendimiento razonable.

1.8 Un caso que lo ilustra todo

Considérese este programa en C, que consigue cometer casi todos los errores posibles con punteros:

int main(int argc, char *argv[]) {
    if (argc == 42) {
        char *p, *q;
        p = NULL;
        printf("%s", p);
        q = (char *)malloc(100);
        p = q;
        free(q);
        *p = 'x';
        free(p);
        p = (char *)malloc(100);
        p = (char *)malloc(100);
        q = p;
        strcat(p, q);
        assert(argc > 87);
    }
}

Las herramientas estándar del compilador, incluido gcc -Wall, no detectan ningún error. Encontrarlos por pruebas es improbable: no ocurre nada malo salvo que se dé la casualidad de ejecutar el programa con exactamente 42 argumentos. Pero con respuestas aproximadas a preguntas sobre valores nulos, destinos de punteros y condiciones de rama, la mayoría de los errores anteriores se detectan estáticamente, sin ejecutar nada.

Idealmente, las aproximaciones que usamos son conservadoras (conservative, también safe), lo que significa que todos los errores se cometen hacia el mismo lado, determinado por la aplicación que se pretenda. Aproximar el uso de memoria de un programa es conservador si las estimaciones nunca son menores que lo realmente posible en ejecución. Ese es el concepto de soundness que el capítulo «2» desarrolla y que, en ingeniería inversa, decide si uno puede fiarse o no de lo que ve en pantalla.

1.9 Cómo se organiza esto

Del binario al modelo construye el modelo: del binario al grafo de flujo de control (capítulos «3» y «4») y la maquinaria matemática mínima, la teoría de retículos (capítulo «5»), previo paso por la discusión de corrección y aproximación (capítulo «2»).

Análisis de flujo de datos es el núcleo operativo: los monotone frameworks y los análisis clásicos (6), cómo resolverlos (7), cómo tratar dominios infinitos con widening (8), cómo ganar precisión con sensibilidad al camino (9), cómo cruzar fronteras de función (10) y el marco IFDS para análisis distributivos, con el taint como aplicación estrella (11).

Forma SSA cubre la representación intermedia sobre la que trabajan los decompiladores: qué es y qué garantiza (12), cómo se construye y se destruye (13), algoritmos avanzados y reconstrucción incremental (14), propagación dispersa (15) y las extensiones que hacen falta para tratar memoria y arrays (16).

Semántica, tipos y memoria aborda lo que el flujo de datos no alcanza: flujo de control desconocido (17), punteros (18), tipos (19), sistemas de tipos y efectos (20) e interpretación abstracta como fundamento de todo lo anterior (21).

Del análisis al código recorre el camino de vuelta: cómo el análisis se convierte en transformación (22), qué huellas deja el generador de código en el binario (23) y, finalmente, cómo se ensambla todo en un decompilador real (24).

1.10 Lecturas

La equivalencia entre los cuatro enfoques del análisis estático, que aquí solo se enuncia, se demuestra por partes a lo largo de los capítulos «6», «17», «20» y «21».

Para el resultado de indecidibilidad, la referencia original es Rice (1953); la cita de Dijkstra sobre las pruebas —«Program testing can be used to show the presence of bugs, but never to show their absence»— es de 1970. La conjetura de Collatz, mencionada como ejemplo de la dificultad de razonar sobre programas triviales, sigue abierta.