Marcos distributivos — IFDS, IDE y análisis de taint

Operativo · Actualizado el 16 de agosto de 2026

El capítulo «10» dejó un problema abierto: la sensibilidad al contexto por el enfoque funcional es precisa pero cara, porque el número de contextos puede ser enorme. Este capítulo muestra cómo la distributividad permite conseguir sensibilidad completa al flujo y al contexto en tiempo polinómico. Las técnicas son de Reps, Horwitz y Sagiv, y son la base de prácticamente todas las herramientas industriales de análisis de taint.

11.1 Un ejemplo motivador: variables posiblemente no inicializadas

El objetivo del análisis de variables posiblemente no inicializadas es aproximar, en cada punto del programa, qué variables pueden tener valores procedentes de variables no inicializadas.

Este análisis es prácticamente idéntico al análisis de taint (taint analysis), que infiere qué cálculos pueden involucrar datos «contaminados» procedentes de entrada no fiable. Lo que en un caso es «no inicializado» en el otro es «contaminado»; la maquinaria es la misma. Aquí se presenta el primero, y en la «sección 11.6 · Análisis de taint sobre binarios» se traduce al segundo.

Un ejemplo, con las variables posiblemente no inicializadas anotadas en cada punto:

var a,b,c;          // a,b,c
a = input;          // b,c
b = a + c;          // b,c
if (input) {        // b,c
    c = 1;          // b
}                   // b,c

Obsérvese que b sigue siendo posiblemente no inicializada tras b = a + c, porque su valor depende de c; el análisis no es, por tanto, el dual del análisis de variables inicializadas. Y en el punto final c es posiblemente no inicializada pese a la asignación c = 1, porque la rama que la contiene puede no tomarse.

Diseñemos el análisis, sensible al flujo y al contexto, con el enfoque funcional del capítulo «10». El retículo de estados abstractos es

State = ℘(Var)

y como los contextos son estados abstractos, Context = State, de modo que el retículo del análisis para un programa con n nodos es

( ℘(Var) → lift(℘(Var)) )ⁿ

Un elemento de este retículo contiene, para cada nodo v, una función

m_v : ℘(Var) → ( ℘(Var) ∪ {unreachable} )

llamada función de salto (jump function). Su significado: si la función de programa que contiene a v se entra desde una llamada con conjunto de variables posiblemente no inicializadas s, entonces el conjunto en v es m_v(s); y m_v(s) = unreachable significa que no existe tal llamada en el programa.

Por ejemplo, para

foo(x, y) {
    var z;
    z = x - y;
    z = z * z;
    return z;
}

se tiene m_{return z}({y}) = {y, z}: si se llama a foo con y posiblemente no inicializada y x definitivamente inicializada, entonces y y z lo están en el retorno.

Las funciones de transferencia son sencillas. Para una declaración, que en TIP deja la variable sin inicializar:

t_{var X}(s) = s ∪ {X}

Y para una asignación:

t_{X = E}(s) = s ∪ {X} si vars(E) ∩ s ≠ ∅ ; s \ {X} en otro caso

es decir, X queda contaminada si y sólo si alguna de las variables que intervienen en E lo estaba.

La restricción de análisis para un nodo v es la habitual del capítulo «10», con el contexto arrastrado:

[[v]](c) = t_v(JOIN(v,c))   si JOIN(v,c) pertenece a P(Var)
         = unreachable      si JOIN(v,c) = unreachable

JOIN(v,c) = join over w in pred(v) of [[w]](c)

Y el resultado final en un punto v se obtiene uniendo sobre todos los contextos: ⊔_{c ∈ Context} ⟦v⟧(c).

Como se vio en el capítulo «10», para el nodo de salida de una función la función de salto resume la función entera. Para el foo anterior:

m_exit(s) = s ∪ {z} si x ∈ s ∨ y ∈ s ; s \ {z} en otro caso

Una vez calculado m_exit(s) para un s dado, el resultado se reutiliza en todas las llamadas cuyo estado de entrada sea s, sin volver a recorrer el cuerpo. El algoritmo de lista de trabajo del capítulo «7» hace esa reutilización automáticamente.

El problema es el coste. Con Context = ℘(Var) hay 2^|Var| contextos posibles, y el retículo tiene altura exponencial. La reutilización ayuda y el marcado de contextos inalcanzables ayuda, pero la cota sigue siendo exponencial. La distributividad es lo que arregla esto.

11.2 Representación compacta de funciones distributivas

Recuérdese que f : L₁ → L₂ es distributiva cuando f(x) ⊔ f(y) = f(x ⊔ y) para todos x, y.

Consideremos funciones f : ℘(D) → ℘(D) distributivas, con D finito. Una representación ingenua de f sería una tabla con 2^|D| entradas —inviable si D es el conjunto de variables de un programa real—. Pero una función distributiva queda caracterizada por su valor sobre el conjunto vacío y sobre cada conjunto unitario. En efecto, f({d₂, d₃}) = f(∅) ∪ f({d₂}) ∪ f({d₃}).

Eso permite descomponer f en una función g : (D ∪ {•}) → ℘(D):

g(•) = f(∅) , g(d) = f({d}) \ f(∅) para d ∈ D

y entonces, para todo X ⊆ D,

f(X) = g(•) ∪ ⋃_{y ∈ X} g(y)

de modo que g representa completamente a f. El símbolo • puede entenderse como un hecho de flujo de datos que se cumple siempre.

Una g así se representa como un grafo bipartito con 2·(|D|+1) nodos: exponencialmente más compacto que la tabla. Con D = {d₁, d₂, d₃}:

     entrada:    *      d1      d2      d3
                 | \                 \    |
                 |   \                 \  |
                 v     v                 v v
     salida:     *      d1      d2      d3

     aristas:  * -> *      (siempre presente)
               * -> d1     (d1 se cumple incondicionalmente a la salida)
               d2 -> d3    (si d2 a la entrada, entonces d3 a la salida)
               d3 -> d3    (si d3 a la entrada, entonces d3 a la salida)

Representacion bipartita de una funcion distributiva. Arriba la entrada, abajo la salida.

Este grafo representa g(•) = {d₁}, g(d₁) = ∅, g(d₂) = g(d₃) = {d₃}, y por tanto la función f tal que f(S) = {d₁, d₃} si d₂ ∈ S o d₃ ∈ S, y f(S) = {d₁} en caso contrario.

En general, las aristas son

{ • → • } ∪ { • → y : y ∈ f(∅) } ∪ { x → y : y ∈ f({x}) ∧ y ∉ f(∅) }

Intuitivamente, las aristas describen cómo depende la salida de la entrada. En el análisis de variables posiblemente no inicializadas, con D = Var, la arista d₂ → d₃ significa: si d₂ está posiblemente no inicializada a la entrada, d₃ lo está a la salida. Y la arista • → d₁ significa que d₁ está incondicionalmente no inicializada a la salida.

Formalización

Las dos propiedades de cierre

Para que esta representación sirva para funciones de salto hacen falta dos propiedades, y afortunadamente ambas se cumplen: la distributividad es cerrada bajo composición y bajo supremo.

Si f_A y f_B son distributivas, entonces f_A ∘ f_B y f_A ⊔ f_B lo son, donde (f_A ⊔ f_B)(S) = f_A(S) ⊔ f_B(S).

Y ambas operaciones tienen una lectura gráfica inmediata: la composición es la concatenación de los dos grafos bipartitos, poniendo uno debajo del otro y quedándose con la alcanzabilidad de arriba abajo; el supremo es la unión de los conjuntos de aristas. Las dos se calculan en tiempo O(|D|³) y O(|D|²) respectivamente, con implementaciones directas.

Ésta es toda la magia del marco IFDS: componer resúmenes de función se convierte en alcanzabilidad en un grafo.

11.3 El CFG explotado

La representación anterior sugiere reorganizar el programa entero como un solo grafo. El CFG explotado (exploded CFG, o exploded supergraph) tiene un nodo por cada pareja ⟨v, d⟩ de un nodo v del CFG y un elemento d ∈ D ∪ {•}.

Si el grafo bipartito de la función de transferencia t_v₁ tiene una arista d₁ → d₂, y el CFG tiene una arista de v₁ a v₂, entonces el CFG explotado tiene una arista de ⟨v₁, d₁⟩ a ⟨v₂, d₂⟩. Llamemos E al conjunto de todas esas aristas.

El paso de parámetros y el flujo de valores de retorno se tratan como asignaciones; y el flujo directo de los nodos de llamada a sus nodos posteriores, para las variables locales que la llamada no afecta, se modela igual.

Por ejemplo, con Var = {x, y, z} y v la asignación x = y + z, con predecesor v', las aristas de E para el análisis de variables posiblemente no inicializadas son:

   <v', *>   <v', x>   <v', y>   <v', z>
      |  \                 |  \      |  \
      |    \               |    \    |    \
      v      v             |      v  v      v
   <v,  *>   <v,  x>   <v,  y>   <v,  z>

   La arista <v',y> -> <v,x> y la arista <v',z> -> <v,x> expresan que
   x queda contaminada si y o z lo estaban. Las aristas <v',y> -> <v,y>
   y <v',z> -> <v,z> expresan que y y z conservan su estado.

Fragmento del CFG explotado para la asignacion x = y + z.

La propiedad clave del CFG explotado es ésta:

Un hecho de flujo de datos d ∈ D puede cumplirse en el nodo v si y sólo si ⟨v, d⟩ es alcanzable desde ⟨entry_main, •⟩ a lo largo de un camino interprocedural válido en el CFG explotado.

El análisis de flujo de datos se ha convertido en un problema de alcanzabilidad en un grafo. Ése es el resultado central de IFDS, y de ahí el nombre: Interprocedural, Finite, Distributive, Subset problems.

11.4 El marco IFDS

El algoritmo procede en dos fases.

Fase 1: tabulación

Se construye incrementalmente un conjunto de aristas de camino (path edges) P, cada una escrita ⟨v₁, d₁⟩ ⇝ ⟨v₂, d₂⟩, donde v₁ es un nodo de entrada de función, v₂ es un nodo del CFG en esa misma función, y d₁, d₂ ∈ D ∪ {•}.

La idea es que el conjunto de aristas de camino que terminan en v₂ constituye la representación bipartita de la función de salto de v₂, relacionando los hechos a la entrada de la función con los hechos en v₂. La alcanzabilidad se sigue al nivel de hechos individuales: una arista de camino se añade sólo si ya se ha establecido que ⟨v₁, d₁⟩ puede ser alcanzable desde la entrada del programa. Es más fino que seguir la alcanzabilidad de funciones (capítulo «10») o de contextos.

Las cuatro reglas, cuya menor solución se calcula con un algoritmo de lista de trabajo:

(1) La entrada del programa siempre es alcanzable:

⟨entry_main, •⟩ ⇝ ⟨entry_main, •⟩ ∈ P

(2) Entrada de función. Si v es un nodo de entrada de función, v₁ ∈ pred(v) es un nodo de llamada que llama a la función que contiene a v, y v₀ es el nodo de entrada de la función que contiene a v₁:

⟨v₀, d₁⟩ ⇝ ⟨v₁, d₂⟩ ∈ P ∧ ⟨v₁, d₂⟩ → ⟨v, d₃⟩ ∈ E ⟹ ⟨v, d₃⟩ ⇝ ⟨v, d₃⟩ ∈ P

A primera vista parece un error, pero recuérdese que esta fase no propaga hechos —eso es la fase 2—, sino que construye aristas de camino para los nodos del CFG explotado alcanzables desde la entrada. La arista nueva ⟨v, d₃⟩ ⇝ ⟨v, d₃⟩ significa simplemente: ⟨v, d₃⟩ puede ser alcanzable.

(3) Nodo posterior a la llamada. Si v es un nodo posterior a la llamada v', v₀ es el nodo de entrada de la función que los contiene, w ∈ succ(v') es el nodo de entrada de la función llamada y w' ∈ pred(v) su nodo de salida:

⟨v₀,d₁⟩ ⇝ ⟨v',d₂⟩ ∈ P ∧ ⟨v',d₂⟩ → ⟨w,d₃⟩ ∈ E ∧ ⟨w,d₃⟩ ⇝ ⟨w',d₄⟩ ∈ P ∧ ⟨w',d₄⟩ → ⟨v,d₅⟩ ∈ E ⟹ ⟨v₀,d₁⟩ ⇝ ⟨v,d₅⟩ ∈ P

      funcion llamadora              funcion llamada f

        <v0, d1>
            :
            :  (P)
            v
        <v', d2> ------(E)------> <w, d3>
                                      :
                                      :  (P)
                                      v
        <v,  d5> <-----(E)------ <w', d4>
            ^
            :
            +---- nueva arista de camino <v0,d1> ~> <v,d5>

Regla del nodo posterior a la llamada. Lineas continuas: aristas de E. Discontinuas: aristas de camino de P.

Nótese cómo esta regla usa las aristas de camino del nodo de salida w' como resumen de la función llamada, y cómo el flujo sigue únicamente caminos interprocedurales válidos —entra por v', sale por el w' correspondiente—. Ahí está la sensibilidad al contexto.

(4) Flujo local. Para el estado local que pasa del nodo de llamada v' a su nodo posterior v, y en general para cualquier nodo v con predecesor v' dentro de la misma función:

⟨v₀, d₁⟩ ⇝ ⟨v', d₂⟩ ∈ P ∧ ⟨v', d₂⟩ → ⟨v, d₃⟩ ∈ E ⟹ ⟨v₀, d₁⟩ ⇝ ⟨v, d₃⟩ ∈ P

Fase 2: lectura del resultado

La segunda fase es notablemente simple y enteramente intraprocedural. El estado abstracto de cualquier nodo v se lee directamente de sus aristas de camino, siendo v₀ el nodo de entrada de la función que lo contiene:

⟨v₀, d₁⟩ ⇝ ⟨v, d₂⟩ ∈ P ⟹ d₂ ∈ ⟦v⟧

Funciona porque en la fase 1 sólo se añadió esa arista si el hecho d₂ puede cumplirse en v. El seguimiento fino de la alcanzabilidad hecho a hecho es lo que hace innecesaria cualquier propagación adicional.

Formalización

Precisión y coste

Coste. La complejidad en el peor caso del análisis IFDS es

O( |E| · |D|³ )

donde E es el conjunto de aristas del CFG. Compárese con el coste exponencial de la formulación directa del enfoque funcional de la «sección 11.1 · Un ejemplo motivador: variables posiblemente no inicializadas». Ésa es la ganancia.

Precisión. Un camino interprocedural válido es un camino v₀ · v₁ · … · v_k en el CFG desde la entrada del programa hasta v = v_k en el que todas las llamadas y retornos casan. Sea IVP el conjunto de todos ellos. Entonces el estado abstracto calculado por IFDS cumple

⟦v⟧ = ⊔_{v₀·v₁·…·v_k ∈ IVP} ( t_{v_k} ∘ t_{v_k-1} ∘ … ∘ t_v₁ )(⊥)

Es decir, IFDS calcula la solución meet-over-all-valid-paths: el análogo interprocedural de la solución MOP del capítulo «7», restringida a los caminos válidos. Es lo mejor que puede pedirse.

Nótese lo que esto significa a la luz del capítulo «7»: allí veíamos que MOP es en general incomputable, y aquí se calcula exactamente. La diferencia es la hipótesis de distributividad, que es justamente la que hacía coincidir MOP con MFP.

11.5 IDE: aristas con etiqueta

IFDS trabaja con hechos de flujo de datos que se cumplen o no se cumplen: el dominio es ℘(D). Muchos análisis interesantes necesitan asociar un valor a cada hecho: no basta con «x está contaminada», hace falta «x vale 5» o «x está contaminada con datos de origen web».

El marco IDE (Interprocedural Distributive Environment problems) generaliza IFDS a funciones de la forma

f : (D → L) → (D → L)

con D finito y L un retículo completo. La representación bipartita se generaliza etiquetando cada arista con una función L → L. Se define g : (D ∪ {•}) × (D ∪ {•}) → (L → L) por

g(d1, d2)(e) = f(bottom[d1 -> e])(d2)     para d1, d2 en D
g(*,  d2)(e) = f(bottom)(d2)              para d2 en D
g(*,  *)(e)  = e
g(d1, *)(e)  = bottom

Intuitivamente, g(a, b) : L → L especifica cómo influye el valor abstracto de a a la entrada en el valor abstracto de b a la salida. Una arista ausente equivale a una arista etiquetada con ⊥, y por convención una arista sin etiqueta dibujada significa la identidad λe.e. La arista g(•, •) es siempre la identidad.

Con D = {d₁, d₂, d₃} y L el retículo de propagación de constantes, un ejemplo:

   entrada:    *          d1         d2         d3
               |  \                    \
               |    \  lambda e . 5      \  lambda e . si e >= 3 entonces T si no bottom
               v      v                    v
   salida:     *          d1         d2         d3

Grafo bipartito etiquetado de IDE. Las etiquetas son funciones de L en L.

Si m = [d₁ ↦ ⊥, d₂ ↦ 42, d₃ ↦ ⊤], entonces f(m) = [d₁ ↦ 5, d₂ ↦ ⊤, d₃ ↦ ⊥].

El resultado que hace utilizable la construcción es:

f(m)(b) = g(•, b)(⊥) ⊔ ⊔_{a ∈ D} g(a, b)(m(a))

Para que todo esto sea práctico hacen falta dos cosas más, que dependen del análisis concreto: una representación compacta de las funciones de arista L → L que aparezcan, y algoritmos eficientes para componerlas y para calcular su supremo. El caso mejor estudiado es la propagación de constantes por copia (copy-constant propagation), donde las funciones de arista son de la forma λe. c o λe. e y se componen trivialmente.

Obsérvese, por último, que IFDS es el caso particular de IDE con L = {⊤, ⊥}: el retículo de dos elementos, en el que ℘(D) y D → L son isomorfos vía la función característica.

11.6 Análisis de taint sobre binarios

En ingeniería inversa

El marco IFDS en la práctica de la seguridad

Traducir el análisis de la «sección 11.1 · Un ejemplo motivador: variables posiblemente no inicializadas» a análisis de taint es un cambio de vocabulario:

Donde el análisis original decía «var X genera el hecho», el de taint dice «una fuente (source) genera el hecho»: recv, read, argv, getenv, la lectura de un fichero.
La regla de propagación de X = E es idéntica: la contaminación se propaga por dependencia de datos.
Aparece una regla nueva que no tenía el original: un sanitizador (sanitizer) mata el hecho. Es un kill puro y encaja sin problemas en el esquema.
Y la consulta cambia de «¿se usa X sin inicializar?» a «¿llega el hecho a un sumidero (sink)?»: system, exec, strcpy, memcpy, printf con formato variable.

Las herramientas industriales de análisis de taint —FlowDroid para Android, y los motores de análisis de binarios basados en Soot o en el marco Heros— son literalmente instancias de IFDS. La elección de fuentes, sumideros y sanitizadores es la configuración; el algoritmo es el de la «sección 11.4 · El marco IFDS».

Lo que se gana. Sensibilidad completa al flujo y al contexto en tiempo O(|E|·|D|³), con resúmenes de función reutilizables. Sobre un binario de tamaño medio esto es minutos, no horas.

Lo que hay que vigilar. IFDS exige distributividad, y hay dos formas habituales de perderla sin darse cuenta:

Sanitización condicional. «x deja de estar contaminada si y está validada» no es distributiva: depende de dos hechos a la vez. La solución habitual es meter la pareja en D, lo que multiplica su tamaño y, como el coste es cúbico en |D|, se paga caro.
Contaminación implícita (implicit flows). Si if (secreto) x = 1; else x = 2;, entonces x depende de secreto sin que haya ninguna dependencia de datos. Capturarlo requiere dependencia de control (capítulo «4»), y las reglas dejan de ser distributivas. Casi todas las herramientas prácticas ignoran los flujos implícitos y lo reconocen abiertamente: es una fuente conocida de falsos negativos.

En binarios, además, D no es el conjunto de variables sino el de posiciones de memoria abstractas: registros, ranuras de pila y objetos del montón identificados por sitio de asignación. Su tamaño depende directamente de la calidad del análisis de punteros del capítulo «18». Un análisis de punteros pobre infla D y el coste cúbico lo castiga; uno bueno lo mantiene pequeño. Es el ejemplo más claro de cómo la precisión de un análisis determina la viabilidad de otro.

11.7 Lecturas

La conexión con la solución MOP, y la coincidencia MOP = MFP bajo distributividad, está en el capítulo «7».

Las referencias originales son Reps, Horwitz y Sagiv (1995) para IFDS y Sagiv, Reps y Horwitz (1996) para IDE. Sobre herramientas, Arzt et al. (2014) para FlowDroid y Bodden (2012) para Heros.