A platform-evidence mapping for DAL-B certification planning on an AMD64 multi-core processor with Xen temporal isolation

Gli aeromobili moderni stanno diventando sempre più complessi, affidandosi a potenti computer per gestire tutto, dai controlli di volo alla navigazione e alla pianificazione della missione. Per garantire la sicurezza, l'industria dell'aviazione utilizza regole rigorose che richiedono che ogni software sia testato e verificato secondo un determinato livello di fiducia. Per i sistemi più critici, come quelli che mantengono un aereo in volo, questo livello di fiducia è il più alto possibile. Tuttavia, è emersa una nuova sfida poiché questi computer si sono evoluti da singoli processori a chip multi-core, simili ai potenti processori che si trovano nei moderni laptop e server. Quando più programmi vengono eseguiti contemporaneamente su core diversi dello stesso chip, spesso competono per l'accesso alle risorse condivise, nello specifico un'area di memoria ad alta velocità chiamata cache di ultimo livello (last-level cache). Questa competizione può rallentare un programma rispetto a un altro in modo imprevedibile, creando un'incertezza temporale che è pericolosa per il software critico per la sicurezza dell'aviazione.

Per risolvere questo problema, i ricercatori stanno sviluppando modi per isolare questi programmi in modo che non interferiscano tra loro. Un approccio promettente coinvolge un tipo di gestore software, noto come hypervisor, che si posiziona tra l'hardware e le applicazioni, dividendo le risorse del computer in compartimenti separati e sicuri. La domanda rimane, tuttavia, se questo isolamento sia abbastanza forte da soddisfare gli standard rigorosi richiesti dall'aviazione commerciale. Un team di ricercatori di Advanced Micro Devices e della Technical University of Munich ha esplorato questa questione creando un piano dettagliato su come certificare un tipo specifico di computer multi-core per l'uso in aeronautica. Il loro lavoro si concentra su una configurazione che utilizza un hypervisor chiamato Xen su processori AMD, combinato con una tecnica chiamata cache coloring, per garantire che le diverse partizioni software non possano accidentalmente calpestarsi i piedi a vicenda.

I ricercatori hanno iniziato identificando il problema specifico: su un processore multi-core, la cache di memoria condivisa è il luogo principale in cui avviene l'interferenza. Se un programma riempie la cache, può costringere un altro programma ad attendere, causando ritardi che potrebbero far mancare una scadenza critica. Per prevenire ciò, il team ha proposto un metodo in cui la memoria del computer viene divisa in gruppi distinti, o "colori", in base a dove risiede il dato. A ogni programma software viene assegnato il proprio set unico di colori, e il sistema è configurato in modo che i dati di un programma non possano mai sostituire i dati di un altro nella cache. Fondamentalmente, questa regola si applica anche all'hypervisor stesso. I ricercatori si sono assicurati che anche i dati del gestore software siano bloccati nel proprio set di colori esclusivo, impedendo che esso possa accidentalmente espungere i dati dei programmi critici per la sicurezza che sta gestendo. Questo crea una garanzia costruttiva che l'interferenza sia limitata (bounded), ovvero che sia matematicamente limitata e prevedibile, piuttosto che sperare semplicemente che non accada.

Il documento presenta una mappatura di questa configurazione tecnica rispetto alle ufficiali regole di certificazione utilizzate dalle autorità aeronautiche negli Stati Uniti e in Europa. Queste regole, note come DO-178C e AC 20-193, richiedono agli richiedenti di dimostrare che le risorse condivise siano gestite in modo sicuro. Gli autori dimostrano come la loro specifica configurazione soddisfi tali requisiti, mostrando che il meccanismo di cache coloring isola efficacementamente la cache di ultimo livello. Mostrano inoltre come il caso di sicurezza (safety case) dell'hypervisor, che è documentato separatamente dalla comunità open-source, possa essere riutilizzato come prova per il produttore dell'aeromobile. Ciò consente al produttore di concentrarsi sulla dimostrazione che le proprie applicazioni specifiche funzionino correttamente all'interno di questo ambiente isolato, invece di dover dimostrare da zero la sicurezza dell'hardware informatico sottostante. I ricercatori delineano un percorso chiaro su come un produttore di aeromobili potrebbe utilizzare questa configurazione per ottenere una certificazione di sicurezza di livello intermedio, nota come DAL-B, che è adatta per molte funzioni importanti ma non vitali.

Tuttavia, gli autori sono cauti nel definire i limiti del loro lavoro. Essi dichiarano esplicitamente che questo piano non dimostra ancora che il sistema sia abbastanza sicuro per il livello più alto di certificazione, noto come DAL-A, che è richiesto per i controlli di volo più critici. Per raggiungere quel livello superiore, sarebbero necessari passaggi aggiuntivi, come la prova formale matematica che lo strumento di allocazione della memoria non commetta mai errori e la raccolta di un'esperienza più estesa nel mondo reale con il processore specifico. Il documento chiarisce anche che non copre i carichi di lavoro dell'intelligenza artificiale o dell'elaborazione grafica, che sono aree emergenti che richiederebbero soluzioni diverse. Inoltre, gli autori sottolineano che si tratta di un articolo metodologico, non di una certificazione finale; fornisce un argomento strutturato e un insieme di strumenti, ma l'approvazione effettiva deve comunque arrivare dai regolatori dell'aviazione, che esamineranno i dettagli specifici di ogni programma aeronautico.

Il nucleo della ricerca è una dimostrazione pratica di come queste astratte regole di sicurezza possano essere applicate a una piattaforma informatica reale. Il team ha descritto una configurazione specifica in cui un computer a quattro core è diviso in partizioni separate per diverse attività, come il controllo del volo, la percezione e la gestione della missione. Hanno mostrato come assegnare a ciascuna partizione un core dedicato e una porzione specifica della cache di memoria, garantendo che il software di controllo del volo abbia sempre le risorse necessarie senza essere rallentato dalle altre attività. Hanno inoltre dettagliato come il sistema controlli gli errori all'avvio per garantire che l'isolamento della memoria stia funzionando correttamente prima che l'aeromobile decolli mai. Questo approccio offre un modo per utilizzare potenti chip informatici disponibili commercialmente nell'aviazione senza sacrificare la prevedibilità e la sicurezza che il settore richiede.

In conclusione, il documento offre un ponte tra l'evoluzione rapida dell'hardware informatico commerciale e il ritmo lento e deliberato della certificazione di sicurezza aeronautica. Dimostra che, con la giusta configurazione, specificamente utilizzando il cache coloring e un hypervisor a partizione statica, è possibile creare un ambiente informatico in cui l'interferenza è controllata e prevedibile. Sebbene il percorso verso i livelli più alti di certificazione richieda ancora ulteriore lavoro, questa ricerca fornisce una solida base affinché i produttori possano iniziare a integrare questi processori avanzati nei loro aeromobili. Il lavoro funge da modello, dimostrando che i meccanismi tecnici esistono per supportare l'integrazione sicura dei sistemi multi-core, a condizione che le regole specifiche e le prove richieste dai regolatori siano attentamente seguite e verificate.