Model checking per l’analisi di un algoritmo di autenticazione a chiave pubblica

Università degli Studi dell'Insubria

Dipartimento di Scienze Teoriche e Applicate

Corso di Laurea in Informatica

Il model checking per l'analisi di un algoritmo di autenticazione a chiave pubblica

Relatore: Brunella Gerla

Tesi di Laurea di: Jennifer Sculco

Matricola Nr. 722306

Anno Accademico 2021/2022

Indice

• Introduzione al model checking
• Il caso Therac-25
• Il caso dell'aeroporto di Denver
• Il Pentium FDIV Bug
• Il caso AT&T telephone network outage
• L’Ariane 5
• Model Checking
• Vantaggi e svantaggi del Model Checking
• Le logiche Model-Based
• Transition Systems
• LTL: Logica temporale lineare
• Sintassi
• Semantica
• L’esempio della "Mutual Exclusion"
• Symbolic Model Checking
• Linguaggio di modellazione PROMELA
• Spin
• SMV e NuSMV
• Branching Time Logic
• CTL: Logica dell’albero computazionale (Computation Tree Logic)
• Sintassi
• Semantica
• L’esempio della "Mutual Exclusion"
• CTL e LTL: due logiche non confrontabili
• Analisi del protocollo crittografico
• Descrizione del protocollo
• Model Checking per i protocolli di sicurezza
• Promela nel model checking del protocollo
• Conclusioni e considerazioni future

Bibliografia

Introduzione al model checking

It is fair to state, that in this digital era correct systems for information processing are more valuable than gold. H. Barendregt. The quest for correctness. 1996

Nella nostra società e nella nostra vita quotidiana ci confrontiamo sempre di più con la tecnologia dell'informazione in modo esplicito tramite PC, Internet, Personal Digital Assistant, ecc. e in modo implicito utilizzando dispositivi come televisori, rasoi elettrici, telefoni cellulari, automobili, mezzi pubblici e così via.

Nel 1995 è stato stimato che le persone sono in contatto con circa 25 "dispositivi di elaborazione delle informazioni" al giorno. A causa dell'elevata integrazione della tecnologia in tutti i tipi di applicazioni, si stima che il 20% dei costi totali di sviluppo di dispositivi di trasporto come automobili, treni e aeroplani siano dovuti a componenti basati su computer.

Al giorno d'oggi, facciamo sempre più affidamento sull'attendibilità dei componenti software e hardware. Questi ultimi sono talmente tanto utilizzati da vedere il loro fallimento come inconcepibile: non accettiamo che il nostro telefono cellulare non funzioni correttamente o che il nostro televisore reagisca in modo imprevisto e sbagliato ai comandi che emettiamo tramite le unità di controllo remoto.

Per evitare errori e malfunzionamenti di questi dispositivi, ci sono delle tecniche di verifica importanti quali:

• La simulazione
• Il testing
• La verifica formale
• Il model checking

La simulazione è un modello astratto del sistema che viene simulato includendo sia dati di input che eventi esterni. La simulazione non può essere eseguita per sempre e molte volte è più lenta del sistema reale. Inoltre, non ha nessuna garanzia che tutte le esecuzioni possibili vengano simulate.

Il testing è un sistema operativo che viene eseguito su insiemi selezionati di input e eventi esterni e che viene poi successivamente anche verificato. Per natura, i test possono essere applicati solo dopo che è stata realizzata un'implementazione del sistema.

La verifica formale, al contrario del test, funziona su modelli piuttosto che su implementazioni ed equivale a una prova matematica della correttezza di un sistema. La verifica formale ha lo scopo di fornire la capacità di esprimere specifiche in maniera precisa e di definire in modo chiaro quando un’implementazione soddisfa le specifiche.

Il model checking, invece, è una delle tecniche di maggior successo e popolarità che sono state sviluppate per questo obiettivo. Ha avuto molto successo nella verifica dell'hardware digitale, nella verifica dei protocolli e, più recentemente, nella verifica del software.

Il model checking è un algoritmo di verifica formale introdotto agli inizi degli anni ’80 da Clarke & Emerson (USA) e contemporaneamente da Quielle & Sifakis (Francia). È una tecnica automatica per verificare le proprietà di correttezza dei sistemi reattivi critici per la sicurezza.

Questo metodo è stato applicato con successo per trovare errori sottili in progetti industriali complessi come circuiti sequenziali, protocolli di comunicazione e controllori digitali. Si prevede che, oltre alle classiche misure di garanzia della qualità come l'analisi statica e il collaudo, il model checking diventerà una procedura standard nella progettazione di sistemi reattivi.

Un enorme problema nell’ambito dell’ICT è che la complessità dei sistemi informatici cresce rapidamente e continuamente, e quindi cresce anche la loro vulnerabilità. Il malfunzionamento delle applicazioni, siano esse hardware, software o sistemi di comunicazione, può comportare danni rilevanti di ogni genere anche gravi con notevoli conseguenze finanziarie per chi li produce. Inoltre, se gli errori non vengono rilevati prima dell’impiego del sistema, la volontà di applicare eventuali misure correttive è, se possibile, ben più difficile e costosa.

Ci sono stati moltissimi errori di software e hardware che sono ancora oggi noti esempi drammatici. Possiamo ricordare tra i più importanti: il bug dell'unità di divisione in virgola mobile del Pentium di Intel all'inizio degli anni Novanta, il caso Therac-25, il caso dell'aeroporto di Denver, il caso AT&T e l’Ariane 5.

Il caso Therac-25 (1985-1987)

Il Therac-25 era una macchina per radioterapia prodotta dall’Atomic Energy of Canada Limited (AECL). In poche parole, era uno "zapper del cancro", un acceleratore lineare medico con un essere umano come bersaglio. Utilizzando i raggi X o un raggio di elettroni, le macchine per la radioterapia, in generale, uccidono il tessuto canceroso anche in profondità all'interno del corpo.

Questi dispositivi medici delle dimensioni di una stanza causano quasi sempre alcuni danni collaterali ai tessuti sani intorno ai tumori. Come con la chemioterapia, la speranza è che l'effetto guarisca il paziente più di quanto lo danneggi.

Per sei sfortunati pazienti nel 1985 fino al 1987, il Therac-25 fece l'impensabile: li espose a massicce dosi di radiazioni, uccidendone quattro e lasciandone altri due con ferite permanenti. Per diversi anni, e con il trattamento effettuato su migliaia di pazienti, non ci furono problemi.

Il 3 giugno 1985 una donna era in cura per un cancro al seno. Le erano state prescritte 200 rad- (Radiation Absorbed Dose) sotto forma di un fascio di elettroni da 10 MeV. Il paziente avvertì un calore tremendo quando la macchina si accese. All'epoca non si sapeva, ma era stata bruciata da 20.000 rad. La paziente rimase in vita, ma perse il seno sinistro e l'uso del braccio sinistro a causa delle radiazioni.

Dopo il primo incidente, la risposta dell'AECL fu semplice: "Dopo un'attenta considerazione, siamo del parere che questo danno non possa essere stato causato da un malfunzionamento del Therac-25 o da un errore dell'operatore".

• Il 26 luglio, un secondo paziente venne ustionato presso la Ontario Cancer Foundation di Hamilton, Ontario, Canada. Questo paziente morì nel novembre dello stesso anno. L'autopsia stabilì che la morte era riconducibile a un cancro cervicale particolarmente aggressivo. Tuttavia, se fosse vissuto, avrebbe avuto bisogno di una sostituzione completa dell'anca per rimediare ai danni causati dal Therac-25.
• Nel dicembre del 1985, una terza donna fu bruciata da un Therac-25 installato a Yakima, Washington. Sviluppò una voglia a strisce sul fianco che corrispondeva alle strisce di blocco del raggio sul Therac-25. Questo paziente sopravvisse, ma alla fine dovette ricorrere a innesti cutanei per chiudere le ferite causate dalle ustioni da radiazioni.
• Il 21 marzo 1986, un paziente a Tyler, in Texas, avrebbe dovuto ricevere il suo nono trattamento Therac-25. Gli furono prescritti 180 rad per un piccolo tumore sulla schiena. Quando la macchina si accese, egli sentì calore e dolore, il che era inaspettato poiché la radioterapia è solitamente un processo indolore. Anche lo stesso Therac-25 iniziò a emettere un suono insolito. Il paziente cercò di alzarsi dal lettino quando venne colpito da un secondo fascio di radiazioni fino ad arrivare a bussare alla porta per chiedere aiuto. Fu ricoverato in ospedale per malattia da radiazioni e morì 5 mesi dopo.
• L'11 aprile 1986 si verificò un altro incidente a Tyler, in Texas. Questa volta il paziente era in cura per un cancro della pelle all'orecchio. Lo stesso operatore stava facendo funzionare la macchina come nell'incidente del 21 marzo. Quando iniziò la terapia, il paziente vide una luce intensa e sentì un ronzio fortissimo. Riportò che gli sembrasse che la sua faccia fosse in fiamme. Il paziente morì tre settimane dopo a causa di ustioni da radiazioni sul lobo temporale destro del cervello e sul tronco encefalico.

Solo dopo il quinto incidente l'AECL intraprese un'azione formale. Tuttavia, fu un fisico dell'ospedale in cui si verificarono il quarto e il quinto incidente, Fritz Hager, che riuscì a riprodurre il misterioso "malfunzionamento 54". Alla fine, l'AECL prese provvedimenti e apportò una serie di modifiche al software del sistema di trattamento delle radiazioni Therac-25. La macchina è la stessa che è ancora in uso oggi.

Durante l'indagine, si stabilì che la causa principale del problema fu duplice:

• In primo luogo, il software che controllava la macchina conteneva dei bug che si sono rivelati fatali.
• In secondo luogo, il design della macchina si basava solo sul computer di controllo per motivi di sicurezza. Non c'erano interblocchi hardware o circuiti di supervisione per garantire che i bug del software non potessero causare guasti catastrofici.

Il codice di questo sistema fu programmato da una sola persona, che aveva eseguito in gran parte tutti i test. La macchina fu testata per sole 2700 ore di utilizzo, ma per un codice che controlla una macchina così critica, si sarebbero dovute dedicare molte più ore alla fase di test. Inoltre, il Therac-25 era stato testato come un'intera macchina piuttosto che come moduli separati: testando moduli separati si sarebbero scoperti molti bug. Inoltre, se l'AECL avesse creduto che ci potessero essere problemi con il Therac-25 subito dopo il primo incidente forse, avrebbe potuto evitare che si verificassero gli altri 5 incidenti e forse, anche le 3 vittime.

Il Therac-25 era la terza macchina per radioterapia dell'azienda, preceduta dal Therac-6 e dal Therac-20. Il funzionamento della macchina è spiegato attraverso la seguente immagine:

Si parte dal computer su cui si trova il software che il tecnico deve utilizzare. Questo viene inviato a un altro minicomputer chiamato PDP-11. Infine, la macchina per le radiazioni riceve i comandi e tratta il paziente. La macchina stessa è racchiusa in una sala di radioterapia per evitare l'esposizione dei tecnici che lavorano nelle vicinanze. Il paziente è dotato di apparecchiature audio e visive che consentono di comunicare con i tecnici.

Il PDP-11 del Therac-25 fu programmato completamente in linguaggio assembly. Non solo l'applicazione, ma l'esecutivo sottostante, che ha preso il posto di un sistema operativo. Il computer aveva il compito di gestire il controllo in tempo reale della macchina, sia il suo normale funzionamento che i sistemi di sicurezza. Oggi, questo tipo di lavoro potrebbe essere gestito da un microcontrollore o due, con un PC che esegue un front-end GUI.

Il Therac-25 è stato uno dei più devastanti disastri di ingegneria informatica mai avvenuti. La macchina era stata progettata per aiutare le persone e in gran parte lo ha fatto. Tuttavia, una progettazione approssimativa da parte dell'AECL ha portato alla morte o a gravi lesioni di sei persone.

Il caso dell’aeroporto di Denver (1994)

Quello che doveva essere il più grande sistema di gestione automatizzata dei bagagli aeroportuali al mondo, è diventato un classico della storia di come i progetti tecnologici e innovativi possano andare male.

Di fronte alla necessità di una maggiore capacità aeroportuale, la città di Denver decise di costruire un nuovo aeroporto all'avanguardia che avrebbe consolidato la posizione di Denver come hub del trasporto aereo. Con una superficie di 140 Km², l'aeroporto doveva essere il più grande degli Stati Uniti e doveva gestire più di 50 milioni di passeggeri all'anno.

I piani dell'aeroporto prevedevano un rivoluzionario sistema di trasporto bagagli computerizzato che avrebbe trasportato i bagagli dei passeggeri in carrelli attraverso l'aeroporto tentacolare su 22 miglia di binari tortuosi e nastri trasportatori col minimo intervento umano.

L'obiettivo era quello di ridurre i tempi di attesa degli aerei a solo 30 minuti e aumentare l'efficienza. Fu concepito come un sistema completamente automatizzato e integrato che serviva tutti i corridoi e le compagnie aeree della DIA (Denver International Airport), spostando i bagagli dal check-in all'aereo, da un aereo all'altro e dall'aereo al ritiro bagagli.

Molte persone che lavorarono al progetto capirono che l'estrema complessità del sistema lo rendeva irrealizzabile, ma i piani andarono avanti lo stesso. Una famigerata dimostrazione mediatica del 1994 del sistema mostrò carrelli che si scontravano, bagagli "lanciava, masticava e sputava i bagagli così spesso lanciati o schiacciati e vestiti sparsi. Durante i test, da essere conosciuto come il sistema bagagli infernale" riferì NBC News.

Nonostante le buone intenzioni, il piano si dissolse rapidamente in quanto una sottovalutazione della complessità del progetto portò a problemi e umiliazioni pubbliche per tutti i soggetti coinvolti e l’apertura dell'aeroporto fu ritardata di ben 16 mesi: il sistema che avrebbe dovuto ridurre i ritardi nei voli, i tempi di attesa dei bagagli e i costi di manodopera, si trasformò nella perdita più costosa nella storia della compagnia aerea americana.

Le decisioni iniziali di pianificazione, la decisione di procedere con un unico sistema integrato a livello aeroportuale, i fermi impegni contrattuali in termini di portata, tempistica e budget e le decisioni impossibili prese da persone che non avevano le conoscenze necessarie furono le scintille che hanno innescato l'incendio.

Problemi meccanici e di software, come la caduta dei bagagli dai carrelli, l'errato instradamento dei bagagli e l'inceppamento degli stessi sui nastri trasportatori, dominarono la fase di test. Il sistema, infatti, non superò i test necessari per l'omologazione.

Le spese per il mantenimento dell'aeroporto vuoto e gli interessi sui prestiti per la costruzione costarono alla città di Denver 1,1 milioni di dollari al giorno per tutto il periodo di ritardo.

L'aeroporto venne finalmente aperto nel febbraio 1995, con la maggior parte dei bagagli trasportati con il vecchio metodo del rimorchio e il sistema automatizzato utilizzato in modo limitato. Dopo altri tentativi di far funzionare correttamente l'intero sistema automatizzato e con i costi associati che passarono da meno di 200 milioni di dollari iniziali a circa 600 milioni di dollari, il sistema fu abbandonato nel 2005.

Un articolo del New York Times dell'epoca la definì "la macchina geniale che non riusciva a rigare dritto".

Il Pentium FDIV Bug (1994)

Uno dei migliori esempi delle differenze tra unit testing e system testing può essere illustrato nel contesto del famigerato bug del Pentium FDIV.

Nel 1994 Intel introdusse il suo microprocessore Pentium e qualche mese dopo Thomas R. Nicely, un matematico del Lynchburg College in Virginia, scoprì che il chip forniva risposte errate ad alcuni calcoli di divisione in virgola mobile. Il chip era leggermente impreciso per alcune coppie di numeri.

Intel sostenne (probabilmente a ragione) che solo una divisione su nove miliardi di operazioni avrebbe mostrato una precisione ridotta. Per migliorare la velocità dei calcoli di divisione in virgola mobile sul chip Pentium rispetto al 486DX, Intel scelse di sostituire l'algoritmo di divisione con l'algoritmo di divisione Sweeney, Robertson e Tocher (SRT).

L'algoritmo SRT poteva generare due bit del risultato della divisione per ciclo di clock, mentre l'algoritmo del 486DX ne poteva generare solo uno. Fu implementato utilizzando un array logico programmabile con 2.048 celle, di cui 1.066 avrebbero dovuto essere popolate con uno dei cinque valori seguenti: -2, -1, 0, +1, +2.

Quando fu compilato l'array originale per il Pentium, cinque valori non vennero scaricati correttamente nell'apparecchiatura che incide gli array nei chip - quindi cinque delle celle dell'array contenevano zero mentre avrebbero dovuto contenere +2. L'errore che causò il guasto fu molto difficile da individuare durante i test del sistema e, in effetti, Intel dichiarò di aver eseguito milioni di casi di test utilizzando questa tabella. Ma le voci della tabella rimasero vuote perché una condizione di test...