Quasi ogni volta che apri un browser Google Chrome sicuro, un nuovo sistema crittografico sviluppato dal MIT aiuta a proteggere meglio i tuoi dati.

In un documento presentato al recente IEEE Symposium on Security and Privacy, I ricercatori del MIT descrivono in dettaglio un sistema che, per la prima volta, genera automaticamente un codice di crittografia ottimizzato che di solito è scritto a mano. Distribuito all'inizio del 2018, il sistema è ora ampiamente utilizzato da Google e da altre aziende tecnologiche.

Il documento ora dimostra ad altri ricercatori nel campo come possono essere implementati metodi automatizzati per prevenire errori commessi dall'uomo nella generazione di criptocodice, e come le modifiche chiave ai componenti del sistema possono aiutare a ottenere prestazioni più elevate.

Per proteggere le comunicazioni online, i protocolli crittografici eseguono algoritmi matematici complessi che eseguono operazioni aritmetiche complesse su grandi numeri. Dietro le quinte, però, un piccolo gruppo di esperti scrive e riscrive questi algoritmi a mano. Per ogni algoritmo, devono pesare varie tecniche matematiche e architetture di chip per ottimizzare le prestazioni. Quando la matematica o l'architettura sottostante cambia, essenzialmente ricominciano da zero. Oltre ad essere laborioso, questo processo manuale può produrre algoritmi non ottimali e spesso introduce bug che vengono successivamente rilevati e corretti.

I ricercatori del Computer Science and Artificial Intelligence Laboratory (CSAIL) hanno invece progettato "Fiat Cryptography, " un sistema che genera automaticamente e contemporaneamente verifica algoritmi crittografici ottimizzati per tutte le piattaforme hardware. Nei test, i ricercatori hanno scoperto che il loro sistema può generare algoritmi che corrispondono alle prestazioni del miglior codice scritto a mano, ma molto più veloce.

Il codice generato automaticamente dai ricercatori ha popolato BoringSSL di Google, una libreria crittografica open source. Google Chrome, app Android, e altri programmi utilizzano BoringSSL per generare le varie chiavi e certificati utilizzati per crittografare e decrittografare i dati. Secondo i ricercatori, circa il 90% delle comunicazioni sicure di Chrome attualmente esegue il proprio codice.

"La crittografia viene implementata facendo aritmetica su grandi numeri. [Fiat Cryptography] rende più semplice l'implementazione degli algoritmi matematici ... perché automatizziamo la costruzione del codice e forniamo prove che il codice è corretto, ", afferma il coautore della carta Adam Chlipala, ricercatore CSAIL e professore associato di ingegneria elettrica e informatica e responsabile del gruppo Linguaggi di programmazione e verifica. "In pratica è come prendere un processo che è stato eseguito nel cervello umano e comprenderlo abbastanza bene da scrivere un codice che imiti quel processo".

Jonathan Protzenko di Microsoft Research, un esperto di crittografia che non era coinvolto in questa ricerca, vede il lavoro come un cambiamento nel modo di pensare del settore.

"La crittografia Fiat utilizzata in BoringSSL avvantaggia l'intera comunità [crittografica], " dice. "[È] un segno che i tempi stanno cambiando e che i grandi progetti software si stanno rendendo conto che la crittografia non sicura è una responsabilità, [e mostra] che il software verificato è abbastanza maturo per entrare nel mainstream. È mia speranza che sempre più progetti software consolidati passino alla crittografia verificata. Forse nei prossimi anni, il software verificato diventerà utilizzabile non solo per algoritmi crittografici, ma anche per altri domini applicativi."

Ad unirsi a Chlipala sulla carta sono:il primo autore Andres Erbsen e i co-autori Jade Philipoom e Jason Gross, chi sono tutti laureati CSAIL; così come Robert Sloan MEng '17.

Dividere i bit

I protocolli di crittografia utilizzano algoritmi matematici per generare chiavi pubbliche e private, che sono fondamentalmente una lunga serie di bit. Gli algoritmi utilizzano queste chiavi per fornire canali di comunicazione sicuri tra un browser e un server. Una delle famiglie di algoritmi crittografici più popolari efficienti e sicure è chiamata crittografia a curva ellittica (ECC). Fondamentalmente, genera chiavi di varie dimensioni per gli utenti scegliendo punti numerici a caso lungo una linea curva numerata su un grafico.

La maggior parte dei chip non può memorizzare numeri così grandi in un unico posto, quindi li dividono brevemente in cifre più piccole che vengono memorizzate su unità chiamate registri. Ma il numero di registri e la quantità di spazio di archiviazione che forniscono varia da un chip all'altro. "Devi dividere i bit in un mucchio di posti diversi, ma si scopre che il modo in cui dividi i bit ha diverse conseguenze sulle prestazioni, "dice Chlipala.

Tradizionalmente, gli esperti che scrivono algoritmi ECC implementano manualmente quelle decisioni di suddivisione dei bit nel loro codice. Nel loro lavoro, i ricercatori del MIT hanno sfruttato queste decisioni umane per generare automaticamente una libreria di algoritmi ECC ottimizzati per qualsiasi hardware.

I loro ricercatori hanno prima esplorato le implementazioni esistenti di algoritmi ECC scritti a mano, nei linguaggi di programmazione C e assembly, e ha trasferito quelle tecniche nella loro libreria di codici. Questo genera un elenco di algoritmi con le migliori prestazioni per ogni architettura. Quindi, utilizza un compilatore, un programma che converte i linguaggi di programmazione in codice che i computer comprendono, che è stato dimostrato corretto con uno strumento di verifica, chiamato Coq. Fondamentalmente, tutto il codice prodotto da quel compilatore sarà sempre verificato matematicamente. Quindi simula ogni algoritmo e seleziona quello con le prestazioni migliori per ogni architettura di chip.

Prossimo, i ricercatori stanno lavorando su come rendere il loro compilatore ancora più veloce nella ricerca di algoritmi ottimizzati.

Compilazione ottimizzata

C'è un'ulteriore innovazione che garantisce che il sistema selezioni rapidamente le migliori implementazioni di suddivisione dei bit. I ricercatori hanno dotato il loro compilatore basato su Coq di una tecnica di ottimizzazione, chiamato "valutazione parziale, " che fondamentalmente precalcola determinate variabili per accelerare le cose durante il calcolo.

Nel sistema dei ricercatori, precalcola tutti i metodi di suddivisione dei bit. Quando li si abbina a una determinata architettura di chip, scarta immediatamente tutti gli algoritmi che semplicemente non funzioneranno per quell'architettura. Ciò riduce drasticamente il tempo necessario per la ricerca nella libreria. Dopo che il sistema si è azzerato sull'algoritmo ottimale, finalizza la compilazione del codice.

Da quello, i ricercatori hanno quindi accumulato una libreria dei modi migliori per dividere gli algoritmi ECC per una varietà di architetture di chip. Ora è implementato in BoringSSL, quindi gli utenti attingono per lo più dal codice dei ricercatori. La libreria può essere aggiornata automaticamente in modo simile per nuove architetture e nuovi tipi di matematica.

"Abbiamo essenzialmente scritto una libreria che, una volta per tutte, è corretto per ogni modo in cui puoi eventualmente dividere i numeri, " dice Chlipala. "Si può esplorare automaticamente lo spazio delle possibili rappresentazioni dei grandi numeri, compilare ogni rappresentazione per misurare le prestazioni, e prendi quello che corre più veloce per un dato scenario."

Questa storia è stata ripubblicata per gentile concessione di MIT News (web.mit.edu/newsoffice/), un popolare sito che copre notizie sulla ricerca del MIT, innovazione e didattica.