EverCrypt: la prima libreria crittografica che non si può hackerare

EverCrypt è stato sviluppato e verificato dal team “Project Everest”, una collaborazione congiunta Microsoft-Accademia. Nasce dal perfetto connubio tra informatica e matematica e non è altro che una libreria crittografica in grado di garantire con “certezza matematica” che le comunicazioni saranno sicure.

È basato su un nuovo linguaggio di programmazione: F*, e include una suite completa di algoritmi che comprende cifrari a blocchi, curve ellittiche e funzioni hash. È stato sviluppato per offrire un’implementazione più solida di TLS, il protocollo che sottostà alle comunicazioni HTTPS (Hypertext Transfer Protocol Secure) protette su Internet, ma è stato progettato per essere utile per un’ampia gamma di software, dalla crittografia del disco alla messaggistica istantanea.

Le Librerie Crittografiche

EverCrypt è una libreria di software che gestisce la crittografia, o la codifica e la decodifica di informazioni private. Queste librerie crittografiche sono intrinsecamente matematiche. Comprendono l’aritmetica con numeri primi e operazioni su oggetti geometrici canonici come le curve ellittiche. Definire che cosa fanno le librerie crittografiche in termini formali non è un problema.

Il lavoro su EverCrypt è iniziato nel 2016 come parte del Project Everest, un’iniziativa guidata da Microsoft Research. All’epoca le librerie crittografiche erano un punto debole di molte applicazioni software, e lo sono ancora oggi. Erano lente, rallentando le prestazioni generali delle applicazioni di cui facevano parte, e piene di bachi.

Impossibile da Hackerare

I ricercatori, con EverCrypt, sono riusciti a dimostrare che il loro approccio alla sicurezza on-line è assolutamente invulnerabile ai principali tipi di attacchi hacker che hanno colpito altri programmi in passato. Tanto che EverCrypt si dichiara più sicuro della concorrenza poiché afferma di essere sicuro tanto quanto una risposta matematica che è dimostrabile e non può essere contestata.

“Quando diciamo dimostrazione, intendiamo dire che proviamo che il nostro codice non può subire questo tipo di attacchi”, ha dichiarato Karthik Bhargavan, informatico dell’Inria di Parigi che ha lavorato su EverCrypt.

Nella creazione di un software, generalmente i programmatori fanno in modo che questo sia in grado di soddisfare determinati obiettivi. Una volta terminata la fase di scrittura, il codice viene testato e se raggiunge gli obiettivi senza mostrare comportamenti indesiderati si conclude che il software fa ciò che deve fare. Tuttavia gli errori di codifica persistono e si possono manifestare in casi estremi rivelando vulnerabilità critiche del codice (e gli attacchi hacking sfruttano proprio queste evenienze).

“È un malfunzionamento a cascata, ed è difficile da trovare sistematicamente perché gli eventi che portano a esso, presi individualmente, sono tutti molto improbabili”, ha detto Bryan Parno, informatico della Carnegie Mellon University che ha lavorato su EverCrypt.

Al contrario EverCrypt si basa su una strategia chiamata “verifica formale”.

“È possibile ridurre la domanda su come si comporta il codice a una formula matematica e quindi è possibile verificare se la formula è valida. Se lo è, sai che il tuo codice ha quella proprietà”, ha detto Parno.

Sostanzialmente in primis viene specificato cosa deve fare il codice e poi si dimostra che effettivamente fa solo quello senza incappare in maniera imprevista in circostanze insolite. Poiché è praticamente impossibile specificare formalmente la funzione di software complessi come un browser web, i ricercatori si sono invece concentrati su programmi che sono critici e al tempo stesso che è possibile definire matematicamente.

Un linguaggio di programmazione di nuovo tipo: F*

EverCrypt è basato su un nuovo linguaggio di programmazione che pone la matematica e il software su un piano di parità.

“Puoi scrivere software come se fossi uno sviluppatore di software, ma allo stesso tempo puoi scrivere una dimostrazione come se fossi un teorico”.

Per questo è stata creata un’unica piattaforma di programmazione che congloba le capacità di un linguaggio software tradizionale come C++ e la sintassi logica e la struttura di programmi proof-assistant come Isabelle e Coq.

“Abbiamo unificato queste cose in un solo quadro coerente in modo che la distinzione tra scrivere programmi e fare dimostrazioni fosse davvero ridotta”, ha affermato Bhargavan.

Vantaggi notevoli

I vantaggi sono molteplici e in primo luogo i ricercatori affermano che EverCrypt sia privo di errori di codifica come i sovraccarichi del buffer che possono permettere gli attacchi hacking. E che esegue ogni volta la matematica crittografica giusta senza la possibilità di una computazione errata.

Tuttavia la garanzia più eclatante è che non permette che il contenuto di un messaggio crittografato venga dedotto semplicemente osservando come funziona il programma.

Per esempio, un osservatore potrebbe sapere che un algoritmo di crittografia viene eseguito un po’ più velocemente quando aggiunge “0” a un valore e un po’ più lentamente quando aggiunge “1”. Misurando la quantità di tempo che impiega un algoritmo per crittografare un messaggio, un osservatore potrebbe iniziare a capire se la rappresentazione binaria di un messaggio contiene più 0 o 1 e finire per dedurre il messaggio completo.

“Da qualche parte, nel profondo dell’algoritmo o nel modo in cui s’implementa l’algoritmo, si stanno perdendo informazioni, il che può vanificare completamente lo scopo dell’intera crittografia”, ha detto Bhargavan.

Tali “attacchi dal canale laterale” (side channel attack) sono stati alla base di alcune delle più famose operazioni di hacking degli ultimi anni, incluso l’attacco Lucky Thirteen. I ricercatori hanno dimostrato che EverCrypt non perde mai informazioni in modi che possono essere sfruttati da questi tipi di attacchi temporali (timing attack).

Il protocollo TLS

Inoltre le librerie crittografiche lavorano in modo adiacente ad altri programmi software come un sistema operativo o applicazioni desktop comuni che generalmente non sono verificate. Poiché la vulnerabilità di questi ultimi può intaccare una libreria crittografica, Project Everest punta a circondare EverCrypt con il software più verificato che può.

L’obiettivo generale è completare un’implementazione completamente verificata dell’HTTPS, il software che protegge la maggior parte delle comunicazioni web. E questo porterà ad una manciata di elementi software ognuno dei quali è verificato per funzionare da solo e tutti sono formalmente verificati per funzionare insieme.

Tuttavia, anche se EverCrypt si è dimostrato immune a molti tipi di attacchi, non inaugura un’età di software perfettamente sicuri. Ci saranno sempre attacchi a cui nessuno ha mai pensato prima: nei confronti di questi, non si può dimostrare che EverCrypt è sicuro, se non altro per il semplice motivo che nessuno sa come saranno.