A methodology based on functional languages for the design of hardware cryptographic primitives resistant to side-channel attacks

The security of hardware cryptographic primitives is critically affected by a class of vulnerabilities due to the unintended leakage, occurring in physical devices, of sensitive information. Attacks against implementations, known as "side-channel" attacks, exploit unexpected physical output channels, such as the instantaneous power consumption, to break cryptographic algorithms otherwise thought as secure. Consequently, hardware cryptographic primitives must be equipped with specific countermeasures that mitigate the side-channel vulnerability of the physical implementations. However, there is an obvious lack of established methodologies for dealing with the design and the implementation of cryptographic primitives protected against side-channel attacks. As a result, the current development process is both onerous and error-prone. The main goal of this thesis is to explore the feasibility of a new hardware design methodology, suitable for closing the gap that exists between current hardware design practices and the diverse set of side-channel cryptanalysis techniques for the assessment of the security vulnerability of cryptographic circuits. We propose to rely on special functional programming patterns for developing a number of domain-specific languages (DSLs) as the basis for the specification, the implementation and the verification of secure designs. We built an instrumentation framework that relies on a new "polymorphic" domain-specific embedded language (DSEL), within Haskell, which can be arbitrarily re-evaluated according to multiple language interpretations. In this way, we manage to perform the variety of validation tasks needed, as well as to generate an industry-standard synthesizable RTL description (written in VHDL or Verilog), starting from the very same high-level circuit specification. We provide an experimental evaluation about the effectiveness of our approach in assisting the design-space exploration of protected primitives, and we demonstrate its actual feasibility in a real-world scenario.

La sicurezza delle primitive hardware che realizzano algoritmi crittografici è gravemente compromessa da una classe di vulnerabilità dovute alla dispersione accidentale, da parte dei dispositivi fisici, di informazioni sensibili. Gli attacchi contro le implementazioni, conosciuti come attacchi "side-channel", sfruttano fonti di output non intenzionali, come il consumo istantaneo di potenza, per infrangere algoritmi crittografici considerati sicuri. Di conseguenza, le primitive crittografiche hardware devono obbligatoriamente essere equipaggiate con particolari contromisure, in grado di mitigare le vulnerabilità side-channel delle implementazioni fisiche. Tuttavia, c'è una evidente carenza di metodologie consolidate per gestire il design e l'implementazione di primitive crittografiche protette contro attacchi side-channel. Come conseguenza, attualmente il processo di progettazione di primitive crittografiche protette contro gli attacchi side-channel è parecchio oneroso nonché soggetto ad errori. L'obiettivo principale di questa tesi è quello di esplorare la fattibilità di una nuova metodologia di progettazione hardware, in grado di ridurre il divario tra le metodologie di progettazione esistenti, da una parte, e la variegata collezione di tecniche di crittoanalisi per la valutazione delle vulnerabilità side-channel dei circuiti crittografici, dall'altra. Proponiamo di fare affidamento su speciali pattern di programmazione funzionale per lo sviluppo di una serie di domain-specific languages (DSL) come base per la specifica, l'implementazione e la verifica di design sicuri. Abbiamo sviluppato un framework di verifica basato su un nuovo DSL "polimorfico", integrato in Haskell (domain-specific embedded language, o DSEL), che può essere arbitrariamente valutato secondo diverse interpretazioni semantiche. In questo modo, siamo in grado di eseguire le varie procedure di verifica necessarie, così come di generare automaticamente una specifica RTL del circuito (scritta in VHDL o Verilog), sintetizzabile per mezzo di strumenti industry-standard, a partire dalla medesima specifica ad alto livello. Forniamo infine una valutazione sperimentale sull'efficacia del nostro approccio nel facilitare l'esplorazione dello spazio delle soluzioni, per quanto riguarda le primitive hardware protette da contromisure, e ne proveremo la concreta fattibilità.