An Approach for Safe and Secure Software Protection Supported by Symbolic Execution

Il paper presenta un nuovo metodo di protezione del software per il controllo industriale che lega il programma all'hardware tramite Funzioni Fisicamente Inimitabili (PUF) e utilizza l'esecuzione simbolica per garantire la sicurezza e la preservazione delle proprietà di sicurezza in caso di esecuzione su macchine non autorizzate o di malfunzionamenti.

L'essenziale

Ecco una spiegazione semplice e creativa del paper, pensata per chiunque, anche senza conoscenze tecniche di informatica.

🛡️ Il "Serratura Magica" per i Software Industriali

Immagina di avere un ricetta segreta per fare il miglior pane del mondo (questo è il tuo software industriale). Il problema è che chiunque può fotocopiarla e portarla a casa sua per provare a cuocere il pane. Se la ricetta è copiata alla lettera, il pane verrà uguale, e il tuo segreto sarà rubato.

Gli autori di questo articolo hanno inventato un modo per rendere la ricetta inutile se non la usi nella tua cucina specifica.

1. Il Problema: La Fotocopia Perfetta

Nell'industria, rubare il "cervello" delle macchine (il software) è un problema enorme. Spesso, i ladri non hanno bisogno di essere geni della matematica: basta che copino il codice esatto e lo installino su un'altra macchina identica. Il software gira, la macchina funziona e il ladro ha rubato il tuo lavoro senza sforzo.

2. La Soluzione: La "Carta d'Identità" della Macchina (PUF)

Per risolvere questo, gli autori usano una cosa chiamata PUF (Funzione Fisica Non Clonabile).
Immagina che ogni chip di computer, anche se prodotto dalla stessa fabbrica, abbia delle micro-screpolature invisibili o delle imperfezioni uniche, proprio come le impronte digitali umane o le venature di un albero.

• Come funziona: Quando il software chiede al chip "Chi sei?", il chip risponde con una sequenza di numeri basata su queste imperfezioni uniche.
• Il trucco: Se copi il software su un'altra macchina, quella macchina avrà un'impronta digitale diversa. La risposta sarà sbagliata.

3. Il Magico "Guardiano" (Esecuzione Simbolica)

Qui arriva la parte geniale. Di solito, se un software riceve una risposta sbagliata dalla serratura, va in tilt, si blocca o fa cose pericolose (come far esplodere una caldaia industriale).

Gli autori hanno usato una tecnica chiamata Esecuzione Simbolica.
Immagina di avere un super-cuoco virtuale che prova a cucinare la ricetta prima che tu la esegua davvero. Questo cuoco virtuale prova tutte le possibilità:

• "Se la serratura dice 'A', cosa succede?"
• "Se dice 'B', cosa succede?"

Il suo compito è trovare un modo per dire: "Ok, se la serratura è sbagliata, invece di far esplodere la cucina, cambiamo il modo di impastare in modo che il pane venga comunque sicuro (anche se non perfetto), ma mai pericoloso."

4. Cosa succede in pratica?

Ecco la scena del crimine (o meglio, del tentativo di furto):

• Scenario A (La Macchina Giusta): Il software chiede la "carta d'identità" alla macchina. La macchina risponde correttamente. Il software dice: "Ok, tutto a posto, ora faccio il pane perfetto!" 🍞✨
• Scenario B (La Macchina Rubata): Il ladro copia il software su un'altra macchina. La macchina risponde con un'impronta diversa. Il software, invece di bloccarsi o esplodere, dice: "Ehi, la serratura non è quella giusta. Non posso fare il pane perfetto, ma per sicurezza farò un pane che non brucia mai, anche se sarà un po' strano e casuale." 🍞❓

Il risultato per il ladro:
Il software gira, ma si comporta in modo imprevedibile e diverso ogni volta. Il ladro non può capire come funziona il sistema originale perché il comportamento cambia continuamente. Per decifrare la logica, dovrebbe passare anni a studiare il codice, rendendo il furto troppo costoso e inutile.

5. Perché è sicuro?

L'articolo dice che questo metodo è sicuro per due motivi:

1. Sicurezza Fisica: Non puoi clonare l'impronta digitale del chip (la PUF).
2. Sicurezza Logica: Anche se il ladro prova a ingannare il sistema, il software è programmato per non fare mai danni. È come se avessi un'auto che, se provi a rubarla, non scappa via, ma si trasforma in un giocattolo lento e sicuro che non può fare male a nessuno, rendendo inutile il tentativo di furto.

In Sintesi

Hanno creato un software che ha una serratura magica legata all'hardware unico della macchina. Se provi a portarlo altrove, non si blocca (per sicurezza), ma inizia a comportarsi in modo strano e casuale, rendendo impossibile per un ladro capire come funziona davvero o replicarlo. È come avere una ricetta che cambia ingredienti ogni volta che la provi in una cucina diversa, ma che garantisce che il cibo non ti faccia mai male.

Sommario tecnico

Ecco un riassunto tecnico dettagliato del paper "An Approach for Safe and Secure Software Protection Supported by Symbolic Execution", presentato in italiano.

1. Il Problema

Il furto di proprietà intellettuale (IP) nell'industria, in particolare attraverso il reverse engineering di software per il controllo industriale, rappresenta una minaccia significativa con perdite economiche stimate in miliardi di euro.

• Vulnerabilità attuale: Il software può spesso essere copiato integralmente senza bisogno di reverse engineering, a differenza dell'hardware che richiede uno sforzo maggiore per essere replicato.
• Limiti delle soluzioni esistenti: I metodi precedenti di protezione basati su PUF (Physically Unclonable Functions), come quelli che utilizzano checksum dinamici, possono portare a comportamenti non sicuri o crash se la risposta del PUF non è quella attesa (es. a causa di errori o tentativi di manipolazione).
• Obiettivo: Creare un metodo di protezione che leghi il software a un hardware specifico in modo che, se eseguito su una macchina diversa (o clonata), il programma non solo si comporti in modo errato (rendendo difficile il reverse engineering), ma garantisca assolutamente il rispetto dei vincoli di sicurezza (safe-by-design), evitando danni fisici o crash.

2. Metodologia

L'approccio proposto combina tre elementi fondamentali:

1. Binding Hardware-Software tramite PUF: Utilizzo di Funzioni Fisiche Non Clonabili (PUF), che sfruttano le variazioni fisiche uniche dei componenti hardware (es. DRAM) per generare risposte uniche a sfide (challenge) specifiche. Il software è vincolato all'hardware target tramite queste risposte.
2. Modellazione tramite ASM (Abstract State Machines): Il software di controllo industriale è modellato come una macchina a stati finiti (Control State ASM). Questo formalismo permette di descrivere algoritmi di controllo come programmi astratti eseguibili.
3. Esecuzione Simbolica per Garanzia di Sicurezza: L'innovazione principale risiede nell'uso dell'esecuzione simbolica per determinare, a priori, quali transizioni di stato sono "sicure".

Il meccanismo di protezione:

• Invece di far saltare il programma a un indirizzo casuale se il PUF fallisce (rischio di crash), il sistema sostituisce le transizioni di stato originali con una procedura (ChoosePhase o ChooseCtlState).
• Questa procedura interroga il PUF per ottenere il prossimo stato previsto.
• Se la risposta del PUF corrisponde allo stato corretto (hardware originale), il programma procede normalmente.
• Se la risposta è diversa (hardware non originale o errore), il sistema seleziona non-deterministicamente un nuovo stato tra un insieme pre-calcolato di "stati sicuri" (safePhases).
• Gli "stati sicuri" sono definiti come quegli stati che non violano i vincoli di sicurezza critici (es. evitare che due luci del traffico siano verdi contemporaneamente).

Fasi dell'algoritmo di protezione:

1. Mappatura delle transizioni di stato del programma originale alle coppie sfida-risposta del PUF.
2. Sostituzione delle regole di aggiornamento dello stato di controllo con una logica che interroga il PUF.
3. Utilizzo dell'esecuzione simbolica sul modello ASM originale per analizzare tutti i percorsi possibili.
4. Identificazione formale dell'insieme di stati che, se raggiunti, non violano i vincoli di sicurezza ($\Psi$).
5. Generazione automatica di una specifica protetta che, in caso di risposta PUF errata, forza il sistema in uno di questi stati sicuri.

3. Contributi Chiave

• Protezione "Safe-by-Design": A differenza di approcci precedenti che rischiano di causare malfunzionamenti critici in caso di fallimento della verifica, questo metodo garantisce che il software, anche se eseguito su hardware non autorizzato, rimanga in uno stato sicuro.
• Generalizzazione per ASM: Il metodo è formalizzato per una vasta classe di algoritmi di controllo industriale rappresentabili come Control State ASM.
• Resistenza al Reverse Engineering: Se un attaccante copia il software su un hardware diverso, il programma esegue un flusso non deterministico e "sbagliato" (ma sicuro). Questo rende estremamente difficile e costoso per un attaccante ricostruire la logica corretta del flusso di controllo, poiché non può dedurre facilmente le risposte corrette del PUF né il flusso logico originale senza un'analisi complessa.
• Formalizzazione Matematica: Il paper fornisce una definizione rigorosa dei passaggi meccanici per trasformare una specifica ASM non protetta in una specifica protetta e sicura.

4. Risultati ed Valutazione

• Sicurezza: L'analisi della minaccia (modello white-box) indica che l'attacco statico (decompilazione) è inefficace perché non rivela i valori del PUF. L'attacco dinamico (esecuzione su hardware clonato) fallisce perché il PUF non è clonabile e il comportamento diventa non deterministico. L'attacco su hardware originale richiede un tracciamento dinamico complesso e costoso, ulteriormente ostacolato da possibili interferenze temporali (es. nei PUF basati su DRAM).
• Sicurezza Funzionale: L'uso dell'esecuzione simbolica garantisce matematicamente che nessun percorso di esecuzione, nemmeno quello attivato da una risposta PUF errata, porti a una violazione dei vincoli di sicurezza.
• Esempio Pratico: Il metodo è stato dimostrato su un algoritmo di controllo per un semaforo a senso unico. È stato mostrato come lo stato "Go1Go2" (entrambi i semafori verdi, stato pericoloso) venga escluso dall'insieme degli stati sicuri, garantendo che il sistema non possa mai raggiungerlo, indipendentemente dall'hardware su cui gira.

5. Significato e Impatto

Questo lavoro rappresenta un passo avanti significativo nella sicurezza del software industriale:

• Affidabilità: Risolve il dilemma tra protezione IP e sicurezza operativa. Spesso, i meccanismi di protezione che falliscono causano danni; questo approccio elimina tale rischio.
• Scalabilità Industriale: Essendo basato su ASM, è applicabile a una vasta gamma di sistemi di controllo industriale (PLC, automazione).
• Futuro: I ricercatori intendono automatizzare l'identificazione degli stati di controllo e l'applicazione del metodo su casi studio industriali reali. Si prevede anche l'uso di solutori SMT (Satisfiability Modulo Theories) per gestire la complessità delle formule logiche generate dall'esecuzione simbolica su sistemi grandi, per evitare impatti sulle prestazioni di tempo reale.

In sintesi, il paper propone un framework teorico e pratico per rendere il software "inutile" se copiato su hardware non autorizzato, senza però mai compromettere la sicurezza fisica dell'impianto industriale.