Avanzare nella sicurezza nella computazione multi-parte

La Computazione Sicura Multi-Parte (MPC) è uno strumento chiave per mantenere i dati privati nel nostro mondo interconnesso. Permette a diverse parti di lavorare insieme senza rivelare i propri dati privati l'uno all'altro. Però, dimostrare che questi protocolli MPC a basso livello sono sicuri spesso si basa su metodi manuali che possono essere complessi e soggetti a errori. Questo è un problema perché i metodi per verificare questi protocolli non sono standardizzati, rendendo difficile per molti esperti in linguaggi di programmazione lavorarci sopra.

Per semplificare questo processo, abbiamo creato un nuovo linguaggio di programmazione che aiuta a definire vari protocolli MPC a basso livello. Questo nuovo linguaggio include anche modi per controllare la Riservatezza e l'Integrità, due importanti caratteristiche di sicurezza. I controlli che proponiamo sono simili a quelli che si trovano nei modelli di flusso d'informazione tradizionali, che aiutano a garantire che informazioni sensibili non vengano diffuse. Mostriamo come il nostro nuovo linguaggio si colleghi con i modelli di sicurezza MPC standard e come possano essere utilizzati insieme per verificare più efficacemente la sicurezza di questi protocolli.

#Importanza della Programmazione MPC a Basso Livello

I linguaggi di programmazione ad alto livello sono progettati per aiutare a creare applicazioni complete. Si concentrano sul rendere la programmazione più facile ed efficace. Però, quando si parla di MPC, molti linguaggi ad alto livello usano protocolli a basso livello per gestire la condivisione e l'elaborazione dei dati. Questi protocolli a basso livello, che includono la condivisione segreta e altri metodi, richiedono una verifica manuale attenta. La sfida è che sono necessari sia design di linguaggi ad alto livello che a basso livello per garantire che i protocolli MPC siano sicuri.

L'interazione tra come scorrono le informazioni e quanto siano sicuri i protocolli MPC diventa complicata, specialmente a livello basso. In MPC, diversi client comunicano tra loro per calcolare e condividere risultati senza necessitare di una terza parte fidata. Questo processo di condivisione può rivelare involontariamente alcune informazioni sugli input privati, anche quando i risultati complessivi rimangono sicuri. La funzionalità ideale in MPC deve delineare una politica per gestire correttamente queste informazioni, e farlo può essere complicato.

#Panoramica dei Nostri Contributi

Questo lavoro introduce un sistema in tre parti per verificare i protocolli MPC:

1. Un nuovo linguaggio di programmazione a basso livello pensato per definire operazioni MPC di base.
2. Un modo automatizzato per verificare le operazioni MPC a basso livello in questo nuovo linguaggio.
3. Un metodo semi-automatizzato per controllare la sicurezza di protocolli MPC più grandi che si basano su queste operazioni a basso livello.

Inoltre, abbiamo definito un insieme di proprietà di sicurezza che potrebbero interessare gli esperti del settore.

#Design del Linguaggio per MPC

Abbiamo sviluppato un nuovo linguaggio di programmazione per aiutare a definire protocolli distribuiti. Questo linguaggio consente messaggi sincroni tra i client che fanno parte del protocollo. Abbiamo anche creato un metalanguage che genera protocolli dinamicamente. Questo dà ai programmatori la possibilità di esprimere concetti a basso livello facilmente.

La sintassi del nostro linguaggio di programmazione è semplice. Supporta operazioni standard come addizione, sottrazione e moltiplicazione all'interno di un campo finito. I client inviano messaggi e rivelano informazioni in un modo che si inserisce nel quadro di questo linguaggio. Questo rende più facile scrivere, capire e verificare i protocolli MPC.

#Modello di Sicurezza per MPC

I protocolli MPC mirano a fornire risultati senza rivelare più informazioni del necessario. Con il nostro nuovo modello di sicurezza, possiamo classificare gli output di questi protocolli in due tipi: reale e ideale. Il concetto chiave è che il protocollo reale non dovrebbe rivelare più informazioni di quelle che il modello ideale rivelerebbe nella stessa situazione.

In un modello di sicurezza di base, si presume che tutti i client seguano le regole dei protocolli. Possiamo dire che un protocollo è "corretto" se, per qualunque input fornito, produce l'output atteso senza rivelare informazioni aggiuntive. Questo livello di sicurezza passiva può essere definito probabilisticamente, usando funzioni matematiche che esprimono come le variabili di input e output si relazionano tra loro.

Quando consideriamo clienti malintenzionati-che decidono di infrangere le regole-introduciamo un modo per rilevare qualsiasi imbroglio che potrebbe avvenire. Questo aggiunge un ulteriore livello di sicurezza al nostro modello. I partecipanti onesti dovrebbero essere in grado di individuare questo comportamento scorretto e interrompere l'operazione se necessario.

#Proprietà di Sicurezza per MPC

Abbiamo creato varie proprietà di sicurezza per valutare la sicurezza dei protocolli MPC. Una proprietà chiave è nota come non interferenza condizionale, che sostiene che osservare i risultati del protocollo non dovrebbe fornire all'osservatore ulteriori informazioni sugli input privati che vengono condivisi.

Un'altra proprietà è il rilascio graduale. Questo significa che il protocollo dovrebbe rilasciare solo una piccola quantità di informazioni alla volta, mantenendo altri dettagli sensibili nascosti. Discutiamo anche della declassificazione robusta, che garantisce che anche se alcune informazioni vengono rivelate, rimangono entro limiti concordati predefiniti dal protocollo.

#Tecniche di Verifica per MPC

Per verificare la sicurezza dei protocolli MPC, abbiamo sviluppato metodi che ci permettono di determinare se certe proprietà siano vere. Questo processo di verifica può essere completamente automatizzato per protocolli semplici, mentre per quelli più complessi, un metodo semi-automatizzato può aiutare nella verifica.

I nostri metodi possono determinare la distribuzione di probabilità dei risultati provenienti da diverse esecuzioni del protocollo, consentendo controlli di sicurezza basati sui dati. Utilizzando questi approcci, possiamo verificare protocolli del mondo reale come quelli utilizzati in applicazioni focalizzate sulla privacy, come il voto sicuro o la condivisione di dati riservati.

#Implicazioni Pratiche e Lavoro Futuro

Il nuovo linguaggio di programmazione che abbiamo progettato, insieme alla nostra esplorazione delle proprietà di sicurezza, getta le basi per definire meglio i protocolli MPC a basso livello. Apre anche porte per migliorare la verifica della sicurezza. Ci sono molte aree che possiamo esplorare ulteriormente, che possono portare a strumenti e metodi migliori per garantire che questi protocolli siano sicuri e affidabili.

Un'area promettente per la ricerca futura è integrare le nostre tecniche di verifica con assistenti alla prova esistenti. Questo permetterebbe ai programmatori di scrivere protocolli più sicuri con meno sforzo. Inoltre, espandere il nostro linguaggio per gestire efficacemente la concorrenza ci permetterebbe di catturare più a fondo pratiche comuni di MPC, come la condivisione di impegni e l'ottimizzazione dei circuiti.

#Conclusione

Il nostro lavoro contribuisce a rendere la computazione sicura multi-parte più accessibile attraverso lo sviluppo di un linguaggio di programmazione specializzato e un processo di verifica sistematica. Concentrandosi sui protocolli a basso livello e integrando miglioramenti nel modo in cui gestiamo la sicurezza, puntiamo a migliorare il modo in cui i dati sensibili possono essere gestiti e protetti in ambienti collaborativi. Le intuizioni ottenute da questo lavoro possono aiutare a spianare la strada per metodi più sicuri ed efficienti nel campo in espansione della privacy dei dati.