Filament: Denning-Style Information Flow Control for Rust

1. Il Problema

Il controllo del flusso di informazioni (IFC - Information Flow Control) è fondamentale per garantire che i dati sensibili vengano accessi e trasmessi solo in conformità alle policy di sicurezza. Esistono due approcci principali:

• Sistemi Denning-style (a grana fine): Tracciano i flussi espliciti (assegnazioni) e impliciti (dipendenze di controllo, come if e cicli) a livello di variabile e istruzione. Offrono garanzie forti e precisione, ma tradizionalmente richiedono modifiche al compilatore e al linguaggio, rendendoli difficili da adottare in linguaggi mainstream come Rust.
• Sistemi a grana grossa (o a blocco): Come Cocoon (l'approccio precedente per Rust), evitano modifiche al compilatore ma impongono modelli di programmazione restrittivi. In Cocoon, i dati sensibili devono essere confinati in blocchi secret_block!, che richiedono l'uso frequente di "escape hatch" (meccanismi di bypass) per gestire effetti collaterali o chiamate a librerie esterne, aumentando il rischio di errori umani e perdite di dati.

Il conflitto fondamentale risiede nel trovare un equilibrio tra la precisione teorica del modello Denning e la praticità di implementazione senza modificare il compilatore.

2. Metodologia: Filament

Filament è una libreria statica IFC per Rust che implementa un sistema di stile Denning senza richiedere modifiche al compilatore. Risolve le sfide tecniche attraverso tre meccanismi innovativi che sfruttano il sistema di tipi e le macro di Rust:

• Controllo dei Flussi Espliciti con Inferenza di Tipo:

  • Utilizza il tipo astratto Labeled<T, L> (dove L è un'etichetta di sicurezza) per incapsulare i dati.
  • Sfrutta l'inferenza dei tipi di Rust per propagare automaticamente le etichette durante le operazioni (es. x + y eredita l'etichetta più restrittiva tra x e y tramite l'operazione di join del reticolo di sicurezza).
  • Introduce la macro relabel! per permettere agli sviluppatori di elevare esplicitamente la sensibilità di un dato quando necessario, superando la rigidità del sistema di tipi di Rust senza violare la sicurezza.

• Controllo dei Flussi Impliciti tramite pc_block!:

  • A differenza di Cocoon che usa blocchi di codice statici, Filament introduce la macro pc_block!{(L) {...}}.
  • Questa macro definisce un contesto lessicale in cui l'etichetta del contatore di programma (pc) viene inizializzata a L.
  • All'interno del blocco, il sistema verifica staticamente che ogni assegnazione rispetti il vincolo: l'etichetta del target deve essere almeno tanto restrittiva quanto il pc corrente. Questo permette di tracciare i flussi impliciti derivanti da condizioni di branch sensibili senza modificare il compilatore.

• Interoperabilità con Librerie Esterne (fcall! e mcall!):

  • Per gestire librerie standard e di terze parti (che non conoscono i tipi Labeled), Filament non richiede di "declassificare" i dati (abbassare la sicurezza) e poi riavvolgerli, un pattern pericoloso usato in Cocoon.
  • Le macro fcall! (per funzioni) e mcall! (per metodi) agiscono come wrapper: estraggono i valori non etichettati, eseguono la chiamata, e avvolgono il risultato nell'etichetta più restrittiva tra tutti gli input. Questo mantiene l'integrità del flusso di informazioni attraverso i confini della libreria.

3. Contributi Chiave

1. Primo sistema IFC Denning-style per Rust senza modifiche al compilatore: Filament è il primo strumento che porta la precisione dei flussi a livello di istruzione in un linguaggio imperativo mainstream mantenendo la compatibilità con il compilatore Rust stabile.
2. Modello di programmazione più permissivo: Rispetto a Cocoon, Filament elimina la necessità di secret_block globali. Le restrizioni sui effetti collaterali si applicano solo all'interno di pc_block! (quando il flusso di controllo dipende da dati sensibili), riducendo drasticamente la necessità di bypassare le controlli di sicurezza.
3. Riduzione del carico di annotazione: Grazie all'inferenza dei tipi di Rust e alle macro intelligenti, Filament richiede meno annotazioni manuali rispetto agli approcci precedenti, rendendo il codice più leggibile e simile al Rust standard.
4. Interoperabilità sicura: I macro fcall! e mcall! risolvono il problema della compatibilità con le librerie esistenti senza introdurre vulnerabilità legate alla declassificazione manuale.

4. Risultati dell'Valutazione

Gli autori hanno valutato Filament reimplementando quattro applicazioni esistenti da Cocoon (Calendar, Battleship, Spotify TUI, Servo) e un'applicazione Jif (JPMail).

• Carico di Annotazione: Filament richiede meno modifiche al codice sorgente rispetto a Cocoon. Ad esempio, in Battleship, Filament richiede 293 righe di codice contro le 315 di Cocoon. Il numero di chiamate API necessarie per gestire i flussi è significativamente inferiore.
• Permissività e Sicurezza: Filament ha eliminato 12 declassificazioni non necessarie e operazioni non controllate presenti nelle implementazioni di Cocoon. Questo riduce il rischio di fughe di informazioni accidentali. In particolare, Filament non richiede l'uso di unchecked_operation per funzioni che modificano dati locali all'interno di contesti sensibili, a differenza di Cocoon che imponeva blocchi rigidi.
• Overhead di Compilazione: L'overhead di compilazione è trascurabile. Per progetti grandi come Servo (327k righe) e Spotify TUI, l'aumento del tempo di compilazione è inferiore all'1% (spesso misurabile solo come fluttuazione). Per progetti piccoli, l'overhead è leggermente più alto in percentuale ma comunque accettabile.
• Compatibilità: Filament è compatibile con Rust stabile (versione 1.69+), a differenza di alcune implementazioni precedenti che richiedevano funzionalità instabili o modifiche al compilatore.

5. Significato

Filament rappresenta un passo avanti significativo nell'adozione pratica del controllo del flusso di informazioni nei linguaggi moderni. Dimostra che è possibile ottenere le garanzie formali e la precisione del modello Denning (che evita il problema del "label creep" e gestisce correttamente i flussi impliciti) senza sacrificare l'usabilità o richiedere un ecosistema di compilazione personalizzato.

Il lavoro suggerisce che l'approccio basato su librerie e macro, se progettato correttamente sfruttando le caratteristiche avanzate del linguaggio (come i tipi fantasma e l'inferenza), può superare i limiti dei sistemi a blocco (come Cocoon), offrendo agli sviluppatori un modello di programmazione più naturale, meno propenso a errori e più sicuro. Questo apre la strada all'integrazione di IFC robusto in progetti Rust su larga scala, come browser engine (Servo) o applicazioni di rete, dove la sicurezza dei dati è critica.