Una crittografia che non si può hackerare
Computer hacker, conceptual image
Dall’unione di informatica e matematica è nato EverCrypt, il primo codice software in grado di resistere a ogni tipo di cyberattacco. O almeno, a tutti quelli che sono stati concepiti finora.
I programmatori sono umani, ma la matematica è immortale. Rendendo la programmazione più matematica, una comunità di informatici spera di eliminare gli errori di programmazione che possono aprire le porte agli hacker, far trapelare i segreti digitali e minacciare in generale la società moderna.
Un gruppo di informatici ha compiuto un passo importante verso questo obiettivo con la pubblicazione di EverCrypt, un insieme di strumenti di crittografia digitale. I ricercatori sono riusciti a dimostrare – nello stesso senso in cui si dimostra il teorema di Pitagora – che il loro approccio alla sicurezza on-line è assolutamente invulnerabile ai principali tipi di attacchi hacker che hanno colpito altri programmi in passato. “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.
Una crittografia che non si può hackerare
EverCrypt non è stato scritto come la maggior parte dei codici. Di solito, un team di programmatori crea un software sperando che possa soddisfare determinati obiettivi. Quando hanno finito, testano il codice. Se raggiunge gli obiettivi senza mostrare comportamenti indesiderati, i programmatori concludono che il software fa ciò che deve fare.
Tuttavia, gli errori di codifica si manifestano spesso solo in casi estremi, i cosiddetti “corner cases”: una tempesta perfetta di eventi improbabili che rivela una vulnerabilità critica. Molti degli attacchi di hacking più dannosi negli ultimi anni hanno sfruttato proprio questi genere di 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, Parno e colleghi hanno prima specificato esattamente che cosa dovrebbe fare il loro codice e poi hanno dimostrato che fa quello e solo quello, escludendo la possibilità che possa deviare in modi imprevisti in circostanze insolite. La strategia generale è 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.
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.
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. “Penso che gli sviluppatori di app abbiano capito che il disastro è dietro l’angolo”, ha dichiarato Jonathan Protzenko, informatico della Microsoft Research che ha lavorato su EverCrypt. “Il mondo del software è maturo per qualcosa di nuovo che offra le garanzie di EverCrypt”.
La principale sfida per la creazione di EverCrypt era lo sviluppo di un’unica piattaforma di programmazione in grado di esprimere tutti i diversi attributi che i ricercatori volevano da una libreria crittografica verificata.
Typing on a laptop computer.
La piattaforma aveva bisogno della capacità di un linguaggio software tradizionale come C++ e della sintassi logica e della struttura di programmi proof-assistant come Isabelle e Coq, che i matematici usano da anni. Quando i ricercatori hanno iniziato a lavorare su EverCrypt, non esisteva alcuna piattaforma che contenesse tutte queste caratteristiche, quindi ne hanno sviluppata una: un linguaggio di programmazione chiamato F*, che mette la matematica e il software su un piano di parità.
“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. “Puoi scrivere software come se fossi uno sviluppatore di software, ma allo stesso tempo puoi scrivere una dimostrazione come se fossi un teorico”.
La loro nuova libreria crittografica offre una serie di garanzie di sicurezza. I ricercatori hanno dimostrato che EverCrypt è privo di errori di codifica, come i sovraccarichi del buffer, che possono permettere gli attacchi di hacking – in effetti, escludendo in modo accettabile la vulnerabilità a tutti i casi possibili. Hanno anche dimostrato che EverCrypt fa la matematica crittografica giusta ogni volta – non esegue mai la computazione errata.
Ma la garanzia più eclatante di EverCrypt riguarda una classe completamente diversa di punti deboli della sicurezza, che si evidenziano quando un malintenzionato deduce il contenuto di un messaggio crittografato semplicemente osservando come funziona un 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).
Tuttavia, anche se EverCrypt si è dimostrato immune a molti tipi di attacchi, non inaugura un’eta di software perfettamente sicuro. Protzenko sottolinea che 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.
Inoltre, anche una libreria crittografica verificata deve lavorare di concerto con una serie di altri software, come un sistema operativo e molte applicazioni desktop comuni, che in genere non sono verificati e probabilmente non lo saranno per il prossimo futuro. “Non miriamo a qualcosa di complesso come un word processor o un client Skype”, ha detto Protzenko, perché non è ovvio come si possa catturare in un linguaggio formale ciò che dovrebbero fare. “È difficile pensare al comportamento previsto di quelle cose”.
Poiché le vulnerabilità nei programmi adiacenti non verificati può compromettere una libreria crittografica, Project Everest punta a circondare EverCrypt con il software più verificato che può. L’obiettivo generale dell’iniziativa è completare un’implementazione completamente verificata dell’Hypertext Transfer Protocol Secure (HTTPS), il software che protegge la maggior parte delle comunicazioni web. Ciò comporterà una manciata di singoli elementi software come EverCrypt, ognuno dei quali è formalmente verificato per funzionare da solo e tutti sono formalmente verificati per funzionare insieme.
“Il progetto Everest sta cercando di costruire una stratificazione più grande di software tutti verificati per funzionare insieme in modo verificato. Col passare del tempo, speriamo che la frontiera del software verificato continui a crescere”, ha affermato Parno.
(L’originale di questo articolo è stato pubblicato il 2 aprile 2019 da QuantaMagazine.org, una pubblicazione editoriale indipendente online promossa dalla Fondazione Simons per migliorare la comprensione pubblica della scienza. Traduzione ed editing a cura di Le )
di Kevin Hartnett/Quanta Magazine
Fonte:
