EverCrypt: un nuovo servizio crittografico (quasi) inattaccabile

EverCrypt è la libreria crittografica sviluppata dai ricercatori dell’Istituto Statale di Informatica e Ricerca (INRIA), Microsoft Research e Carnegie Mellon University nell’ambito del progetto Everest che dovrebbe fornire nuove e più sicure forme di crittografia e di protezione, così da poter ristabilire la piena fiducia nell’utilizzo dello scambio di dati e delle transazioni online.

EverCrypt nasce per rispondere ad una necessità reale: Internet è un gigantesco mondo virtuale in continua espansione e, per quanto lo sforzo dei ricercatori e degli addetti al settore sia constantemente teso a renderlo sempre più sicuro e di facile utilizzo, esso è ancora pervaso da innumerevoli e preoccupanti vulnerabilità.

EverCrypt, per essere più sicuri

Uno dei protocolli più importanti ed utilizzati per navigare in internet, attraverso il browser, è HTTP (HyperText Transfer Protocol). Nato dallo straordinario lavoro di Tim Berners-Lee nell’anno 1989 é stato il principale “responsabile” per la straordinaria espansione, sia tecnologica che economica, del mondo virtuale.

Purtroppo, con la rapida diffusione degli scambi commerciali ci si è presto resi conto della debolezza strutturale di questo protocollo e dell’impellente necessità di proteggere gli utenti da frodi informatiche effettuate attraverso transazioni insicure.

Nasce cosi il protocollo HTTPS (Hypertext Transfer Protocol Secure), un protocollo di trasferimento dati basato sulla crittografia, che avrebbe dovuto porre rimedio alle vulnerabilità evidenziate in precedenza.

Sfortunatamente, gli ultimi devastanti attacchi come Heartbleed, Poodle, Beast e Crime ai danni di HTTPS e dei servizi crittografici SSL/TLS sul quale sono basati i meccanismi di protezione, hanno causato danni per milioni di euro ed hanno minato, ancora una volta, la fiducia riposta dai naviganti in questa tecnologia.

Come nasce EverCrypt e come è strutturata

Storicamente, scrivere una libreria crittografica di alta qualità, affidabile e che garantisca alte prestazioni, è stato un compito molto difficile. Per soddisfare le esigenze e le aspettative dei programmatori e delle moderne applicazioni e piattaforme, una libreria crittografica dovrebbe possedere alcune funzioni principali come:

• comprensibilità: gli sviluppatori desiderano un’unica libreria che copra tutte le funzionalità di cui avranno bisogno come crittografia, firma asimmetrica e simmetrica, hashing e derivazione delle chiavi;
• agilità: una moderna libreria crittografica dovrebbe fornire più ampio set di algoritmi per la stessa funzionalità e tutti dovrebbero impiegare una singola API unificata per semplificare la modifica nel caso sia necessario modificare il codice;
• funzionalità multiplexing: la libreria dovrebbe supportare il multiplexing ma fare queste scelte automaticamente piuttosto che forzare lo sviluppatore a farlo;
• performance: scritta in linguaggi low-level in modo da riuscire ad ottemperare alle prestazioni richieste su piattaforme di ogni genere e distribuite;
• sicurezza: la libreria dovrebbe presentare standard di sviluppo e garanzie verificabili per la riduzione dei bug e gli errori di programmazioni.

Sfruttando le peculiarità di alcuni linguaggi di programmazione e basansosi sulle precedenti implementazioni di servizi e librerie crittografiche, gli sviluppatori del progetto Everest hanno realizzato EverCrypt tentando di inglobare tutte le caratteristiche appena elencate, mantenendo le necessarie garanzie crittografiche indipendentemente dall’implementazione, dalla piattaforma o dall’algoritmo utilizzato.

In sostanza, EverCrypt combina due progetti lanciati dalla piattaforma Everest che sono: HACL * e Vale-Crypto, fornendo la possibilità di usare una API unificata.

La libreria HACL * è una libreria crittografica scritta usando il linguaggio Low * ed il compilatore KreMLin. I programmi scritti in questo modo compilano un codice C leggibile e idiomatico, così da renderli molto efficaci nella programmazione a basso livello e che possono contare su librerie crittografiche ad alta sicurezza. Questa libreria mira a fornire crypto-primitives da usare attraverso delle API in stile libsodium o NaCL (Networking and Cryptography library).

La libreria Vale-Crypto (Verified Assembly Language for Everest) è scritta sostanzialmente in codice Assembly, usando il ValeTool per la costruzione di codice ad alte prestazioni e formalmente verificato, con particolare attenzione al codice crittografico.

Vale-Tool, inoltre, supporta diverse architetture come: x86, x64 ed ARM, ed è compatibile con le principali piattaforme come Windows, Mac e Linux.

La prima versione di EverCrypt presenta implementazioni verificate dei seguenti algoritmi crittografici che vengono proposti in versioni C o assembler (quando si utilizza la libreria, viene automaticamente scelta l’implementazione ottimale per la piattaforma corrente):

• Algoritmi di hash: tutte le varianti di SHA2, SHA3, SHA1 e MD5;
• Codici di autenticazione: HMAC su SHA1, SHA2-256, SHA2-384 e SHA2-512 per l’autenticazione dell’origine dati;
• Algoritmo di generazione chiavi HKDF (funzione di derivazione chiave di estrazione ed espansione basata su HMAC);
• Chacha20 stream cipher (versione C non ottimizzata disponibile);
• Message Authentication Algorithm (MAC) Poly1305 (versione C e assembler), Protocollo Diffie-Hellman, Curve25519 (versioni in C e assemblatore con ottimizzazioni basate su istruzioni BMI2 e ADX). Modalità di crittografia blocco AEAD (crittografia autenticata) Chach Algoritmi supportati da EverCrypt.

Essendo un progetto giovane EverCrypt è comunque da considerarsi un work in progress. Molti algoritmi sono ancora in fase di sviluppo. Nelle prossime versioni, si mira ad includere maggiori features e miglioramenti. Alcuni degli algoritmi supportati da EverCrypt (l’elenco completo è riportato in figura) sono i seguenti:

• versioni di fallback C per tutti gli algoritmi;
• Curve NIST P;
• AES-CBC;
• un Ed25519 aggiornato.

Ogni distribuzione di EverCrypt contiene un Makefile GNU che genera una libreria statica e un oggetto condiviso. Il codice dipende da kremlib, che contiene implementazioni C verificate ed estratte da alcune funzioni della libreria standard F *.

Quando si integra EverCrypt, si può scegliere una distribuzione, insieme alla directory kremlib, dando così un’integrazione della libreria EverCrypt.

Per un’integrazione più graduale, i programmatori possono integrare gli algoritmi uno alla volta, selezionando i file e le funzioni a cui sono interessati. Verificare e creare EverCrypt da zero è abbastanza complicato e richiede diversi strumenti. Quindi l’approccio più semplice è quello di cercare il tag più recente usando il contenitore Docker HACL *, per poi recuperarlo utilizzando il comando Docker relativo.

Tutti i vantaggi della nuova libreria EverCrypt

Alcuni dei problemi principali che si riscontrano sia in fase di realizzazione che durante l’utilizzo delle librerie crittografiche, spesso sono il risultato di implementazioni estremamente complesse, progettate per ottenere il massimo delle prestazioni. Proprio per questo, EverCrypt utilizza metodi matematici di verifica formale dell’affidabilità crittografica.

Con le sue capacità e prestazioni è molto vicina alle librerie crittografiche esistenti (ad esempio, OpenSSL), ma a differenza di esse fornisce ulteriori garanzie di affidabilità e sicurezza.

Il processo di verifica si basa sulla definizione di specifiche dettagliate che descrivono tutto il comportamento del programma e forniscono una prova matematica che il codice scritto è pienamente conforme alle specifiche dettate.

A differenza dei metodi di controllo di qualità basati sulla programmaticità dei test, la verifica approntata con metodi analitici fornisce garanzie affidabili che l’applicazione basata su EverCrypt verrà eseguita esclusivamente come disegnato dagli sviluppatori, riducendo drasticamente o in alcuni casi eliminando del tutto possibili errori e conseguenti vulnerabilità.

Ad esempio, la conformità con le specifiche architetturali garantisce che le porzioni di memoria coinvolte nella gestione di servizi crittografici lavorino con una quasi totale assenza di errori e che dunque possano evitare vulnerabilita derivanti dal Buffer Overrun, attraverso puntatori di dereferenziamento, all’accesso alle aree di memoria già liberate o durante la liberazione dei blocchi di memoria.

EverCrypt offre un controllo accurato dei tipi di variabili e dei valori attribuiti, assicurando che vengano rispettati i parametri stabiliti, e che l’accesso ai servizi gestiti non possa essere effetuato da parte di quelle componenti che non soddisfano i requisiti prestabiliti.

Per proteggersi dagli attacchi side-channel, il comportamento durante i calcoli (ad esempio, la durata dell’esecuzione o la presenza di accessi a una determinata memoria) non dipende dalla natura dei dati segreti elaborati.

Tutti i possibili contro della nuova libreria crittografica

Sfortunatamente, rimangono alcune piccole lacune nella nuova libreria crittografica EverCrypt: ad esempio, il toolkit utilizzato nello sviluppo rimane non verificato, compresa la possibile esistenza non del tutto verificata di bug nel linguaggio F * o nel compilatore KreMLin e nei compilatori per la creazione di codice C (se non si utilizza un CompCert verificato).

È ipotizzabile, inoltre, che in qualche modulo non verificato correttamente ci possano essere vulnerabilita nascoste e pertanto il team di sviluppo di EverCrypt consiglia un audit approfondito e dei test delle specifiche, prima di procedere alla creazione di versioni ottimizzate dell’applicazione finale basata sulla nuova libreria crittografica.

Un altro problema che potrebbe essere fonte di vulnerabilità di tipo Side-channel è che i modelli di verifica utilizzati non tengono conto di minacce come Spectre e Meltdown e non proteggono da nuove classi di attacchi ancora sconosciuti che potrebbero apparire in futuro.

Conclusioni

EverCrypt propone una metodologia di risoluzione di alcune classi di vulnerabilità riscontrabili nelle componenti che costituiscono il fondamento dello sviluppo di applicazioni, che recentemente sembrano essere fonte di spunti per imprevisti attacchi da parte dei criminal hacker.

In particolare, ciò avviene utilizzando un approccio matematico di verifica costante dei processi, delle variabili, dei valori e dei metodi, puntando inoltre alla riduzione di quelle vulnerabilità che affliggono l’allocazione di porzioni di memoria con le quali è possibile vanificare il lavoro fatto per garantire applicazioni e servizi sicuri.

Tentando, ovviamente, di non tralasciare altri aspetti, come quello delle prestazioni, che rimangono di fondamentale importanza per tutte le applicazioni che sfruttano librerie e servizi crittografici.

Alcune parti del codice preparate dal progetto sono già utilizzate in Firefox, nel kernel di Windows, nella blockchain di Tezos e nella VPN Wireguard: ci si attende, dunque, un crescente utilizzo di EverCrypt ed un maggior incremento di sicurezza nelle future applicazioni.