Les attaques par canaux cachés sont une forme d'attaque particulièrement dangereuse. Dans cette thèse, nous nous intéressons au canal caché temporel. Un programme est dit ''constant-time'' lorsqu'il n'est pas vulnérable aux attaques par canal caché temporel. Nous présentons dans ce manuscrit deux méthodes reposant sur l'analyse statique afin de s'assurer qu'un programme est constant-time. Ces méthodes se placent dans le cadre de vérification formelle afin d'obtenir le plus haut niveau d'assurance possible en s'appuyant sur une chaîne de compilation vérifiée composée du compilateur CompCert et de l'analyseur statique Verasco. Nous proposons aussi une méthode de preuve afin de s'assurer qu'un compilateur préserve la propriété de constant-time lors de la compilation d'un programme. / Side-channel attacks are an especially dangerous form of attack. In this thesis, we focus on the timing side-channel. A program is said to be constant-time if it is not vulnerable to timing attacks. We present in this thesis two methods relying on static analysis in order to ensure that a program is constant-time. These methods use formal verification in order to gain the highest possible level of assurance by relying on a verified compilation toolchain made up of the CompCert compiler and the Verasco static analyzer. We also propose a proof methodology in order to ensure that a compiler preserves constant-time security during compilation.

Geothermal energy is an important source of clean and renewable energy. This project deals with the study of deep geothermal power plants for the generation of electricity. The design involves the extraction of heat from the Earth and its conversion into electricity. This is performed by allowing fluid deep into the Earth where it gets heated due to the surrounding rock. The fluid gets vaporized and returns to the surface in a heat pipe. Finally, the energy of the fluid is converted into electricity using turbine or organic rankine cycle (ORC). The main feature of the system is the employment of side channels to increase the amount of thermal energy extracted. A finite difference computer model is developed to solve the heat transport equation. The numerical model was employed to evaluate the performance of the design. The major goal was to optimize the output power as a function of parameters such as thermal diffusivity of the rock, depth of the main well, number and length of lateral channels. The sustainable lifetime of the system for a target output power of 2 MW has been calculated for deep geothermal systems with drilling depths of 8000 and 10000 meters, and a financial analysis has been performed to evaluate the economic feasibility of the system for a practical range of geothermal parameters. Results show promising an outlook for deep geothermal systems for practical applications.

The nodes in wireless sensor networks (WSNs) utilize the radio frequency (RF) channel to communicate. Given that the RF channel is the primary communication channel, many researchers have developed techniques for securing that channel. However, the RF channel is not the only interface into a sensor. The sensing components, which are primarily designed to sense characteristics about the outside world, can also be used (or misused) as a communication (side) channel. In our work, we aim to characterize the side channels for various sensory components (i.e., light sensor, acoustic sensor, and accelerometer). While previous work has focused on the use of these side channels to improve the security and performance of a WSN, we seek to determine if the side channels have enough capacity to potentially be used for malicious activity. Specifically, we evaluate the feasibility and practicality of the side channels using today's sensor technology and illustrate that these channels have enough capacity to enable the transfer of common, well-known malware. Given that a significant number of modern robotic systems depend on the external side channels for navigation and environment-sensing, they become potential targets for side-channel attacks. Therefore, we demonstrate this relatively new form of attack which exploits the uninvestigated but predominantly used side channels to trigger malware residing in real-time robotic systems such as the iRobot Create. The ultimate goal of our work is to show the impact of this new class of attack and also to motivate the need for an intrusion detection system (IDS) that not only monitors the RF channel, but also monitors the values returned by the sensory components.

Geothermal energy is an important source of clean and renewable energy. This project deals with the study of deep geothermal power plants for the generation of electricity. The design involves the extraction of heat from the Earth and its conversion into electricity. This is performed by allowing fluid deep into the Earth where it gets heated due to the surrounding rock. The fluid gets vaporized and returns to the surface in a heat pipe. Finally, the energy of the fluid is converted into electricity using turbine or organic rankine cycle (ORC). The main feature of the system is the employment of side channels to increase the amount of thermal energy extracted. A finite difference computer model is developed to solve the heat transport equation. The numerical model was employed to evaluate the performance of the design. The major goal was to optimize the output power as a function of parameters such as thermal diffusivity of the rock, depth of the main well, number and length of lateral channels. The sustainable lifetime of the system for a target output power of 2 MW has been calculated for deep geothermal systems with drilling depths of 8000 and 10000 meters, and a financial analysis has been performed to evaluate the economic feasibility of the system for a practical range of geothermal parameters. Results show promising an outlook for deep geothermal systems for practical applications.

Protokol TLS je komplexní a jeho použití je široce rozšířené. Mnoho zařízení používá TLS na ustanovení bezpečné komunikace, vzniká tak potřeba tento protokol důkladně testovat. Tato diplomová práce se zaměřuje na útoky přes časové postranní kanály, které se znovu a znovu objevují jako variace na už známé útoky. Práce si klade za cíl usnadnit korektní odstranění těchto postranních kanálů a předcházet vzniku nových vytvořením automatizovaného frameworku, který pak bude integrován do nástroje tlsfuzzer, a vytvořením testovacích scénářů pro známé útoky postranními kanály. Vytvořené rozšíření využívá program tcpdump pro sběr časových údajů a statistické testy spolu s podpůrnými grafy k rozhodnutí, zda se jedná o možný postranní kanál. Rozšíření bylo zhodnoceno pomocí nových testovacích skriptů a byla předvedena jeho dobrá schopnost rozlišit postranní kanál. Rozšíření spolu s testy je nyní součástí nástroje tlsfuzzer.

La sécurité des applications sur le web est totalement dépendante de leur design et de la robustesse de l'implémentation des algorithmes et protocoles cryptographiques sur lesquels elles s'appuient. Cette thèse présente une nouvelle approche, applicable à de larges projets, pour vérifier l'état de l'art des algorithmes de calculs sur les grands nombres, tel que rencontrés dans les implémentations de référence. Le code et les preuves sont réalisés en F*, un langage orienté preuve et qui offre un système de types riche et expressif. L'implémentation et la vérification dans un langage d'ordre supérieur permet de maximiser le partage de code mais nuit aux performances. Nous proposons donc un nouveau langage, Low*, qui encapsule un sous ensemble de C en F* et qui compile vers C de façon sûre. Low* conserve toute l'expressivité de F* pour les spécifications et les preuves et nous l'utilisons pour implémenter de la cryptographie, en y intégrant les optimisations des implémentations de référence. Nous vérifions ce code en termes de sûreté mémoire, de correction fonctionnelle et d'indépendance des traces d'exécution vis à vis des données sensibles. Ainsi, nous présentons HACL*, une bibliothèque cryptographique autonome et entièrement vérifiée, dont les performances sont comparables sinon meilleures que celles du code C de référence. Plusieurs algorithmes de HACL* font maintenant partie de la bibliothèque NSS de Mozilla, utilisée notamment dans Firefox et dans RedHat. Nous appliquons les mêmes concepts sur miTLS, une implémentation de TLS vérifiée et montrons comment étendre cette méthodologie à des preuves cryptographiques, du parsing de message et une machine à état. / The security of Internet applications relies crucially on the secure design and robust implementations of cryptographic algorithms and protocols. This thesis presents a new, scalable and extensible approach for verifying state-of-the-art bignum algorithms, found in popular cryptographic implementations. Our code and proofs are written in F∗, a proof-oriented language which offers a very rich and expressive type system. The natural way of writing and verifying higher-order functional code in F∗ prioritizes code sharing and proof composition, but this results in low performance for cryptographic code. We propose a new language, Low∗, a fragment of F∗ which can be seen as a shallow embedding of C in F∗ and safely compiled to C code. Nonetheless, Low∗ retains the full expressiveness and verification power of the F∗ system, at the specification and proof level. We use Low∗ to implement cryptographic code, incorporating state-of-the-art optimizations from existing C libraries. We use F∗ to verify this code for functional correctness, memory safety and secret in- dependence. We present HACL∗, a full-fledged and fully verified cryptographic library which boasts performance on par, if not better, with the reference C code. Several algorithms from HACL∗ are now part of NSS, Mozilla’s cryptographic library, notably used in the Firefox web browser and the Red Hat operating system. Eventually, we apply our techniques to miTLS, a verified implementation of the Transport Layer Security protocol. We show how they extend to cryptographic proofs, state-machine implementations and message parsing verification.

Issues of this thesis are focused on side-channel cryptanalysis. Particularly attention is paid to differential power analysis, when is simulated an attack on the cryptographic module for different conditions and for different structural features of this module. As the cryptographic module is used a PIC microcontroller, which is operating with AES symmetric encryption algorithm. For this purpose, a design of experimental printed circuit board was created. Then, this PCB was equipped only with the necessary components for the function of the cryptographic module. Cryptanalysis is aimed on current consumption of crypto module that is caused by execution of AddRoundKey instructions. Power consumption of PIC microcontroller is measured in depending on the size of power supply voltage, size of serial resistor, size of bypass capacitor, and this thesis also examines the influence of ambient temperature on power consumption of PIC. The measured values are graphically presented and then discussed.

Side channels fundamentally changes the view of the cryptographic system security in cryptography. It is not enough to analyze the security algorithm only from a mathematical point of view using abstract models but it is necessary to focus on the implementation of the algorithms. The introduction of the thesis deals with the basic terms, principles of side channel attacks and basic clasification of side channels. The following chapter describes the objectives of the thesis. The main goal of the thesis is to propose and experimentally verify a new power analysis method whish will use the neural network. This main goal was based on the realized analyzes presented in the following chapters. These chapters contain a detailed analysis of currently used power analysis and analysis of AES encryption algorithm. AES was selected becouse the algorithm is resistant to the conventional cryptoanalysis. The following section describes the experimental results of the optimization of existing methods, the influence of the parameters affecting power consumption and the results of the proposed analysis using neural networks. This section includes the discussion of the results. This type of side channel attack has not been published yet thus it is a completely new idea. The final goal of the thesis was to summarize the possible countermeasures protecting against the side channel attacks.