Vulnerability Abundance: A formal proof of infinite vulnerabilities in code

Titolo: Abbondanza delle Vulnerabilità: Una dimostrazione formale dell'infinità delle vulnerabilità nel codice

1. Il Problema

Il dibattito fondamentale nella sicurezza informatica riguarda la natura delle vulnerabilità software: sono finite e esauribili (sparse) o infinite e inesauribili (dense)?

• Se le vulnerabilità sono sparse, la strategia di "patching esaustivo" ha senso: ogni correzione riduce significativamente l'esposizione al rischio.
• Se sono dense, correggere una singola vulnerabilità diventa un lavoro di Sisifo, poiché il serbatoio di difetti non si esaurisce mai e nuove vulnerabilità vengono continuamente generate.
  Mentre argomentazioni teoriche (come quelle basate sul problema della fermata o sul teorema di Rice) suggeriscono che le vulnerabilità potrebbero essere illimitate, mancava una dimostrazione costruttiva ed esplicita che un singolo programma potesse generare un numero infinito di vulnerabilità distinte e assegnabili a un CVE (Common Vulnerabilities and Exposures).

2. Metodologia

Gli autori adottano un approccio formale che combina teoria degli insiemi, teoria della computabilità e analisi del codice reale:

• Costruzione del "Vulnerability Factory": Gli autori hanno sviluppato un programma C specifico (622 righe) chiamato Vulnerability Factory. Questo programma non è un semplice bug, ma un generatore di vulnerabilità.
  • Base Set (B): Contiene 11 funzioni di base, ognuna con una vulnerabilità classica di una diversa classe CWE (es. overflow di buffer, injection, use-after-free).
  • Generatore (G): Ad ogni esecuzione, il generatore legge un contatore persistente $n \in \mathbb{N}$, crea un nuovo file sorgente C (vuln_module_n.c) contenente 5 vulnerabilità parametrizzate (dove i parametri come dimensioni dei buffer o soglie di overflow dipendono da $n$), lo compila in una libreria condivisa e incrementa $n$.
• Formalizzazione Matematica:
  • Le vulnerabilità sono definite come tuple $(c, t, p)$ dove $c$ è il componente software, $t$ il tipo CWE e $p$ i parametri.
  • Viene applicata la teoria degli insiemi elementare per dimostrare che l'insieme delle vulnerabilità generate è numerabile ($\aleph_0$).
  • Viene utilizzata la Teoria della Computabilità (Macchina di Turing) per modellare il generatore, dimostrando che il comportamento di generazione è decidibile e strutturale.
• Verifica delle Regole CVE: L'analisi verifica che ogni vulnerabilità generata soddisfi le regole di assegnazione del CVE di MITRE (componente identificabile, fixabile indipendentemente, causa radice distinta).

3. Contributi Chiave

Il paper presenta cinque contributi principali:

1. Dimostrazione Costruttiva: Presentazione del Vulnerability Factory, un artefatto C che prova matematicamente l'esistenza di un insieme numerabile infinito di vulnerabilità distinte e assegnabili a CVE.
2. Formalizzazione come Macchina di Turing: Il generatore è modellato come una Macchina di Turing, rendendolo un "artefatto di prova" riutilizzabile per futuri risultati formali nella teoria delle vulnerabilità.
3. Concetto di "Abbondanza delle Vulnerabilità" (Vulnerability Abundance): Introduzione di un nuovo framework quantitativo, analogo all'abbondanza degli elementi chimici, che descrive la distribuzione proporzionale delle classi di vulnerabilità in un corpus software globale.
4. Distinzione tra Vulnerabilità ed Exploit: Analisi critica che separa l'infinità delle vulnerabilità teoriche dalla popolazione finita degli exploit effettivamente utilizzati, introducendo il concetto di "esposizione all'exploit" basato sulla quota di mercato del software.
5. Utilità Pratica: Dimostrazione che la misurazione dell'abbondanza e della sua interazione con il deployment del software ha valore concreto per la prevenzione e l'analisi del rischio informatico.

4. Risultati Principali

• Teorema dell'Infinità: L'insieme delle vulnerabilità $V$ generate dal Vulnerability Factory è numerabilmente infinito. Ogni modulo $M_n$ genera 5 nuove vulnerabilità distinte dai moduli precedenti (a causa di parametri diversi come dimensioni di buffer e layout della memoria), soddisfacendo i criteri per ottenere un CVE unico.
• Robustezza: La prova è robusta anche se alcune classi di vulnerabilità venissero invalidate (rimozione di un numero finito di template CWE), poiché l'insieme rimanente rimane infinito.
• Implicazione Teorica: Poiché esiste un singolo programma con infinite vulnerabilità, l'insieme di tutte le vulnerabilità software è necessariamente infinito. Di conseguenza, nessun database di vulnerabilità finito può essere mai completo.
• Abbondanza Dinamica: L'abbondanza delle vulnerabilità non è statica; dipende dal linguaggio di programmazione (es. C/C++ favoriscono corruzione di memoria, mentre linguaggi sicuri come Rust spostano l'abbondanza verso errori logici o injection) e dalle tendenze del mercato.
• Il Principio del "Piccolo Exploit": Sebbene le vulnerabilità siano infinite, gli exploit sono pochi. La quota di mercato del software agisce come un moltiplicatore: un singolo exploit contro un software dominante (es. Windows, Linux kernel) espone una frazione enorme di macchine, rendendo il rischio sistemico legato alla concentrazione del deployment, non alla quantità totale di bug.

5. Significato e Implicazioni

• Cambio di Paradigma: Il lavoro risolve il dibattito "denso vs. sparso" in modo costruttivo: le vulnerabilità sono dense (infinite). Tuttavia, questo non significa che la sicurezza sia impossibile, ma che la strategia deve cambiare. Non si tratta di "svuotare l'oceano" di bug, ma di mappare le correnti (abbondanza) e capire dove si concentrano i rischi.
• Economia della Sicurezza: Fornisce una base quantitativa per l'economia della sicurezza. Se si può misurare l'abbondanza di certi tipi di bug (es. 70% errori di sicurezza in C/C++ sono problemi di sicurezza della memoria), gli investimenti possono essere indirizzati strategicamente (es. migrazione a Rust) per massimizzare il ROI.
• Prevenzione e Risk Analysis: Il concetto di "Abbondanza" permette di prevedere il rischio basandosi sulla distribuzione dei linguaggi e delle architetture software, piuttosto che sul semplice conteggio dei CVE.
• Strumento per la Ricerca: Il Vulnerability Factory diventa un "oggetto di test" fondamentale per valutare la scalabilità degli strumenti di analisi statica e per dimostrare i limiti della verifica formale (nessuno scanner finito può essere esaustivo).

In conclusione, il paper dimostra che l'infinità delle vulnerabilità è una proprietà strutturale della computazione, non un'anomalia. La sfida per la sicurezza non è l'esaurimento dei bug, ma la gestione dinamica della loro distribuzione (abbondanza) e la mitigazione del rischio attraverso la diversificazione dei linguaggi e la comprensione delle dinamiche di mercato.