Trustworthy Deployment of ML-DSA: Secure Implementation supported by Runtime Controller

L’ecosistema digitale moderno è sempre più caratterizzato da un’interconnettività pervasiva e da un panorama delle minacce informatiche in continua evoluzione. In questo contesto, la crittografia è diventata uno dei pilastri fondamentali per la protezione delle comunicazioni digitali, delle informazioni sensibili e delle infrastrutture critiche. Allo stesso tempo, il rapido progresso dell’informatica quantistica pone sfide senza precedenti agli attuali standard crittografici. Il passaggio alla crittografia post-quantistica (PQC) non è più una questione puramente teorica, ma una necessità operativa, poiché si prevede che gli schemi a chiave pubblica ampiamente adottati, quali RSA ed ECC, diventeranno vulnerabili ad attacchi quantistici su larga scala. Tuttavia, la semplice sostituzione degli algoritmi vulnerabili con alternative resistenti ad attacchi quantistici non è sufficiente a garantire la sicurezza dei sistemi. Anche gli schemi crittografici matematicamente validi possono comunque essere compromessi da difetti di implementazione, condizioni di esecuzione impreviste o attacchi tramite canali laterali. Questo problema è particolarmente critico per gli schemi di firma digitale come ML-DSA, in cui esecuzioni anomale o stati malformati potrebbero potenzialmente esporre materiale segreto sensibile. Le tecniche di validazione tradizionali, tra cui i test e l’analisi statica, spesso faticano a rilevare le anomalie dinamiche e dipendenti dal contesto che emergono durante l’effettiva esecuzione dei sistemi implementati. Di conseguenza, vi è una crescente necessità di meccanismi computazionalmente leggeri ma rigorosi, in grado non solo di osservare il comportamento in fase di esecuzione, ma anche di garantire la corretta esecuzione in ambienti critici dal punto di vista della sicurezza. Per affrontare queste sfide, la presente tesi indaga l’applicazione della verifica in fase di esecuzione (Runtime Verification, RV) come meccanismo di controllo attivo del processi nei protocolli crittografici post-quantistici. Nello specifico, il lavoro integra tecniche di monitoraggio in fase di esecuzione nel flusso esecutivo dello schema di firma ML-DSA per rilevare comportamenti non sicuri e rafforzare la sicurezza operativa. Tra i principali contributi figurano la formalizzazione delle proprietà di sicurezza fondamentali per ML-DSA mediante macchine a stati finiti, la progettazione di un’architettura di applicazione in fase di esecuzione ispirata agli ambienti di esecuzione affidabili (TEE) e lo sviluppo di un prototipo di monitor. Infine, viene presentata una valutazione sperimentale esaustiva volta a valutare sia i vantaggi in termini di sicurezza sia il sovraccarico prestazionale, dimostrando la fattibilità pratica di proteggere le implementazioni crittografiche post-quantistiche dai guasti in fase di esecuzione.

The modern digital ecosystem is increasingly characterized by pervasive inter-connectivity and a continuously evolving cyber-threat landscape. In this context, cryptography has become one of the fundamental pillars of protecting digital communications, sensitive information, and critical infrastructures. At the same time, the rapid advancement of quantum computing introduces unprecedented challenges to current cryptographic standards. The transition toward Post-Quantum Cryptography (PQC) is no longer a purely theoretical concern, but an operational necessity, as widely adopted public-key schemes such as RSA and ECC are expected to become vulnerable to large-scale quantum attacks. However, replacing vulnerable algorithms with quantum-resistant alternatives alone is not sufficient to guarantee secure systems. Even mathematically sound cryptographic schemes may still be compromised by implementation flaws, unexpected runtime conditions, or side-channel attacks. This issue is particularly critical for digital signature schemes such as ML-DSA, where anomalous executions or malformed states may potentially expose sensitive secret material. Traditional validation techniques, including testing and static analysis, often struggle to capture the dynamic and context-dependent anomalies that emerge during the actual execution of deployed systems. Consequently, there is a growing need for lightweight yet rigorous mechanisms capable not only of observing runtime behaviour, but also of enforcing correct execution in security-critical environments. To address these challenges, this thesis investigates the application of Runtime Verification (RV) as a mechanism for active process enforcement in Post-Quantum cryptographic protocols. Specifically, the work integrates runtime monitoring techniques into the execution flow of the ML-DSA signature scheme to detect unsafe behaviours and strengthen operational security. The main contributions include the formalization of critical safety properties for ML-DSA using Finite State Machines, the design of a Runtime Enforcement architecture inspired by Trusted Execution Environments (TEE), and the development of a prototype monitor. Finally, an exhaustive experimental evaluation is presented to assess both the security benefits and the performance overhead, demonstrating the practical feasibility of securing post-quantum cryptographic implementations against runtime faults.