τTau SolutionsAnálisis de flujo de datos

Sensibilidad al camino y análisis relacional

Operativo · Actualizado el 16 de agosto de 2026

Hasta ahora hemos ignorado los valores de las condiciones de rama y de bucle, tratando los if y los while como una elección no determinista entre dos ramas. A eso se le llama análisis insensible al control. Y como consecuencia también es insensible al camino, porque no distingue los distintos caminos que llevan a un mismo punto del programa. Este capítulo recupera esa información, que resulta ser exactamente la que hace falta para razonar sobre código ofuscado.

9.1 Qué se pierde

Considérese este programa:

x = input;
y = 0;
z = 0;
while (x > 0) {
    z = z+x;
    if (17 > y) { y = y+1; }
    x = x-1;
}

El análisis de intervalos del capítulo «8», incluso con widening y narrowing, concluye que tras el bucle x está en [-∞, ∞], y en [0, ∞] y z en [-∞, ∞]. A la vista de los condicionales, ese resultado es demasiado pesimista: cualquier lector humano ve que y no puede pasar de 17, que x acaba en 0 o menos, y que z no puede ser negativa.

La información está en las condiciones, y el análisis la está tirando.

9.2 Sensibilidad al control mediante aserciones

Para explotar la información de los condicionales, extendemos el lenguaje con una sentencia artificial assert(E), donde E es una expresión booleana. En tiempo de ejecución aborta si E es falsa y no hace nada en caso contrario; pero sólo la insertaremos en lugares donde E está garantizada, así que nunca aborta. Su función es puramente la de transportar información al análisis.

El programa anterior se transforma así:

x = input;
y = 0;
z = 0;
while (x > 0) {
    assert(x > 0);
    z = z+x;
    if (17 > y) { assert(17 > y); y = y+1; }
    x = x-1;
}
assert(!(x > 0));

Siempre es seguro ignorar las aserciones, lo que corresponde a la regla trivial ⟦assert(E)⟧ = JOIN(v). Con ella no se gana nada. Aprovecharlas requiere conocer el análisis concreto y definir reglas no triviales y correctas.

Para el análisis de intervalos, extraer la información que llevan condiciones generales como E₁ > E₂ o E₁ == E₂ es complicado y constituye en sí mismo un área de estudio. Por simplicidad, consideremos sólo condiciones de las formas X > E y E > X. La primera se maneja con

assert(X > E): ⟦v⟧ = JOIN(v)[ X ↦ gt( JOIN(v)(X), eval(JOIN(v), E) ) ]

donde gt modela el operador «mayor que» sobre intervalos:

gt([l₁,h₁], [l₂,h₂]) = [l₁,h₁] ⊓ [l₂, ∞]

Léase: si sabemos que X ∈ [l₁,h₁] y que X > E con E ∈ [l₂,h₂], entonces X está además en [l₂, ∞], y podemos quedarnos con la intersección. Las condiciones negadas se tratan de forma análoga, y a todas las demás se les da por defecto la regla trivial.

Con este refinamiento, el análisis del programa de la «sección 9.1 · Qué se pierde» concluye que tras el bucle x ∈ [-∞, 0], y ∈ [0, 17] y z ∈ [0, ∞]. Que es lo que un humano diría.

Un análisis que tiene en cuenta la información de las condiciones de rama se llama sensible al control (control sensitive) o sensible a la rama. Hay dos alternativas técnicas a la inserción de assert: modelar cada nodo de bifurcación con dos variables de restricción en lugar de una, correspondientes a los dos resultados posibles de la evaluación de la condición; o asociar las restricciones de flujo de datos a las aristas del CFG en lugar de a los nodos. Los detalles técnicos difieren, pero la idea es la misma.

9.3 Lo que la sensibilidad al control no basta para hacer

La sensibilidad al control es insuficiente para razonar sobre propiedades relacionales, que son las que surgen de la correlación entre ramas. El ejemplo típico:

if (condition) {
    open();
    flag = 1;
} else {
    flag = 0;
}
...
if (flag) {
    close();
}

open y close abren y cierran un fichero. El fichero está inicialmente cerrado, condition es una expresión compleja cualquiera, y los ... son sentencias que no llaman a open ni a close ni modifican flag. Queremos un análisis que compruebe que close sólo se llama si el fichero está abierto, que open sólo se llama si está cerrado, y que el fichero está definitivamente cerrado al salir. La propiedad crítica es que la rama que llama a close se toma sólo si antes se tomó la rama que llamó a open.

Primer intento, con el retículo de partes

L = ℘({open, closed})

y las restricciones ⟦open()⟧ = {open}, ⟦close()⟧ = {closed}, ⟦entry⟧ = {closed} y ⟦v⟧ = JOIN(v) para el resto, siendo JOIN el habitual de un análisis forward may. El resultado en el segundo if es {open, closed}: el análisis no sabe nada. Es lógico, porque el retículo ni siquiera menciona flag.

Segundo intento, con un producto que siga también el valor de la bandera:

L' = ℘({open, closed}) × ℘({flag = 0, flag ≠ 0})

e insertando aserciones para modelar los condicionales. Sigue sin funcionar. En el punto posterior al primer if-else, el análisis sólo sabe que open puede haberse llamado y que flag puede ser 0. Ha perdido la correlación entre ambas cosas.

Este tipo de análisis se llama de atributos independientes (independent attribute), porque el valor abstracto del fichero es independiente del valor abstracto de la bandera. Lo que hace falta es un análisis relacional, capaz de mantener relaciones entre variables.

9.4 Contextos de camino

Una forma de conseguirlo es generalizar el análisis para que mantenga varios estados abstractos por punto de programa. Si L es el retículo original, se sustituye por el retículo de aplicaciones

L'' = Path → L

donde Path es un conjunto finito de contextos de camino (path contexts). Un contexto de camino es típicamente un predicado sobre el estado del programa —una condición del programa define uno—. Cada sentencia se analiza entonces en tantos contextos como elementos tenga Path, cada uno describiendo un conjunto de caminos que llevan a esa sentencia. De ahí el nombre: análisis sensible al camino (path-sensitive analysis).

Para el ejemplo, tomamos Path = {flag = 0, flag ≠ 0}. Las restricciones para open, close y la entrada, usando notación lambda:

[[open()]]  = \p . {open}
[[close()]] = \p . {closed}
[[entry]]   = \p . {closed}

Las asignaciones dan trato especial a flag:

flag = 0:   [[v]] = [ flag = 0  |->  union over p in Path of JOIN(v)(p),
                      flag != 0 |->  {} ]

flag = I:   [[v]] = [ flag != 0 |->  union over p in Path of JOIN(v)(p),
                      flag = 0  |->  {} ]        (I constante distinta de 0)

flag = E:   [[v]] = \q . union over p in Path of JOIN(v)(p)   (E expresion cualquiera)

La primera regla dice que tras flag = 0 la bandera vale definitivamente 0, así que la información sobre el fichero se recoge de los predecesores con independencia de lo que valiera antes; y el contexto flag ≠ 0 se pone a ∅ —el elemento mínimo— porque ese contexto es infactible en ese punto. Ahí está la ganancia: marcar contextos como imposibles.

Para las aserciones, también trato especial:

assert(flag):   [[v]] = [ flag != 0 |-> JOIN(v)(flag != 0),
                          flag = 0  |-> {} ]

Nótese la diferencia, pequeña pero decisiva, con la regla de flag = 1: la aserción no cambia la información, sólo descarta el contexto incompatible.

Para cualquier otro nodo, la regla mantiene separada la información de los distintos contextos y se limita a propagarla: ⟦v⟧ = λp. JOIN(v)(p), con JOIN(v)(p) = ⋃w ∈ pred(v) ⟦w⟧(p).

La solución mínima para el programa de ejemplo:

Nodo contexto flag = 0 contexto flag ≠ 0
entry {closed} {closed}
condition {closed} {closed}
assert(condition) {closed} {closed}
open() {open} {open}
flag = 1 ∅ {open}
assert(!condition) {closed} {closed}
flag = 0 {closed} ∅
... {closed} {open}
flag {closed} {open}
assert(flag) ∅ {open}
close() {closed} {closed}
assert(!flag) {closed} ∅
exit {closed} {closed}

En el punto posterior al primer if-else el análisis produce [flag = 0 ↦ {closed}, flag ≠ 0 ↦ {open}]: exactamente la correlación que buscábamos. Y la restricción de assert(flag) elimina la posibilidad de que el fichero esté cerrado justo antes de close(). Objetivo cumplido.

9.5 El coste: la explosión de caminos

El análisis sensible al camino multiplica el trabajo por el número de contextos. Si se toma como Path el conjunto de todas las combinaciones de valores de verdad de las condiciones del programa, ese número es exponencial en el número de condicionales y el análisis deja de ser viable.

Todas las técnicas prácticas son, por tanto, estrategias para elegir un Path pequeño y útil:

  • Sensibilidad dirigida por la propiedad. Se toman como contextos sólo los predicados relevantes para la propiedad que se quiere comprobar. Es lo del ejemplo: flag entró en Path porque el análisis de ficheros lo necesitaba.
  • Partición de trazas (trace partitioning, Mauborgne y Rival). Se decide dinámicamente, durante el análisis, en qué puntos conviene partir el estado abstracto y en cuáles conviene volver a fusionarlo. El criterio suele ser la pérdida de precisión detectada al unir.
  • Refinamiento guiado por contraejemplos (CEGAR). Se empieza con un solo contexto —análisis insensible— y cada vez que el análisis produce un contraejemplo espurio se añade el predicado que lo elimina. Es la base de los verificadores de software por abstracción de predicados.
  • Selección por dominancia. En análisis de binarios, una heurística barata y eficaz es tomar como contextos sólo las condiciones que dominan al punto de interés, en el sentido del capítulo «4».

9.6 El extremo del espectro: la ejecución simbólica

Si se lleva la sensibilidad al camino hasta el límite —un contexto por cada camino de ejecución— se obtiene la ejecución simbólica (symbolic execution). Cada camino se representa mediante una condición de camino (path condition), una fórmula lógica sobre las entradas que caracteriza exactamente cuándo se toma ese camino, y las variables toman valores simbólicos en lugar de concretos. Un solucionador SMT decide qué caminos son factibles y produce entradas concretas que los recorren.

La ejecución simbólica no es un análisis estático en el sentido que aquí se le da: no calcula un punto fijo sobre un retículo de altura finita y no termina en presencia de bucles no acotados. Pero ocupa el mismo espacio conceptual, en el extremo opuesto:

Insensible al camino Sensible al camino Ejecución simbólica
Contextos uno un número finito fijo uno por camino
Terminación garantizada garantizada no garantizada
Falsos positivos muchos pocos ninguno, por camino explorado
Falsos negativos ninguno ninguno muchos: caminos no explorados
Coste lineal lineal por el nº de contextos exponencial

Obsérvese el cambio de naturaleza en las dos filas centrales: el análisis estático es correcto pero impreciso; la ejecución simbólica es precisa pero incompleta. Las herramientas modernas de análisis de binarios —angr es el ejemplo canónico— combinan ambas: análisis estático para acotar el espacio y decidir qué merece la pena explorar, y ejecución simbólica para resolver los casos concretos difíciles.

9.7 Aplicación: predicados opacos

9.8 Lecturas

Las referencias son Mauborgne y Rival (2005) para la partición de trazas, Clarke et al. (2000) para CEGAR, King (1976) para la ejecución simbólica y Shoshitaishvili et al. (2016) para angr y la combinación de ambos enfoques. Sobre predicados opacos, la referencia original es Collberg, Thomborson y Low (1998).