Swarn Priya PhD’s defense:
Formally computer-verified protections against timing-based side-channel attacks
Jury members:
(1) Sandrine Blazy, Professeur et Chercheur, Université de Rennes 1 et IRISA (Rapporteurs)
(2) Karthikeyan Bhargavan, Directeur de recherche Inria, Paris (Rapporteurs)
(3) Étienne Lozes, Professeur des universités Université Cote d’Azur, I3S lab (Examinateurs)
(4) Lesly-Ann Daniel, Docteur, KU Leuven (Examinateaurs)
(5) Yves Bertot, Directeur de recherche, Centre Inria d’Université Côte d’Azur (Advisor)
(6) Benjamin Grégoire, Chargé de recherche, Centre Inria d’Université Côte d’Azur (Co-Advisor)
Title: Formally computer-verified protections against timing-based side-channel attacks
Abstract:
Developers of high-assurance software aim to design functionally correct software with properties like confidentiality. However, confidentiality is not a direct consequence of functional correctness, as there could be unintentional side-channel leaks like execution time that might help the attacker retrieve secret data. For example, a functionally correct algorithm to verify a password is a string-comparison algorithm that compares two strings character by character and exits in case of a mismatch or returns success when strings are equal. However, an attacker can guess the password’s length by measuring the execution time of the algorithm, which means the latter is not secure against timing attacks. More generally, branching on secrets may leak secret data as the two branches may have different execution times. Modern processors use branch prediction to maximize the performance of the program. For example, if the destination of a branch condition leads to a memory read, the processor bypasses the condition check and executes the memory read operation speculatively. In case of misprediction, the processor backtracks and starts the execution again with the correct condition’s result. Though backtracking corrects the misspeculated results, it still leaves a trace in the cache, which the attacker can exploit to get to the secret data (illustrated in Spectre attacks). Thus, the speculation improves overall efficiency at the expense of security.
Side-channel effects are not captured in the classic formal semantics of programs, and hence, these semantics cannot be used to reason about hyperproperties like timing-based side-channel attacks. Without the notion of formal models capturing side-effects produced during a program’s execution, the developers can only manually fix the program to ensure it always takes the same time to execute and assume that the compiler does not break the property while compiling the program to assembly with no formal guarantees. Traditionally, to defend against timing-based side-channel attacks, cryptographers have used the constant-time property to develop programs that do not perform secret-dependent memory access and branching at the source level. Unfortunately, the optimizations performed by the compiler to increase the efficiency of the program tend to break the constant-time property. This calls for the existence of a formal model that captures the side effects produced during a program’s execution.
This thesis aims to provide formal models for capturing the side-effects produced during a program’s execution together with a formal notion of security properties like constant-time and speculative constant-time. The thesis incorporates the development of a formally verified secure compiler that preserves the constant-time property and methodologies to add protections against various kinds of Spectre attacks. It defines type systems that help check the correct usage of these protections and also illustrates an efficient method to protect against Spectre v1 attacks called Selective Speculative Load Hardening. All these works are formally verified using the interactive theorem prover Coq, leading to machine-checked proofs rather than relying on human assurances.
Keywords: Formal verification, Computer-verified proofs, Verified cryptography, Compilation
