Automatizzare la sicurezza: L'approccio CoDefeater

Quando si parla di sistemi critici per la sicurezza, come quelli usati in sanità, trasporti, energia e aviazione, garantire il loro funzionamento sicuro è una questione seria. Questi sistemi possono avere conseguenze gravi in caso di guasto, causando danni a persone, ambiente e beni. Per questo motivo, c'è un forte bisogno di metodi per dimostrare che questi sistemi sono sicuri da usare.

Un modo per farlo è attraverso un processo chiamato casi di assurance. Un caso di assurance espone affermazioni su come funziona un sistema e fornisce argomenti e prove per supportare queste affermazioni. Tuttavia, una delle sfide con i casi di assurance è che a volte possono mancare punti o argomenti importanti che indeboliscono le affermazioni, noti come sconfittori. Questi sconfittori possono essere considerati dubbi o prove che sfidano le affermazioni fatte nei casi di assurance. Identificare e affrontare questi sconfittori è fondamentale per assicurarsi che le affermazioni di sicurezza siano valide e affidabili.

#Cosa sono gli Sconfittori?

Gli sconfittori evidenziano problemi o lacune nelle prove che supportano le affermazioni. Ad esempio, se un'affermazione dice che una batteria ha abbastanza carica, uno sconfittore potrebbe mettere in evidenza un difetto nel sistema di monitoraggio della batteria che potrebbe portare a un'assunzione errata sul suo livello di carica.

In molti casi, trovare questi sconfittori si basa sull'esperienza e sul giudizio degli analisti di sicurezza. Questo rende il processo piuttosto laborioso e dispendioso in termini di tempo. Gli analisti di sicurezza devono spesso pensare in modo creativo riguardo ai possibili punti deboli negli argomenti, il che aggiunge complessità. La natura in evoluzione della tecnologia e delle regolamentazioni complica ulteriormente le cose, rendendo essenziale rivedere e aggiornare continuamente i casi di assurance.

#CoDefeater: Un Approccio Automatizzato

Per aiutare a trovare sconfittori, introduciamo un processo chiamato CoDefeater. Questo metodo utilizza modelli linguistici di grandi dimensioni (LLM) per assistere nell'identificazione e generazione di sconfittori per i casi di assurance. Gli LLM sono modelli informatici che possono capire e generare linguaggio umano, rendendoli strumenti utili per vari compiti nell'ingegneria del software.

L'idea alla base di CoDefeater è che utilizzare LLM potrebbe automatizzare il processo di identificazione degli sconfittori, rendendolo più veloce ed efficiente. I risultati iniziali dei test di CoDefeater su casi di assurance del mondo reale indicano che gli LLM possono identificare efficacemente sia sconfittori noti che sconosciuti. Questo potrebbe aiutare gli analisti di sicurezza a sentirsi più sicuri nei loro casi di assurance, migliorandone la completezza e l'affidabilità.

#Casi di Assurance Spiegati

Un caso di assurance è costruito in modo strutturato. Consiste in affermazioni su come un sistema funzionerà in un ambiente specifico, supportato da argomenti e prove. Esistono diverse notazioni formali per documentare questi casi. Esempi comuni includono la Notazione di Strutturazione degli Obiettivi e le Affermazioni-Argomenti-Prove.

Tuttavia, un problema sorge quando queste notazioni non sono completamente esaustive o possono essere incerte. Questo può portare a una fiducia in affermazioni che potrebbero non reggere a un'analisi approfondita, risultando infine in fallimenti. Un esempio ben noto di ciò è un incidente aereo causato da ragionamento inadeguato nel caso di sicurezza di un sistema.

Per rafforzare i casi di assurance, è essenziale individuare e affrontare gli sconfittori, che espongono lacune nel ragionamento o nelle prove. Identificare gli sconfittori rimane una sfida ed è normalmente un processo manuale. Questo porta a un rischio di pregiudizio, in cui gli analisti umani potrebbero trascurare punti importanti.

#Il Ruolo dei Modelli Linguistici

Recenti progressi hanno dimostrato che gli LLM possono aiutare ad automatizzare vari compiti nell'ingegneria del software, inclusa la generazione di test e la ricerca di difetti nei sistemi. Questi modelli hanno anche mostrato promettenti risultati in compiti che necessitano di una comprensione complessa, come la raccolta di requisiti e la creazione di codice. A causa di queste capacità, abbiamo iniziato a indagare se gli LLM potessero assistere nell'identificazione degli sconfittori all'interno dei casi di assurance.

Nonostante l'interesse crescente nell'utilizzo degli LLM per questo scopo, è mancata una ricerca empirica che esamini la loro efficacia. Pertanto, il nostro obiettivo era valutare il potenziale degli LLM per assistere nell'identificazione degli sconfittori e supportare gli analisti di sicurezza nel processo.

#Domande di Ricerca

Per guidare la nostra indagine, ci siamo concentrati su due domande principali:

1. Quanto sono efficaci gli LLM nell'identificare e analizzare gli sconfittori nei casi di assurance?
2. Possono gli LLM aiutare i professionisti a generare nuovi e utili sconfittori?

#Impostazione dell'Esperimento

Abbiamo condotto esperimenti utilizzando due casi di assurance. Il primo caso proveniva dal Large Hadron Collider, che doveva garantire che il suo sistema di protezione della macchina potesse prevenire danni. Il secondo caso riguardava piccoli sistemi aerei senza pilota (SUAS), affrontando specificamente l'affermazione che la batteria avesse una carica sufficiente per la sua missione.

Per analizzare l'efficacia dell'LLM, abbiamo utilizzato ChatGPT, un modello linguistico ben noto. Gli esperimenti prevedevano di presentare compiti al modello e valutare le sue risposte per accuratezza e rilevanza.

#Criteri di Valutazione

Data la complessità dei compiti, avevamo bisogno di un modo chiaro per valutare le prestazioni del modello. Ci siamo affidati a valutazioni umane per classificare le risposte come corrispondenze complete, corrispondenze parziali o nessuna corrispondenza rispetto ai sconfittori di verità stabilita.

Per la valutazione dei nuovi sconfittori, abbiamo controllato se i sconfittori generati dall'LLM fossero ragionevoli e potessero potenzialmente rientrare nella verità stabilita. Questo approccio mirava a valutare la creatività e l'efficacia del modello nella generazione di nuove idee.

#Risultati

#Efficacia nell'Identificare Sconfittori

I risultati hanno mostrato che l'LLM era efficace nell'identificare sconfittori. In un contesto zero-shot, in cui il modello non aveva esempi precedenti, è riuscito a identificare completamente un numero significativo di sconfittori e a identificarne parzialmente altri. Anche nei casi complessi, le prestazioni del modello sono state notevolmente buone.

Tuttavia, alcuni sconfittori sono rimasti non identificati, spesso quelli che richiedevano conoscenze specifiche del dominio o che mettevano in discussione assunzioni implicite. Ad esempio, quando si analizzava un'affermazione relativa al monitoraggio dei segnali, l'LLM potrebbe non notare uno sconfittore che metteva in dubbio la validità del segnale monitorato.

#Utilità nella Generazione di Nuovi Sconfittori

Quando abbiamo chiesto all'LLM di fornire ulteriori sconfittori per il caso degli sUAS, ha generato con successo cinque nuovi sconfittori. Questi sono stati considerati ragionevoli dopo ulteriori indagini e hanno evidenziato potenziali problemi legati a scariche di energia inaspettate o interferenze esterne.

Una proposta interessante è stata che gli uccelli potrebbero attaccare gli sUAS, un esempio di come gli LLM possano aiutare a identificare rischi che potrebbero non venire in mente inizialmente.

#Sfide e Opportunità

Sebbene i risultati siano stati promettenti, sono emerse diverse sfide. Progettare prompt efficaci per l'LLM si è rivelato cruciale poiché influenzavano notevolmente la qualità delle risposte. Trovare il giusto equilibrio tra la generazione di idee creative e il rimanere rilevanti per il compito da svolgere è stata una preoccupazione costante.

Inoltre, l'LLM forniva non solo sconfittori ma anche motivazioni per le sue proposte. Questo potrebbe assistere gli analisti nella comprensione della fattibilità di uno sconfittore e delle potenziali modalità per affrontarlo. La ricerca futura può esplorare tecniche migliori per stimolare l'LLM per migliorare le sue capacità.

#Conclusione e Lavoro Futuro

Il processo CoDefeater offre un approccio innovativo per scoprire sconfittori nei casi di assurance utilizzando LLM. I nostri esperimenti hanno mostrato le capacità zero-shot del modello nell'identificare sconfittori noti e il suo potenziale per assistere gli analisti nella generazione di nuovi.

Man mano che andiamo avanti, sono necessari studi più ampi per validare questi risultati ed esplorare diversi modelli e tecniche. Con il tempo, i miglioramenti negli LLM e nel loro addestramento potrebbero portare a prestazioni ancora migliori nell'assistere gli analisti di sicurezza nei casi di assurance, contribuendo infine a sistemi più sicuri e affidabili.