Chasing Elusive Memory Bugs in GPU Programs

Sintesi Tecnica: Dare la caccia agli elusivi bug di memoria nei programmi GPU

Problematica
I bug di sicurezza della memoria, in particolare gli accessi fuori limite (out-of-bounds, OOB), rimangono una vulnerabilità critica nel software accelerato da GPU, minacciando sia la sicurezza che l'affidabilità. Sebbene gli strumenti di rilevamento esistenti (ad esempio, NVIDIA Compute Sanitizer, cuCatch, GMOD) utilizzino l'analisi dinamica a runtime per identificare gli OOB, essi soffrono di due limitazioni fondamentali:

1. OOB dipendenti dall'input: Questi bug si manifestano solo sotto specifiche condizioni di input. Poiché gli strumenti a runtime richiedono che il bug si verifichi effettivamente durante l'esecuzione per essere rilevato, essi spesso mancano questi errori elusivi se non vengono forniti gli input "corretti" durante i test.
2. OOB intra-allocazione: Nei programmi CUDA, è comune partizionare logicamente una singola allocazione di memoria (specialmente la memoria condivisa dinamica o la memoria locale) in più strutture dati distinte utilizzando l'aritmetica dei puntatori. Gli strumenti esistenti tracciano solo i confini dell'allocazione grezza e sono agnostici rispetto a queste partizioni logiche. Di conseguenza, non possono rilevare quando un thread accede a una struttura dati al di fuori della propria partizione logica ma ancora entro i confini della partizione genitrice.

Inoltre, gli strumenti esistenti basati esclusivamente su software comportano significativi carichi di lavoro (overhead) in termini di prestazioni e memoria a runtime a causa dell'strumentazione, mentre le soluzioni assistite dall'hardware richiedono modifiche hardware non standard.

Metodologia: SCuBA
Gli autori propongono SCuBA (Static CUDA Bounds Analyzer), un nuovo strumento di analisi statica a tempo di compilazione progettato per rilevare sia gli OOB dipendenti dall'input che quelli intra-allocazione senza overhead a runtime o modifiche all'hardware.

• Intuizione Centrale: Gli autori osservano che nei programmi GPU privi di bug, esiste una relazione semantica tra le variabili che determinano le dimensioni dell'allocazione di memoria (tipicamente nel codice host/CPU) e le variabili che calcolano gli offset di accesso alla memoria (nel codice kernel della GPU). L'assenza di tale relazione di legame indica un potenziale OOB.
• Analisi Statica e IR: SCuBA utilizza il framework MLIR (Multi-Level Intermediate Representation) e il compilatore CGeist per tradurre sia il codice CUDA host che quello kernel in una rappresentazione intermedia. A differenza dell'analisi binaria, MLIR conserva informazioni semantiche di alto livello, inclusa l'aritmetica dei puntatori utilizzata per la partizione logica.
• Generazione dei Vincoli:
  • Analisi Host: SCuBA costruisce alberi di espressione (Expression Trees, ET) per modellare come le dimensioni di allocazione della memoria (ad esempio, cudaMalloc) e le dimensioni della griglia dei thread siano derivate dalle variabili di input.
  • Analisi Kernel: Traccia come vengono calcolati gli offset di accesso alla memoria utilizzando gli identificatori dei thread (threadIdx, blockIdx) e analizza l'aritmetica dei puntatori per identificare le partizioni logiche all'interno della memoria condivisa e locale.
  • Partizione Logica: Per la memoria condivisa dinamica, SCuBA traccia l'allocazione di base e gli offset utilizzati per ritagliare le sottostrutture, calcolando la dimensione logica di ogni partizione.
• Risolutore SAT: SCuBA formula il problema del rilevamento come un problema di soddisfacibilità (SAT). Genera vincoli che rappresentano:
  1. La semantica CUDA (ad esempio, gli ID dei thread devono essere inferiori alle dimensioni della griglia).
  2. Le relazioni semantiche derivate dal codice (ad esempio, equazioni delle dimensioni di allocazione).
  3. La condizione per un OOB (offset $\ge$ dimensione di allocazione).
     Il risolutore SAT (Google OR-Tools) verifica se esiste qualsiasi assegnazione di input legale che soddisfi contemporaneamente tutti i vincoli. Se una soluzione esiste, un OOB è possibile, indipendentemente dal fatto che si sia manifestato in una specifica esecuzione.
• Use-After-Free (UAF): Lo strumento traccia anche i cicli di vita della memoria per rilevare gli UAF, mantenendo un insieme di allocazioni vive e verificando che gli accessi avvengano solo su memoria valida e non deallocata.

Contributi Chiave

1. Scoperta di Bug Elusivi: Gli autori dimostrano l'esistenza di OOB dipendenti dall'input in ampiamente utilizzati programmi e librerie CUDA open-source che sfuggono agli attuali strumenti a runtime.
2. Identificazione di OOB Intra-Allocazione: Identificano e definiscono una nuova classe di bug derivanti dalla partizione logica delle allocazioni di memoria, che gli strumenti esistenti non possono rilevare.
3. Primo Strumento Statico del Genere: SCuBA è il primo strumento che combina l'analisi statica con la risoluzione SAT per rilevare questi OOB elusivi e gli errori intra-allocazione senza overhead a runtime o modifiche all'hardware.

Risultati
Gli autori hanno valutato SCuBA contro un set diversificato di 20 carichi di lavoro, inclusi popolari librerie (Kaldi, llm.c), suite di benchmark (Rodinia, HeCBench, Indigo) e campioni CUDA.

• Capacità di Rilevamento: Rispetto a NVIDIA Compute Sanitizer, SCuBA ha rilevato 45 OOB che il sanitizer ha mancato. Nello specifico, ha trovato 30 OOB dipendenti dall'input precedentemente non segnalati e 19 OOB intra-allocazione (introdotti per testare programmi che erano altrimenti sicuri).
• Accuratezza: SCuBA ha riportato zero falsi positivi e zero falsi negativi attraverso i carichi di lavoro valutati.
• Overhead: Come strumento di analisi statica, SCuBA non comporta alcun overhead di prestazioni o di memoria a runtime. Il tempo di analisi è un costo di compilazione una tantum, che varia da 8 millisecondi a 32 secondi, con il risolutore SAT che rappresenta il principale contributore a questo tempo.

Significato
L'articolo sostiene che la dipendenza dall'analisi dinamica a runtime sia un collo di bottiglia fondamentale per la sicurezza della memoria nelle GPU, poiché non può rilevare proattivamente bug che dipendono da specifici input non testati o da complesse strutture logiche di memoria. Spostando l'approccio verso l'analisi statica che sfrutta le relazioni semantiche e la risoluzione SAT, SCuBA offre un modo per garantire l'assenza di questi elusivi bug di sicurezza della memoria prima della distribuzione. Gli autori posizionano SCuBA come un'evoluzione necessaria nell'instrumentazione GPU per affrontare i limiti degli attuali sanitizers standard del settore, particolarmente per applicazioni critiche per la sicurezza dove mancare un bug intermittente è inaccettabile.