Scientific direction Development of key enabling technologies
Transfer of knowledge to industry

PhD : selection by topics

Technological challenges >> Cyber security : hardware and sofware
7 proposition(s).

See all positions [+]

embedded elapsed-time attestation

Département Systèmes (LETI)

Laboratoire Sécurité des Objets et des Systèmes Physiques

01-10-2021

SL-DRT-21-0089

christine.hennebert@cea.fr

Cyber security : hardware and sofware (.pdf)

With the emergence of a protocol that secures a history of transactions on a peer-to-peer network, Bitcoin introduced the first decentralized digital currency in 2009. The security of the Bitcoin protocol is based on the proof of work and common rules and procedures among peers in the network who participate in the consensus, i.e. the choice of the next block of data to be added to the shared and replicated ledger. The proof of work has two major drawbacks. On the one hand, it ensures security by design by requiring nodes participating in the consensus to work with a computing intensity corresponding to the maximum of Moore's law, which is obviously very energy consuming. On the other hand, the parallelization of this proof process with an implementation in ASICs makes the system vulnerable to Sybil-type attacks by recentralizing resources. The mining pools exploit this vulnerability. The present thesis topic aims at building a proof for embedded and resource constrained objects, which ensures the security of a transaction history at low power. The work will focus on the embedded implementation of the proof mechanism on a system-on-module platform using a TPM 2.0 (Trusted Platform Module) security hardware component as root-of-trust. The solution introduced will have to be robust to the above-mentioned drawbacks and vulnerabilities.

Download the offer (.zip)

Automatic design of secure hardware architectures

Département Systèmes et Circuits Intégrés Numériques

Laboratoire Environnement de Conception et Architecture

01-10-2021

SL-DRT-21-0190

caaliph.andriamisaina@cea.fr

Cyber security : hardware and sofware (.pdf)

Embedded systems are more and more ubiquitous and interconnected; they are an attractive target for security attacks. The security aspect is thus becoming more and more important when designing these systems, as a vulnerability in one system can compromise an entire infrastructure of connected systems. Thus, each system contributes to the construction of a global chain of trust. Moreover, given the increasing complexity of the applications running on these systems, it is becoming increasingly difficult to meet all security criteria (for instance application isolation, system authentication, secret and private data protection, communications protection). The design of these systems therefore requires an in-depth analysis of the various security constraints to which they are subject, based on a threat model associated with the potential attacker. While extra-functional design objectives such as performance, power consumption and area are generally well taken into account during the very early stages of embedded system design, security is still generally considered afterwards, leading to security solutions seen as an addition to the initial system. This design approach needs to be reconsidered in order to develop solutions that integrate security by construction and no longer as an additional element. The objective of this thesis is thus to take into account the security constraints in addition to the performance, power consumption and area constraints during the design space exploration (DSE) of hardware architectures in order to automatically generate an architecture optimized with respect to all these constraints. This study will begin with an analysis of the threat models in particular with respect to hardware attacks and existing countermeasures at the hardware level. Then, the security modeling and quantifying in the context of DSE will be carried out, as it will be essential to clearly characterize the techniques and approaches for taking into account the security needs of the systems. From this step, the candidate will propose a DSE flow of hardware architectures taking into account security constraints, in addition to power consumption, performance and area constraints. The goal is to be able to analyze the security, area, power consumption and performance trade-offs according to the designers' specifications at both functional and non-functional levels. This flow will then be applied to a practical case of hardware architecture design in order to validate the developed DSE approach. The developed solutions will have to demonstrate their level of robustness with respect to the security constraint in order to guarantee the security of the systems while respecting and optimizing the other design constraints.

Download the offer (.zip)

Proof of functional equivalence of binary codes in the context of programs hardening

Département Systèmes et Circuits Intégrés Numériques

Laboratoire Fonctions Innovantes pour circuits Mixtes

01-10-2021

SL-DRT-21-0192

damien.courousse@cea.fr

Cyber security : hardware and sofware (.pdf)

The general context of this thesis is the cyber-security of embedded systems. The research background of this thesis is tied to the automatic application of counter-measures against the so-called physical attacks, which encompass observation attacks (side-channel attacks) and perturbation attacks (fault-injection attacks). The CEA List is working on COGITO, a compiler toolchain based on LLVM for the automatic application of software counter-measures against physical attacks. Given a source-level implementation of an unprotected program, our toolchain produces an optimised binary program including targeted counter-measures, such that the compiled program is hardened against a specified threat model. Two key points are today crucial to trust the compiled programs: 1. the proof of robustness of programs produced by our toolchain, 2. the proof that adding counter-measures does not alter the functionality of the target programs. This thesis will target the second point: bringing formal guarantees about the functional correctness of the secured programs. We will use sound and exhaustive symbolic reasoning, supported by BINSEC (). BINSEC is an open-source toolset developed at CEA List to help improve software security at the binary level. It relies on cutting-edge research in binary code analysis, at the intersection of formal methods, program analysis, security and software engineering. The PhD thesis will be hosted at the CEA in Grenoble, in a multidisciplinary environment including experts in embedded software, cyber-security, hardware design, and machine learning. Short-term stays at the DILS at the CEA in Saclay will be planned throughout the three years of the thesis to collaborate with experts and developers of BINSEC.

Download the offer (.zip)

Formal verification of hardware micro-architectures to analyze the influence of faults injection and the robustness of countermeasures

Département Systèmes et Circuits Intégrés Numériques

Laboratoire Environnement de Conception et Architecture

01-10-2021

SL-DRT-21-0276

Mathieu.Jan@cea.fr

Cyber security : hardware and sofware (.pdf)

The never race towards higher average performance for numerical systems leads to increase the complexity of modern hardware architectures. This threatens the design of secure embedded systems as it opens new attack vectors. For example, the Spectre family of attacks exemplifies the issues that speculative execution mechanisms can raise in modern processor architectures. In the context of this PhD proposal, the more complex a processor architecture is, the larger is the attack surface exploitable by fault injection attacks. Such attacks, performed by the means of a physical perturbation of the circuit, aim at exploiting a logical perturbation in the computing for various purposes: leaking secrets, bypassing authentication procedures, escalation of privileges, etc. The modeling of the logical effects of a physical perturbation over numerical systems has been studied extensively, but it is still challenging to model precisely. Furthermore, recent research work has shown that inducing faults in the processor microarchitecture can lead to subtle effects, opening interesting research questions about the modeling and the analysis of such effects, and possible mitigations. The objective of this PhD thesis is to investigate formal approaches on the hardware side to better understand the consequences of fault injections, as well as to verify the efficiency of countermeasures shipped in secure embedded systems.

Download the offer (.zip)

Fuzzing techniques to support static security analyses

Département Ingénierie Logiciels et Systèmes (LIST)

Laboratoire pour la Sûreté du Logiciel

01-10-2021

SL-DRT-21-0557

michael.marcozzi@cea.fr

Cyber security : hardware and sofware (.pdf)

Guaranteeing digital security is a crucial issue. In this context, static analyses and fuzzing are popular approaches making it possible to detect software vulnerabilities directly at the binary level. The two approaches are complementary: static analyses can either provide guarantees that the program is safe, or report possibly unsafe program executions. On the contrary, fuzzing cannot provide any strict guarantee about program security, but is able to identify executions that exhibit a vulnerability for sure. In this thesis, we will thus take advantage of fuzzing to confirm vulnerability reports from static analysis. This will require us to develop a fuzzer able to target the possibly insecure executions identified by the static analyser. This is quite challenging as targeted fuzzing is a difficult and underresearched domain. In addition, static analysers provide rather loose descriptions of the possibly vulnerable executions, making the fuzzer's task even harder. To overcome these challenges, we will take advantage of tried and tested solutions from the fields of search-based testing and advanced coverage criteria, which have been underexploited in the field of fuzzing. The developed fuzzer will be evaluated at scale in real use cases and we will measure how much it enables a better prioritisation and a more precise elaboration of vulnerability reports. Finally, we will provide elements of generalisation, making targeted fuzzing more adaptable to problems sharing similarities with confirming vulnerability reports.

Download the offer (.zip)

Speculating About Low-level Security

Département Ingénierie Logiciels et Systèmes (LIST)

Laboratoire pour la Sûreté du Logiciel

SL-DRT-21-0559

sebastien.bardin@cea.fr

Cyber security : hardware and sofware (.pdf)

We consider the general context of automated code-level security analysis. While standard attacks such as control-flow hijacking take advantage of programming flaws (typically, missing bound checks), recent micro-architectural attacks take advantage of subtle behaviours at the micro-architectural levels, typically speculative behaviours introduced in modern architectures for efficiency, in order to bypass protections and leak sensitive data. These vulnerabilities are extremely hard to find by a human expert, as they require to reason at a very low-level, on an exponential number of otherwise-hidden speculative behaviours, and on complex security properties (leaks and data interference, rather than standard memory corruptions). The goal of this doctoral work is to understand how automated symbolic verification and bug finding methods (especially but not limited to, symbolic execution) can be efficiently lifted to the case of speculative micro-architectural attacks, with the ultimate goal of securing essential security primitives in cryptographic libraries and OS kernels. This general objective raises challenges in terms of semantics of speculative behaviours, semantics of security properties and scalability of verification techniques. These techniques will be implemented in the binary-level code analysis framework BINSEC and their benefits assessed through rigorous experimental evaluation.

Download the offer (.zip)

Distributed intrusion detection in a constrained edge network context

Département Intelligence Ambiante et Systèmes Interactifs (LIST)

Laboratoire Systèmes Communiquants

01-09-2021

SL-DRT-21-0965

alexis.olivereau@cea.fr

Cyber security : hardware and sofware (.pdf)

The objective of the proposed PhD thesis is to define a distributed, autonomous, and reactive security system able to reconfigure itself in real time in order to take into account in particular the possible attacks, the traffic pattern to be monitored and its own resources. In this system, intrusion detection probes are essential components. They implement anomaly-based detection using artificial intelligence, capable of detecting weak signals in a potentially very high-speed environment. The analyses of the different probes are correlated in order to increase the overall capacity to identify malicious behavior on the scale of the network to be protected. Finally, the question of energy efficiency is to be considered both at the level of individual probes and that of the orchestration of the global monitoring function. PhD thesis subject proposed in the framework of the European GREENEDGE project: https://greenedge-itn.eu/wp-content/uploads/2021/03/ESR11_description.pdf All applications must be submitted via the GREENEDGE project website: https://greenedge-itn.eu/phd-hiring-call/

Download the offer (.zip)

See all positions