Per anni abbiamo raccontato la sicurezza come un problema di codice, configurazioni e patch. Oggi non basta più. Le moderne microarchitetture, spinte da speculazione, parallelismo, eterogeneità e ottimizzazioni dipendenti dai dati, possono compromettere la riservatezza anche quando il software è corretto.
Il dibattito è stato rinfocolato dalle ricerche di Caroline Trippel, Assistant Professor a Stanford e guida dell’High Assurance Computer Architectures Lab, che nel suo nuovo paper “Specification and Formal Verification of Hardware–Software Contracts for High-Assurance Computer Architectures” (IEEE ComputingEdge, marzo 2026) propone di trattare i contratti hardware-software come il nuovo perimetro della fiducia digitale: non più una promessa vaga tra ISA (Instruction Set Architectures) e implementazione, ma una specifica formale di ciò che l’hardware può fare, di ciò che può far trapelare e di come verificarlo davvero.
Più che un contributo accademico, il suo framework è già leggibile come una roadmap strategica per l’industria del silicio.
Indice degli argomenti
Il chip non è più innocente con l’attenuarsi della Legge di Moore
Il prossimo incidente grave di sicurezza hardware non nascerà necessariamente da una backdoor hollywoodiana o da un bug spettacolare.
Più probabilmente nascerà da qualcosa di molto più banale e molto più pericoloso: unafiducia eccessiva in un processore che fa “la cosa giusta” dal punto di vista funzionale, ma agendo nel modo sbagliato dal punto di vista della riservatezza.
È qui che si colloca il vero salto di maturità del dibattito: capire che un microprocessore può eseguire correttamente un programma e, nello stesso tempo, tradirlo lateralmente.
È il punto su cui insiste l’articolo di Trippel, là dove osserva che la crescente complessità dei design hardware e dei deployment moderni sta esponendo i limiti delle specifiche e dei flussi di verifica attuali.
La tesi è scomoda, ma difficilmente contestabile.
Con l’attenuarsi dei benefici lineari della Legge di Moore, l’industria ha cercato performance attraverso parallelismo, specializzazione hardware, eterogeneità hardware-software e ottimizzazioni data-dependent.
Nel frattempo, gli scenari d’uso sono diventati più critici: multitenancy, hyperscale, automotive, sanità, infrastrutture, servizi di sicurezza.
Trippel, nel suo lavoro, colloca il tema dentro un quadro di assurance requirements stringenti, cioè correttezza, sicurezza e affidabilità insieme. Non è solo una questione di ingegneria elegante: è una ridefinizione del concetto stesso di piattaforma affidabile.
La fiducia malriposta nell’hardware
Per un CISO di un produttore hardware, o per chi ha in carico la product security di piattaforme avanzate, questa erosione della fiducia nel silicio ha ricadute molto concrete.
Significa costi di remediation più tardivi e più costosi, firmware update che inseguono leak emersi tardi, frizioni con i team crypto, maggiore complessità nelle assurance review dei clienti enterprise, esposizione reputazionale nei mercati regolati, e un tema sempre più sensibile nelle catene di fornitura: saper spiegare non solo che cosa fa il chip, ma anche che cosa non farà ai dati sensibili.
In questo senso, la fiducia malriposta nell’hardware diventa un rischio economico prima ancora che tecnico. L’inferenza regolatoria è chiara: in un contesto come quello del Cyber Resilience Act (CRA), che impone requisiti di cyber security lungo il ciclo di vita di prodotti hardware e software, la capacità di dimostrare scelte progettuali robuste e verificabili si avvicina sempre di più a una forma di due diligence tecnica.
Le ISA tradizionali falliscono: correttezza non è più sinonimo di riservatezza
Per decenni, l’Instruction Set Architecture è stata il contratto implicito che ha tenuto insieme l’ecosistema: il software definiva il “cosa”, l’hardware si prendeva in carico il “come”.
È stato un patto industrialmente vincente. Oggi, però, quel patto mostra le crepe.
Trippel lo formula in modo netto: il primo problema è lo specification challenge, cioè il fatto che le ISA tradizionali non siano abbastanza ricche da catturare tutti i modi in cui una microarchitettura può compromettere l’assurance del software.
In altre parole, il software continua a ragionare con astrazioni ordinate; il silicio decide in tempo reale, specula, riordina, condivide risorse, ottimizza e lascia tracce. L’esempio più chiaro viene dai Memory Consistency Models (MCM).
La storia dell’architettura insegna che, quando la complessità cresce, il contratto hardware-software va esplicitato, non lasciato nel sottinteso.
A partire dagli anni Ottanta e poi con l’era multicore, le ISA sono state estese con modelli di consistenza per permettere un ragionamento formale sui programmi concorrenti.
La zona grigia diventa disciplina rigorosa
Litmus test, formalizzazioni e strumenti automatici hanno trasformato quella che era una zona grigia in una disciplina rigorosa.
Oggi, però, la sfida si amplia ancora: nei sistemi eterogenei, i mismatch tra modelli di memoria tra cluster differenti rendono difficile persino definire quale debba essere il comportamento complessivo del sistema, e il paper richiama sia i compound consistency models sia l’approccio modulare di MemGlue come esempi di questa evoluzione.
Ma la vera frattura è emersa con Spectre e con l’intera famiglia degli attacchi da transient execution.
Qui il problema non è che il processore sbagli il risultato finale; il problema è che, durante un percorso speculativo poi annullato, può avere già toccato cache, predictor, porte di memoria o altre risorse in modo osservabile.
Il risultato architetturale resta corretto; la riservatezza, no. È per questo che la frase “l’esecuzione è corretta” non basta più a descrivere la sicurezza di una piattaforma.
In altri termini: il software guarda ancora il risultato; l’attaccante osserva il tragitto.
Il fallimento delle ISA in una riga
Una CPU può restituire il risultato giusto e avere comunque già perso il segreto lungo il percorso.
È qui che la correttezza cessa di coincidere con la sicurezza.
Dai modelli di memoria ai modelli di leakage: dove nasce il nuovo contratto
Il passaggio più importante del lavoro di Trippel è forse questo: trattare la sicurezza side-channel come un problema di specifica formale, non come una collezione di contromisure scollegate.
Se i Memory Consistency Models (MCM) hanno definito i contratti della concorrenza, i nuovi Leakage Containment Models (LCM) fanno lo stesso per la perdita di informazione.
L’idea è potente perché sposta il dibattito dal “come tamponare” al “come specificare ciò che l’hardware è autorizzato a esporre”.
Nel suo articolo, Trippel descrive gli LCM come contratti assiomatici costruiti estendendo direttamente i modelli assiomatici di memoria. È una scelta elegante sul piano teorico e molto pragmatica su quello industriale: si riusa un vocabolario già noto per entrare nel territorio del leakage.
Una tassonomia di base chiara
Un attacco side-channel coinvolge un transmitter, cioè un’operazione che modula una risorsa hardware in modo dipendente dagli operandi; un channel, cioè la risorsa stessa; e un receiver, che osserva indirettamente la modulazione, per esempio attraverso tempo di esecuzione o contesa.
Cache, branch predictor, functional units e memory ports sono tutti candidati naturali.
La forza del framework di Trippel è che non si limita a descrivere il fenomeno: lo porta dentro una forma che il software può usare e che il silicio può, almeno in linea di principio, promettere.
Il contratto oggi più adottato è quello constant-time.
Il paper lo definisce, in sostanza, come il contratto di leakage più diffuso: un modo per enumerare i transmitter di una microarchitettura e i loro operandi insicuri, così che i segreti non li raggiungano durante l’esecuzione.
È qui che la ricerca di Trippel usa una formulazione che merita di essere riportata, perché sintetizza bene l’ordine delle priorità: il constant-time è il “gold standard” software per proteggere il codice crittografico dagli attacchi side-channel hardware.
E non è più soltanto una disciplina di nicchia: il paper ricorda che questi contratti CT sono stati adottati molto recentemente da ISA maggiori, inclusi Arm, Intel e RISC-V.
Una convergenza non solo teorica
Arm documenta esplicitamente la modalità Data Independent Timing (DIT), come meccanismo architetturale per sequenze a tempo indipendente dai dati. Intel pubblica una guidance ufficiale sul Data Operand Independent Timing, precisando che questa proprietà è utile soprattutto per codice scritto in constant time, come quello crittografico.
E la specifica ufficiale delle estensioni crittografiche scalar di RISC-V include un meccanismo che consente agli implementatori di fornire garanzie di Constant Time Execution.
Il dato interessante, per il mercato, è che il lessico della side-channel resilience sta già entrando nelle ISA. Non è più ricerca che osserva l’industria da fuori, bensì ricerca che ne riscrive il vocabolario.
Oltre il constant-time: i contratti di nuova generazione contro Spectre
Il punto, però, è che il constant-time da solo non basta più.
Lo stesso articolo insiste sul fatto che i contratti di prossima generazione devono essere più fini, perché gli attacchi speculative e transient execution dipendono da condizioni di scheduling microarchitetturale che una semplice lista di operandi “leaky” non riesce a descrivere.
Trippel porta un esempio molto efficace: una store può perdere il proprio indirizzo quando coesegue con una load, poiché la load può rallentare o accelerare a seconda che ci sia un match o un mismatch di indirizzo.
Il leakage, dunque, non è sempre un attributo statico dell’istruzione: può essere unaproprietà relazionale, contestuale, emergente.
È qui che compaiono gli execution contracts, cioè contratti che caratterizzano il control-flow e il data-flow speculativi che un programma può manifestare su una specifica implementazione hardware.
Un notevole salto culturale
Significa dire che la sicurezza non riguarda più solo la correttezza dell’architettural state finale, ma anche i comportamenti intermedi, speculative, transienti, bound-to-squash.
In termini industriali, vuol dire che la superficie di sicurezza di una piattaforma non si misura più soltanto in istruzioni supportate, ma nella qualità del patto che offre al software su ciò che accade nel sottobosco microarchitetturale.
Il messaggio dalla ricerca può arrivare a noi in un modo che è più semplice, ossia: chi costruisce il prossimo processore general purpose, il prossimo acceleratore crittografico, il prossimo SoC edge o il prossimo core per ambienti regolati non potrà limitarsi a dire “supportiamo il software X”.
Dovrà iniziare a dire “offriamo il contratto di leakage Y, con la verifica Z”. In altri termini, la sicurezza del silicio sta entrando nell’era delle promesse verificabili.
La verifica è il vero collo di bottiglia: perché il top-down non basta più
Una specifica migliore non ha alcun valore se non si riesce a dimostrare che il design la rispetta. Ed è qui che il paper diventa particolarmente duro con lo stato dell’arte.
Trippel richiama uno studio 2024 di Siemens EDA e Wilson Research Group secondo cui, nonostante l’enorme quantità di tempo spesa in verification, bug critici arrivano ancora fino al silicio nell’87% dei progetti FPGA e nell’86% dei progetti IC/ASIC.
È una fotografia che dovrebbe inquietare non solo gli ingegneri di verifica, ma anche board, CISO e product leader: il settore continua a spendere moltissimo per dimostrare la qualità del chip, ma lascia ancora passare troppi difetti in produzione.
Il paradigma top-down sulla graticola
Il bersaglio principale della critica è il paradigma top-down.
Nel modello industriale classico, il verification engineer prende requisiti astratti, li traduce a mano in proprietà formali sui segnali del design e poi usa model checker o strumenti analoghi per verificare il tutto.
Funziona, ma scala male.
Soprattutto, quando si entra nel dominio dei side-channel e della two-trace noninterference, il problema esplode: bisogna confrontare due esecuzioni che differiscono solo per i segreti e dimostrare che non emergano differenze osservabili.
Il paper spiega bene il limite dei metodi diretti: analizzare due copie del design insieme, in un product circuit, porta a un’esplosione dello spazio degli stati e costringe spesso a lavorare da stati iniziali simbolici non sempre realistici, con forte intervento manuale per distinguere controesempi veri e falsi.
La proposta: la svolta bottom-up
Non si parte più soltanto dalla specifica per verificare il design; si parte anche dal design per sintetizzare una specifica formalmente verificata che rifletta ciò che l’hardware fa davvero.
Qui si descrive questo approccio come una generazione automatica di molte proprietà semplici, derivate da template e analisi statica del netlist, che consentono di ricostruire un modello verificato del comportamento microarchitetturale.
Qui entrano in scena i grafi di microarchitectural happens-before (μhb), i modelli μspec e, soprattutto, i μpath, cioè i percorsi di esecuzione microarchitetturale ciclo per ciclo.
È un cambio di prospettiva enorme: la verifica non è più solo un controllo di conformità, ma anche un processo di reverse engineering formale della realtà del design.
rtl2mμpath, SynthLC, CloU, Serberus: quando la teoria cambia il prodotto
Il lavoro di Trippel smette qui di sembrare “solo accademico” e comincia a parlare direttamente ai team di product security.
L’articolo ripercorre infatti una traiettoria precisa.
Prima rtl2μspec, capace di sintetizzare modelli μspec verificati da design semplici.
Poi rtl2mμpath, nato per superare il limite della singola execution path e produrre un insieme completo di percorsi microarchitetturali cycle-accurate per ogni istruzione.
Ed è proprio nella costruzione di rtl2mμpath che emerge l’intuizione decisiva: quando un’istruzione ammette più di un μpath, quella variabilità è spesso il segnale di un side-channel.
SynthLC
Da qui nasce SynthLC, che estende rtl2mμpath con symbolic information flow tracking per sintetizzare un insieme completo di leakage signatures formalmente verificate da un design SystemVerilog, assumendo un attaccante che osserva tempo di esecuzione o contesa delle risorse.
Il paper è molto chiaro nel descriverne il valore: queste firme di leakage catturano i dettagli microarchitetturali necessari a implementare dieci difese side-channel di stato dell’arte e rendono SynthLC la prima metodologia automatizzata per verificare l’implementazione corretta di tali difese nel codice RTL.
Per un team di validazione, questo significa passare dalla speranza che il design “non perda troppo” alla capacità di estrarre un inventario verificato di dove, come e in quali condizioni il design perde informazione.
Il caso CVA6: una questione concreta
Sul core RISC-V CVA6, SynthLC ha fatto emergere 94 leakage signatures uniche, 72 transponders e 26 transmitters, trovando anche un nuovo canale che perde gli operandi di indirizzo di load e store e apre a una nuova classe di speculative interference attacks.
Lo stesso approccio è stato poi applicato alla cache dati L1 e al relativo controller, diventando – sempre secondo Trippel – la prima analisi formale side-channel di una cache realistica.
La notizia nuova e rilevante, per chi fa business sull’hardware, è lampante: la verifica formale non sta solo dimostrando proprietà note, sta scoprendo vulnerabilità che i flussi tradizionali tendono a lasciarsi sfuggire.
Lato software: la stessa traiettoria produce CloU e Serberus
CloU, costruito sugli LCM e su solutori SMT, ha trovato 5 dei 7 nuovi gadget Spectre in librerie molto studiate come OpenSSL e Libsodium. Serberus, a sua volta, viene presentato nell’articolo come la prima difesa compiler-based completa per proteggere codice constant-time da Spectre su hardware esistente, formalmente corretta rispetto al contratto operativo ASP.
E il paper aggiunge un dettaglio di enorme interesse industriale: a valle di questo lavoro, Intel ha aggiornato la propria guidance di sicurezza software per confermare che due sue microarchitetture rispettano ASP.
È difficile immaginare una prova più forte del fatto che il confine tra paper e roadmap di vendor sia già stato attraversato.
Perché SynthLC cambia davvero le regole del gioco
Non verifica soltanto se il design “funziona”: estrae firme di leakage verificabili, confrontabili con l’intento del progettista e riusabili come evidenza di assurance.
L’angolo dell’AI: accelerare il design o i bug
Un passaggio dell’articolo che merita attenzione speciale, perché tocca un nervo scoperto del 2026: l’uso dell’AI nel design hardware.
Trippel non adotta toni apocalittici, ma il messaggio è inequivocabile.
Con l’aumento della trazione degli strumenti AI-driven nello spazio hardware, il numero di bug pre-silicon da trovare e correggere tenderà con ogni probabilità a crescere.
Il motivo non è solo la qualità iniziale dei dati di training: è, più a monte, l’ambiguità delle specifiche in linguaggio naturale, che ammettono implementazioni plausibili ma non allineate all’intento del progettista.
Dunque, l’AI può accelerare la produzione di RTL. Senza contratti formali e
verifica forte, può accelerare anche la produzione di errori.
La stessa agenda di ricerca di Stanford insiste proprio su questo punto: formal methods e automated reasoning non sono un freno all’AI nel design, ma la condizione che può renderla governabile.
L’inferenza strategica, qui, è difficile da evitare: più il settore si affiderà a strumenti generativi per property generation, RTL authoring o traduzione di specifiche, più il mercato premierà chi saprà chiudere quel ciclo con verifica automatizzata, dataset di qualità e contratti formali ben definiti.
In altre parole, il prossimo vantaggio competitivo non nascerà dall’AI “da sola”, ma dall’AI disciplinata da assurance.
La chiusura che conta: fiducia ingegnerizzata o prodotti indifendibili
Alla fine, la questione non è se i contratti hardware-software diventeranno rilevanti. Lo sono già.
La vera domanda è chi riuscirà a trasformarli prima in un linguaggio di prodotto, di governance e di conformità.
Per i CISO delle aziende che progettano semiconduttori, per i responsabili security degli OEM, per chi governa piattaforme di confidential computing o apparati per settori regolati, il messaggio è netto: l’epoca della sicurezza come patch reattiva del silicio sta finendo.
Inizia l’epoca della fiducia ingegnerizzata. Non significa che ogni vendor debba domani riscrivere da zero la propria ISA o adottare integralmente l’intero arsenale formale nato in laboratorio.
Significa però che non è più difendibile un modello in cui il chip promette poco, documenta meno e verifica in ritardo.
In un mercato che va verso requisiti di sicurezza più stringenti lungo il ciclo di vita dei prodotti digitali, è ragionevole aspettarsi che la capacità di dimostrare contratti, leakage model e verifica robusta diventi sempre più un elemento di credibilità verso clienti, auditor e autorità.
E da qui discende la vera call to action. Chi non inizia oggi a costruire contratti hardware-software verificabili, domani rischia di trovarsi con prodotti non solo vulnerabili, ma difficili da difendere commercialmente, tecnicamente e dal punto di vista della compliance.
