AutoTam: Specifying Secure Protocol Implementations with Tamarin Model Generation

Problema
La verifica formale è fondamentale per garantire la sicurezza dei protocolli crittografici, tuttavia rimane una barriera significativa per i professionisti. Sebbene strumenti come Tamarin e ProVerif abbiano automatizzato gran parte del processo di verifica, persiste il divario tra i modelli simbolici di alto livello e le implementazioni concrete dei protocolli. Colmare questo divario richiede tradizionalmente una sostanziale competenza nei metodi formali per modellare manualmente le implementazioni o per interpretare i risultati della verifica per specifici codebase. Inoltre, gli approcci esistenti che estraggono modelli da linguaggi general-purpose impongono spesso vincoli restrittivi (come il divieto di cicli o ricorsione) per mantenere la trattabilità, lasciando parti della macchina a stati del protocollo alla gestione di assunzioni manuali. Questa limitazione è problematica, poiché vulnerabilità storiche (ad esempio, SKIP) sono derivate da macchine a stati implementate in modo errato. Inoltre, il trasferimento dei risultati di verifica alle implementazioni concrete manca di una connessione automatizzata e fondata, richiedendo una conoscenza esperta per garantire che una proprietà provata in un modello simbolico si applichi effettivamente al codice in esecuzione.

Metodologia
Gli autori presentano AutoTam, un nuovo approccio "language-first" che integra l'implementazione del protocollo, la generazione del modello simbolico e l'esecuzione simbolica dinamica. Il nucleo della metodologia è un linguaggio specifico per il dominio (DSL) progettato appositamente per i protocolli crittografici.

1. Linguaggio AutoTam: Il linguaggio è progettato per allinearsi al livello di astrazione delle proprietà di sicurezza di alto livello pur rimanendo eseguibile. Modella i protocolli come macchine a stati finiti in cui i ruoli consistono in stati (divisi in parti di output e di input) e transizioni. Il linguaggio restringe il controllo del flusso al livello della macchina a stati del protocollo per garantire la decidibilità durante la traduzione, evitando problemi di raggiungibilità indecidibili. Supporta macchine a stati arbitrarie, inclusi i cicli necessari per le fasi di trasporto, ma limita le scelte intra-procedurali affinché facciano parte della logica della macchina a stati.
2. Interprete ed Esecuzione: AutoTam include un interprete che esegue le descrizioni dei protocolli direttamente. Ciò consente l'interoperabilità con le implementazioni esistenti (ad esempio, WireGuard). L'interprete utilizza una tabella di lookup per funzioni predefinite (I/O di rete, operazioni crittografiche come ChaCha20-Poly1305, Ed25519 e Blake2s) implementate tramite la libreria formalmente verificata HACL.
3. Traduzione Fondata verso Tamarin: Gli autori hanno sviluppato una procedura di traduzione che converte le descrizioni dei protocolli AutoTam in modelli Tamarin. La traduzione mappa le transizioni estese (combinando l'input dello stato sorgente, la logica di transizione e l'output dello stato target) in singole regole di rewrite di Tamarin. Gli autori forniscono una prova formale di soundness (fondatezza), dimostrando che qualsiasi proprietà di traccia provata nel modello Tamarin generato si applica all'esecuzione concreta dell'implementazione AutoTam sotto il modello Dolev-Yao. Ciò garantisce che i risultati della verifica siano direttamente applicabili all'implementazione.
4. Integrazione dell'Esecuzione Simbolica: Per affrontare la sicurezza della memoria e gli errori a livello di implementazione, AutoTam si integra con il motore di esecuzione simbolica dinamica KLEE. L'interprete viene compilato in bytecode LLVM e le funzioni crittografiche vengono sostituite con astrazioni simboliche. Ciò consente l'esplorazione sistematica dei percorsi di esecuzione sotto input di rete arbitrari, escludendo errori di memoria come i buffer overflow.

Contributi Chiave

• Linguaggio AutoTam: Un linguaggio specifico per il dominio, completamente eseguibile, per i protocolli crittografici che codifica naturalmente macchine a stati, parsing di messaggi e operazioni crittografiche.
• Estrazione del Modello Fondata: Una procedura per estrarre modelli Tamarin da implementazioni eseguibili, accompagnata da una prova formale di soundness riguardo alle proprietà di traccia. Ciò garantisce che le proprietà di traccia universali verificate nel modello si traducano nuovamente nell'implementazione.
• Esecuzione Simbolica Integrata: Un workflow completamente integrato che utilizza KLEE per analizzare le implementazioni AutoTam per la sicurezza della memoria, fornendo test di copertura completi contro input di rete arbitrari.
• Case Studies: L'implementazione e la verifica di due protocolli:
  • Un protocollo di scambio di chiavi Diffie-Hellman firmato.
  • Il protocollo VPN WireGuard.
    Gli autori dimostrano che la loro implementazione di WireGuard è interoperabile con le attuali implementazioni del kernel Linux e Go e raggiunge prestazioni accettabili.

Risultati

• Efficienza della Verifica: Lo strumento ha generato modelli Tamarin per entrambi i casi di studio in meno di 1 secondo. Il protocollo Diffie-Hellman è stato verificato per tutte le proprietà di sicurezza (segretezza, autenticazione) in meno di 5 secondi.
• Verifica di WireGuard: La verifica del modello WireGuard ha richiesto l'aggiunta manuale di un "sources lemma" per guidare il prover, un requisito comune per protocolli complessi in Tamarin. Nonostante ciò, il modello generato è stato verificato con successo per le proprietà di handshake (debole segretezza e accordo iniettivo) in circa 360 secondi.
• Fedeltà del Modello: Il modello WireGuard generato ha catturato più dettagli rispetto a diversi modelli scritti da esperti, incluso il modeling esplicito dei passaggi HKDF e della decrittazione/validazione AEAD, che sono spesso astratti in altri lavori.
• Sicurezza della Memoria: L'analisi dell'esecuzione simbolica ha esplorato con successo migliaia di percorsi di esecuzione per entrambi i protocolli (ad esempio, 4.120 percorsi per il responder di WireGuard) e non ha riscontrato errori di memoria, escludendo efficacemente buffer overflow e bug simili di implementazione.
• Prestazioni: L'implementazione di WireGuard basata sull'interprete di AutoTam ha raggiunto un throughput comparabile all'implementazione ufficiale di WireGuard in Go quando eseguita su hardware identico, nonostante la mancanza di ottimizzazioni low-level specifiche.

Significatività
L'articolo sostiene che AutoTam offra un percorso semplificato verso lo sviluppo di protocolli sicuri, minimizzando la necessità di competenza in verifica formale durante la fase di implementazione. Legando il linguaggio di implementazione direttamente al modello simbolico, l'approccio garantisce che scrivere l'implementazione del protocollo in AutoTam generi in gran parte un modello "pronto per la verifica" gratuitamente. La proprietà di soundness è centrale per questa affermazione, poiché colma il divario tra la verifica astratta e l'esecuzione concreta, permettendo agli sviluppatori di fare affidamento su prove formali per la sicurezza dell'implementazione. Inoltre, l'integrazione dell'esecuzione simbolica fornisce un doppio livello di garanzia: la verifica formale della logica del protocollo e il rilevamento automatico degli errori di memoria a livello di implementazione. Gli autori posizionano questo lavoro come un passo significativo verso il miglioramento dell'adozione dei metodi formali nell'industria, riducendo la barriera della competenza e garantendo che il modello verificato rifletta accuratamente il codice in esecuzione.