Building a framework for constant-time analysis of cryptographic SW on embedded systems.

In this work the problem of constant-time attacks, a subclass of side-channel attacks, is addressed, with particular attention to the implications in embedded systems. The main focus is developing an automated framework, capable of running different tools to analyze cryptographic libraries on the board and identify any vulnerabilities. If such vulnerabilities are not present, the framework confirms that the library is implemented in constant time. Each tool performs its own analysis, using techniques such as statistical tests, formal verification or symbolic analysis, which will be discussed in detail in the following chapters. The framework was developed in Rust, a choice that will be justified during the course of the work. The first step was to study the State-Of-The-Art of the existing tools. There are a lot of tools that verify if a code is written in constant time, other tools perform the analysis directly from the binary code. This distinction depends on the type of analysis on which the tool is based. It is possible to distinguish two macro areas: • Formal tools • Dynamic tools Among the formal tools we have a predominance of static analyses, which are based on the abstrac- tion of binary code, converted into a mathematical model and conclude with a formal verification of requirements and mathematical properties. On the other hand, among dynamic tools, we find some tools that use a purely symbolic approach to detect vulnerabilities, while others check at runtime for time differences in the execution of the source code. Symbolic analysis, unlike formal analysis, does not test the correctness of the code in the form of mathematical models, but explores every possible scenario using symbolic values instead of concrete ones, to find those conditions in which the program behaves unexpectedly. Once the most promising tools have been studied and selected, they have been tested to check their operation. First by small demonstration tests and then implementing concrete projects using some open source libraries. For the analysis have been selected three cryptographic libraries, executed on a particular board such as STM32L4. The libraries analyzed are: • MbedTLS, known to be vulnerable to this type of attack. • BearSSL, written entirely in constant-time but not optimized, with the aim of being compat- ible with different architectures. • STM32 cryptographic library, written entirely in constant-time and implemented to be run on the STM32 microcontrollers. This allowed us to check the quality of the tools and decide whether to continue testing them, and if so integrate them into the framework, or discard them.