TU Darmstadt / ULB / TUbiblio

Semantics-Based Cache-Side-Channel Quantification in Cryptographic Implementations

Weber, Alexandra (2022)
Semantics-Based Cache-Side-Channel Quantification in Cryptographic Implementations.
Technische Universität Darmstadt
doi: 10.26083/tuprints-00021208
Dissertation, Erstveröffentlichung, Verlagsversion

Kurzbeschreibung (Abstract)

Performance has been and will continue to be a key criterion in the development of computer systems for a long time. To speed up Central Processing Units (CPUs), micro-architectural components like, e.g., caches and instruction pipelines have been developed. While caches are indispensable from a performance perspective, they also introduce a security risk. If the interaction of a software implementation with a cache differs depending on the data processed by the software, an attacker who observes this interaction can deduce information about the processed data. If the dependence is unintentional, it is called a cache side channel. Cache side channels have been exploited to recover entire secret keys from numerous cryptographic implementations.

There are ways to mitigate the leakage of secret information like, e.g., crypto keys through cache side channels. However, such mitigations come at the cost of performance loss, because they cancel out the performance benefits of caching either selectively or completely. That is, there is a security-performance trade-off that is inherent in the mitigation of cache-side-channel leakage. This security-performance trade-off can only be navigated in an informed fashion if reliable quantitative information on the cache-side-channel security of an implementation is available. Quantitative security guarantees can be computed based on program analyses. However, the existing analyses either do not consider caches, do not provide quantitative guarantees across all side-channel output values, or are only applicable to a limited range of crypto implementations.

In this thesis, we propose a suite of program analyses that can provide quantitative security guarantees in the form of reliable upper bounds on the cache-side-channel leakage of a variety of real-world cryptographic implementations. Technically, our program analyses are based on a combination of information theory and abstract interpretation. The distinguishing feature of each analysis is the underlying abstraction of the execution environment and program semantics.

Our first program analysis is based on an abstraction that captures the state of a CPU with a regular Arithmetic Logic Unit (ALU) during the execution of x86 instructions. In particular, our abstraction captures two status flags that are used, e.g., during the execution of different AES implementations. Our analysis is capable of computing quantitative cache-side-channel security guarantees for off-the-shelf AES implementations from multiple popular libraries. In a comparative study, we clarify the security impact of design choices in these implementations. For instance, we find that the number and size of lookup tables used for just the last transformation round of AES already has a significant impact on the guarantees for the entire implementation.

Our second program analysis is based on an abstraction that captures the execution of additional x86 instructions, including instructions that process larger operands. This abstraction can be used to quantify the leakage of crypto implementations that are based on large parameters. For instance, the lattice-based signature scheme ring-TESLA has a maximum key size of 49152 bit. With our analysis, we successfully computed leakage bounds for the implementation of ring-TESLA. These bounds lead to the detection of multiple vulnerabilities that might be exploited to break the entire signature scheme. As a result, mitigations were integrated into the implementations of ring-TESLA and qTESLA, before the latter was submitted to the NIST PQC standardization.

Our third program analysis is based on an abstraction that captures the state of a CPU with an ALU and a Floating-Point Unit. It can be used to compute leakage bounds for crypto implementations that rely on floating-point instructions, e.g., to compute probabilities. The software used in Quantum Key Distribution (QKD), e.g., heavily relies on probabilities to perform error correction. With our analysis, we computed leakage bounds for a QKD implementation and detected a vulnerability that might leak the entire secret key. We proposed a mitigation and verified its effectiveness using our analysis. In the new version of the implementation, which is used at the TU Darmstadt Department of Physics, our mitigation is already integrated.

Finally, we broaden the scope to side channels that arise from the combination of caching and instruction pipelining. Such side channels are exploited, e.g., by the Spectre-PHT attack. The fourth program analysis in our suite is, to our knowledge, the first ever program analysis that computes reliable quantitative security guarantees with respect to such side channels.

Typ des Eintrags: Dissertation
Erschienen: 2022
Autor(en): Weber, Alexandra
Art des Eintrags: Erstveröffentlichung
Titel: Semantics-Based Cache-Side-Channel Quantification in Cryptographic Implementations
Sprache: Englisch
Referenten: Mantel, Prof. Dr. Heiko ; Malacaria, Prof. Dr. Pasquale
Publikationsjahr: 2022
Ort: Darmstadt
Kollation: x, 132 Seiten
Datum der mündlichen Prüfung: 21 April 2022
DOI: 10.26083/tuprints-00021208
URL / URN: https://tuprints.ulb.tu-darmstadt.de/21208
Kurzbeschreibung (Abstract):

Performance has been and will continue to be a key criterion in the development of computer systems for a long time. To speed up Central Processing Units (CPUs), micro-architectural components like, e.g., caches and instruction pipelines have been developed. While caches are indispensable from a performance perspective, they also introduce a security risk. If the interaction of a software implementation with a cache differs depending on the data processed by the software, an attacker who observes this interaction can deduce information about the processed data. If the dependence is unintentional, it is called a cache side channel. Cache side channels have been exploited to recover entire secret keys from numerous cryptographic implementations.

There are ways to mitigate the leakage of secret information like, e.g., crypto keys through cache side channels. However, such mitigations come at the cost of performance loss, because they cancel out the performance benefits of caching either selectively or completely. That is, there is a security-performance trade-off that is inherent in the mitigation of cache-side-channel leakage. This security-performance trade-off can only be navigated in an informed fashion if reliable quantitative information on the cache-side-channel security of an implementation is available. Quantitative security guarantees can be computed based on program analyses. However, the existing analyses either do not consider caches, do not provide quantitative guarantees across all side-channel output values, or are only applicable to a limited range of crypto implementations.

In this thesis, we propose a suite of program analyses that can provide quantitative security guarantees in the form of reliable upper bounds on the cache-side-channel leakage of a variety of real-world cryptographic implementations. Technically, our program analyses are based on a combination of information theory and abstract interpretation. The distinguishing feature of each analysis is the underlying abstraction of the execution environment and program semantics.

Our first program analysis is based on an abstraction that captures the state of a CPU with a regular Arithmetic Logic Unit (ALU) during the execution of x86 instructions. In particular, our abstraction captures two status flags that are used, e.g., during the execution of different AES implementations. Our analysis is capable of computing quantitative cache-side-channel security guarantees for off-the-shelf AES implementations from multiple popular libraries. In a comparative study, we clarify the security impact of design choices in these implementations. For instance, we find that the number and size of lookup tables used for just the last transformation round of AES already has a significant impact on the guarantees for the entire implementation.

Our second program analysis is based on an abstraction that captures the execution of additional x86 instructions, including instructions that process larger operands. This abstraction can be used to quantify the leakage of crypto implementations that are based on large parameters. For instance, the lattice-based signature scheme ring-TESLA has a maximum key size of 49152 bit. With our analysis, we successfully computed leakage bounds for the implementation of ring-TESLA. These bounds lead to the detection of multiple vulnerabilities that might be exploited to break the entire signature scheme. As a result, mitigations were integrated into the implementations of ring-TESLA and qTESLA, before the latter was submitted to the NIST PQC standardization.

Our third program analysis is based on an abstraction that captures the state of a CPU with an ALU and a Floating-Point Unit. It can be used to compute leakage bounds for crypto implementations that rely on floating-point instructions, e.g., to compute probabilities. The software used in Quantum Key Distribution (QKD), e.g., heavily relies on probabilities to perform error correction. With our analysis, we computed leakage bounds for a QKD implementation and detected a vulnerability that might leak the entire secret key. We proposed a mitigation and verified its effectiveness using our analysis. In the new version of the implementation, which is used at the TU Darmstadt Department of Physics, our mitigation is already integrated.

Finally, we broaden the scope to side channels that arise from the combination of caching and instruction pipelining. Such side channels are exploited, e.g., by the Spectre-PHT attack. The fourth program analysis in our suite is, to our knowledge, the first ever program analysis that computes reliable quantitative security guarantees with respect to such side channels.

Alternatives oder übersetztes Abstract:
Alternatives AbstractSprache

Performanz spielt schon seit langer Zeit eine wichtige Rolle in der Entwicklung von Computersystemen. Auf Mikroarchitekturebene werden verschiedene Komponenten eingesetzt, um die Ausführungsgeschwindigkeit zu erhöhen. Insbesondere Caches sind aus modernen Computerarchitekturen nicht mehr wegzudenken. Gleichzeitig bergen Caches allerdings ein Sicherheitsrisiko. Hängt die Cachenutzung einer Softwareimplementierung von den verarbeiteten Daten ab, dann kann ein Beobachter aus der Cachenutzung Rückschlüsse auf diese Daten ziehen. Im Falle einer unbeabsichtigten Abhängigkeit handelt es sich um einen sogenannten Cacheseitenkanal. Solche Kanäle werden oft ausgenutzt, um geheime Schlüssel aus Kryptoimplementierungen zu extrahieren.

Es gibt verschiedene Gegenmaßnahmen, um Cacheseitenkanäle zu schließen oder zu reduzieren. Allerdings werden dadurch die Vorteile von Caches ganz oder teilweise aufgehoben, sodass sich die Performanz verschlechtert. Es muss also zwischen Sicherheit und Performanz abgewogen werden. Um informiert über Seitenkanalgegenmaßnahmen entscheiden zu können, werden quantitative Informationen über das Ausmaß des jeweiligen Cacheseitenkanals benötigt. Solche quantitativen Sicherheitsgarantien können grundsätzlich mithilfe von Programmanalysen hergeleitet werden. Die bisherigen Analysen sind allerdings entweder nicht quantitativ, berücksichtigen keine Caches, oder sie sind nicht für ein breites Spektrum realer Kryptoimplementierungen anwendbar.

Diese Dissertation präsentiert eine Toolsuite aus Programmanalysen, die verlässliche quantitative Sicherheitsgarantien in Form von oberen Schranken für die durch Cacheseitenkanäle preisgegebenen Informationen in verschiedenen Kryptoimplementierungen bestimmen können. Die Analysen basieren auf Informationstheorie und Abstract Interpretation. Sie setzen dabei verschiedene neuartige abstrakte Repräsentationen von Programmausführungen ein.

Die erste Programmanalyse basiert auf einer Abstraktion eines x86-Prozessors mit Arithmetisch-logischer Einheit (ALU). Diese Abstraktion berücksichtigt zwei Statusflags, die beispielsweise bei der Ausführung von AES-Implementierungen verschiedener Kryptobibliotheken verwendet werden. Dadurch kann die Analyse quantitative Sicherheitsgarantien für solche Implementierungen bestimmen. Mithilfe der Analyse klären wir auch, welchen Einfluss Designentscheidungen in AES-Implementierungen auf deren Cacheseitenkanalsicherheit haben. So kann beispielsweise die Nutzung verschiedener Lookuptabellen allein in der letzten AES-Transformationsrunde die Sicherheitsgarantien für die Gesamtimplementierung bereits signifikant beeinflussen.

Die zweite Programmanalyse basiert auf einer Abstraktion, die Instruktionen mit größeren Operanden berücksichtigt. Sie kann quantitative Sicherheitsgarantien auch für Implementierungen mit großen Parametern berechnen. In der Implementierung des ring-TESLA-Signaturverfahrens, dessen maximale Schlüsselgröße 49152 bit beträgt, konnten durch unsere Analyse mehrere Cacheseitenkanäle gefunden werden. Entsprechende Gegenmaßnahmen wurden in die Implementierungen von ring-TESLA und dem Nachfolgeverfahren qTESLA integriert, bevor letzteres zum Standardisierungsprozess für Postquantenkryptographie des NIST eingereicht wurde.

Die dritte Programmanalyse basiert auf einer Abstraktion eines x86-Prozessors mit ALU und Gleitkommaeinheit. Sie kann die Cacheseitenkanalsicherheit von Implementierungen quantifizieren, die Gleitkommainstruktionen z.B. zur Berechnung von Wahrscheinlichkeiten nutzen. Ein Beispiel sind Implementierungen zum Quantenschlüsselaustausch, die Gleitkommainstruktionen für ein Fehlerkorrekturverfahren nutzen. In einer solchen Implementierung konnten wir mit unserer Analyse einen Cacheseitenkanal finden, der zur Preisgabe des gesamten geheimen Schlüssels führen könnte. Um den Kanal zu schließen, entwickelten wir eine Gegenmaßnahme, die mittlerweile in einer neuen Version der Implementierung am Fachbereich Physik der TU Darmstadt genutzt wird.

Abschließend untersuchen wir Seitenkanäle, die aus der Kombination von Cache und Pipeline entstehen und bei Angriffen wie Spectre-PHT ausgenutzt werden. Unsere vierte Programmanalyse kann erstmals verlässliche quantitative Sicherheitsgarantien für solche Kanäle berechnen.

Deutsch
Status: Verlagsversion
URN: urn:nbn:de:tuda-tuprints-212088
Sachgruppe der Dewey Dezimalklassifikatin (DDC): 000 Allgemeines, Informatik, Informationswissenschaft > 004 Informatik
Fachbereich(e)/-gebiet(e): 20 Fachbereich Informatik
20 Fachbereich Informatik > Modellierung und Analyse von Informationssystemen (MAIS)
Hinterlegungsdatum: 09 Mai 2022 12:03
Letzte Änderung: 10 Mai 2022 06:49
PPN:
Referenten: Mantel, Prof. Dr. Heiko ; Malacaria, Prof. Dr. Pasquale
Datum der mündlichen Prüfung / Verteidigung / mdl. Prüfung: 21 April 2022
Export:
Suche nach Titel in: TUfind oder in Google
Frage zum Eintrag Frage zum Eintrag

Optionen (nur für Redakteure)
Redaktionelle Details anzeigen Redaktionelle Details anzeigen