Renaming or Tightness: Enforcing Disjunctive Information Flow Policies

Sintesi Tecnica: Rinomina o Precisione: L'imposizione di Politiche di Flusso di Informazioni Disgiuntive

Definizione del Problema
Le politiche di flusso di informazioni disgiuntive limitano un valore a dipendere al massimo da uno di due segreti, proibendo la combinazione di rilasci altrimenti ammissibili (ad esempio, un muro etico che impedisce a un rapporto di dipendere sia dai file del Cliente A che da quelli del Cliente B, o uno schema di condivisione di segreti che rilascia solo una quota). A differenza delle standard politiche basate su reticoli, dove il join di due dipendenze ammissibili è ammissibile, le politiche disgiuntive non hanno una forma a reticolo. Hunt e Sands hanno precedentemente fornito una semantica per queste politiche utilizzando il "quantale dell'informazione", dove la congiunzione è un tensore ($\otimes$) non idempotente anziché un join. Tuttavia, lo strato di enforcement — specificamente, ciò che un sistema di tipi sensibile al flusso può certificare riguardo a tali politiche — rimaneva un problema aperto.

La sfida centrale è che gli esistenti sistemi di tipi sensibili al flusso, che si affidano a un oggetto universale per consentire un'analisi indipendente dalla politica (tramite rinomina monotona), non riescono a preservare la precisione sotto politiche disgiuntive. Nello specifico, quando una sorgente viene letta due volte (ad esempio, un riepilogo usato sia in un'intestazione che in una tabella), i meccanismi standard perdono la correlazione che entrambe le letture rispettano lo stesso disgiunto. Di conseguenza, sovra-approssimano il flusso di informazioni, certificando che l'output riveli entrambi i segreti ($\top$) anche quando la politica è soddisfatta.

Metodologia
Gli autori costruiscono una famiglia di sistemi di tipi sensibili al flusso ($F_1$) su un quantale affine commutativo arbitrario $M$. L'analisi procede investigando l' "oggetto universale" dal quale tutti i sistemi specifici della politica si specializzano. Nell'era dei reticoli, l'insieme delle parti delle variabili serviva come singolo oggetto universale. Il documento dimostra che, su un quantale, questo oggetto si divide in tre candidati distinti, ciascuno con diverse proprietà riguardanti la precisione e la capacità di supportare la rinomina monotona:

1. L'Oggetto Multiset ($U_N$): Il monoide commutativo libero sulle variabili (gli elementi sono multiset). Supporta la piena rinomina monotona e le tipizzazioni principali, ma perde la "correlazione della stessa sorgente". Tratta due letture di una sorgente come due usi indipendenti, portando alla sovra-approssimazione ($\sigma(v) \otimes \sigma(v)$).
2. L'Oggetto Insieme ($U$): Il monoide commutativo idempotente libero (gli elementi sono insiemi di variabili, rappresentati come downset della powerset). Preserva la correlazione della stessa sorgente (due letture di una sorgente contano come una), ma rompe la proprietà oもmorfica richiesta per la rinomina monotona. La specializzazione qui è una sezione oplaxa, non un omoformismo.
3. Il Locale Libero ($L$): L'oggetto dell'era dei reticoli (insiemi di variabili con l'unione come combinazione), che è stretto per letture singole ma confonde la disgiunzione di ramo con la combinazione tensoriale, cancellando la distinzione tra "l'esecuzione A ha usato X, l'esecuzione B ha usato Y" e "alcuna esecuzione ha usato X e Y".

Il documento analizza i compromessi tra questi oggetti, dimostrando che nessun meccanismo della forma di "attributo indipendente" (dove gli ambienti mappano le variabili a singoli elementi del quantale) può supportare simultaneamente la rinomina monotona e ottenere limiti stretti per le politiche disgiuntive.

Contributi Chiave e Risultati

1. Famiglia di Sistemi di Tipi ($F_1$): Una famiglia di sistemi di tipi sicuri ancorata ai lemmi di composizione di Hunt e Sands. Gestisce i cicli utilizzando la chiusura idempotente del fattore di guardia, un aggiustamento necessario per i quantali che è invisibile nei reticoli.
2. La Scissione dell'Oggetto Universale: Il documento stabilisce una tricotomia:
   • Su $U_N$, l'intero meccanismo di tipizzazioni principali e completezza interna sopravvive incondizionatamente, ma il limite è debole per le sorgenti riutilizzate.
   • Su $U$, il limite è strettamente più preciso (registra che due letture rispettano un unico disgiunto), ma la specializzazione non è più un omoformismo, rompendo la proprietà di rinomina.
   • Su $L$, l'oggetto perde la disgiunzione di ramo, fallendo nel distinguere tra esecuzioni alternative ed esecuzioni combinate.
3. Impossibilità di Rinomina e Precisione: Gli autori dimostrano che per qualsiasi meccanismo di forma a attributo indipendente che supporti la rinomina monotona, il limite certificato per una sorgente riutilizzata sotto un'etichetta "satura" (dove $m \otimes m = \top$) è $\top$. Ciò significa che sotto etichette di tipo muro etico o condivisione di segreti, una seconda lettura di una sorgente non certifica nulla, causando il rifiuto di programmi che sono in realtà conformi alla politica.
4. La Riparazione (Specializzazione Differita): Per recuperare la precisione, il documento propone di differire la specializzazione al livello del giudizio. Invece di applicare la mappa di etichettatura all'ambiente (il che forza una struttura omoformica), la mappa viene applicata solo alla lettura finale (read-out).
   • Questo approccio utilizza l'Oggetto Insieme ($U$) per la tipizzazione e la mappa $\alpha_\sigma$ per la lettura.
   • La mappa di lettura risultante è provata essere la mappa meno sonora che preserva il join.
   • Questa "riparazione" sacrifica la capacità di presentare l'esito come una derivazione all'interno del sistema target (rinomina), ma ottiene il limite più stretto possibile per i meccanismi a attributo indipendente.
5. Decidibilità: Il documento mostra che il controllo di conformità è decidibile. Sebbene $U_N$ sia infinito, il limite specializzato dipende solo dalle molteplicità fino all'ordine dell'etichetta (ad esempio, 2 per i muri etici), permettendo una troncatura finita. $U$ è un reticolo finito, garantendo la terminazione.

Significato e Rivendicazioni
Il documento sostiene che la transizione da sistemi basati su reticoli a sistemi basati su quantali impone una scelta fondamentale che prima era nascosta: si può avere la rinomina monotona o la precisione, ma non entrambe.

• Per il Paradigma della Rinomina: Il documento dimostra che l'approccio dell' "oggetto universale", che consente di analizzare un programma una sola volta e riutilizzare il risultato per qualsiasi politica, incontra un tetto invalicabile. Per le politiche disgiuntive, questo tetto è così basso (spesso $\top$) da rendere il meccanismo inutile per scenari comuni come la condivisione di segreti o i muri etici, dove un valore viene usato più volte.
• Per la Precisione: Il documento fornisce una soluzione costruttiva (specializzazione differita) che recupera la precisione mancante. Dimostra che mantenendo il tipo universale nell'Oggetto Insieme ($U$) e applicando l'etichettatura solo alla fine, è possibile certificare programmi che il paradigma della rinomina rifiuta.
• Implicazione Pratica: La distinzione tra "una sorgente letta due volte" (sicura sotto politiche disgiuntive) e "due sorgenti lette una volta" (non sicura) è preservata solo dall'Oggetto Insieme ($U$). L'oggetto multiset (amico della rinomina) e l'oggetto locale (amico dei reticoli) falliscono entrambi nel distinguere correttamente questi casi nel contesto delle politiche disgiuntive.

Gli autori concludono che, mentre l'oggetto dell'era dei reticoli è un quoziente che perde la disgiunzione di ramo, e l'oggetto multiset perde la correlazione della stessa sorgente, l'Oggetto Insieme ($U$) è l'unico che mantiene entrambi. Il costo di questa precisione è la perdita della proprietà di rinomina, un compromesso che è necessario per l'enforcement di politiche disgiuntive. Il documento non pretende di risolvere il problema per le analisi relazionali o i meccanismi sensibili al percorso (che sono suggeriti come direzioni future in lavori correlati), ma caratterizza pienamente i limiti e le possibilità della famiglia a attributo indipendente.