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

PhD : selection by topics

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

See all positions [+]

Safety/Security Modeling for Security Characterization of Industrial Control Systems

Département Systèmes (LETI)

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

01-10-2021

SL-DRT-21-0031

Cyber security : hardware and sofware (.pdf)

Industrial systems are often used to monitor and control a physical process such as energy production and distribution, water cleaning or transport systems. They are often simply called Supervisory Control And Data Acquisition (SCADA) systems. Due to their interaction with the real world, the safety of these systems is critical and any incident can potentially harm humans and the environment. Since the Stuxnet worm in 2010, such systems increasingly face cyberattacks caused by various intruders, including terrorists or enemy governments [1]. As the frequency of such attacks is increasing, the security of SCADA systems becomes a priority for governmental agencies [2]. One of the main research axis in cybersecurity of industrial systems deals with combination of safety and security properties. Safety relates to applicative properties of the system (e.g. chemical properties for a chemical factory); while security properties take into account how an intruder can harm the system. As show in [3], combining safety and security is a challenging topic as these properties can be either dependent, strengthening, antagonist or independent. As show in [4], combining both safety and security in a common modeling is challenging as both come with sources of combinatorial explosion. Moreover, there are tools used either for security or safety analyzes but currently no tool is able to handle both aspects at the same time. In this context, we propose a Ph.D thesis revolving around modeling of industrial systems taking into account both safety properties of the physical process and security properties. Besides the definition of an accurate, yet automatically analyzable modeling framework/language, many aspects can be part of the subject. For instance, programmable automata (PLC) configuration files could be generated from this model in order to only deploy programs validated beforehand. PLC vulnerabilities could be studied (firmware reverse engineering, protocol fuzzing) in order to test the technical feasibility of found attacks. Finally, in a certification context, security analyzes on the model could include requirements from standards such as IEC 62443 [5] to help evaluation process. Références [1] J. Weiss, Protecting industrial control systems from electronic, Momentum Press, 2010. [2] ANSSI, Managing cybersecurity for ICS, ANSSI, 2012. [3] L. Piètre-Cambacédès, Des relations entre sûreté et sécurité, Paris: Télécom ParisTech, 2010. [4] M. P. a. A. K. M. Puys, Generation of applicative attacks scenarios against industrial systems, Nancy: FPS'17, 2017. [5] IEC-62443, Industrial communication networks - Network and, International Electrotechnical Commission, 2010.

Download the offer (.zip)

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)

Improving Side-channel based instruction disassembling

Département Systèmes (LETI)

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

01-09-2021

SL-DRT-21-0375

thomas.hiscock@cea.fr

Cyber security : hardware and sofware (.pdf)

Side-channel based disassembling is a family of side-channel attacks that strive to recover instructions executed by a processor from some of its physical emanations. Power consumption or electro-magnetic (EM) field are the most widely exploited sources of leakage. From a security designer perspective, knowing the best possible attacks is mandatory to secure a product. Le LSOSP laboratory is very active of this topic. In 2019 it proposed a new approach for performing side-channel based disassembling called mono-bit reconstruction, which was proved to be very effective on small microcontrolers. The main goal of this PhD is to study whether (or not) such attacks are possible on complex cores, such as processors found on smartphones. We will study how the complex microarchitecture of recent processors affect the leakages (Power or EM)? And how can we still extract some information from it? The latter will require to develop machine Learning Tools to recover information from very noisy measurements. At the end of the PhD, we hope to have a better understanding of the side-channel disassembling and some reflexion on countermeasures that would mitigate them.

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)

Hardware vulnerability exploitation for FORENSIC's use-cases on mobile devices.

Département Systèmes (LETI)

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

01-09-2021

SL-DRT-21-0742

driss.aboulkassimi@cea.fr

Cyber security : hardware and sofware (.pdf)

The smartphones as convergent single device have diverse functions and features such as calling, Internet surfing, game playing, banking, storage of personal and professional data. Therefore, it is seems to be a favorite target for data attacker. These targets often include security applications such as software or hardware implementations of encryption functions, or security mechanism such as secure boot, TEE (Trusted Execution Environment), etc. The security features of these recent devices present a real challenge for LEA (Law Enforcement Agencies) within Forensic context. However, state of the art of hardware vulnerability exploitation have shown a potential again this type of security mechanism. There are two main categories of physical attacks: the observation of side channel such as correlation power analysis, and perturbation based especially on fault injection. For example, in [1] authors show that by using Electro-Magnetic Analysis some secret related to TEE can be retrieved. In [2], authors show how faults injection method based on Electromagnetic pulse, allow elevation of privilege achieved by authenticating with a wrong password. Within this framework, this thesis will study the opportunity that offer physical vulnerability to bypass the security functions or to extract secrets from Smartphones. First, the PhD student will explore new methods to resolve synchronization problem, especially, when it is required to synchronize attack bench and target execution time, in order to increase the success rate of attacks. The next topic that will be addressed by the PhD Student consist in applying a relevant scenarios for forensic applications, by developing an automatic tools, for example to define the OS instruction to be exploited by fault injection, or to ensure that the obtained results are the same when we change the target or switching set-up On/Off vice versa. In fact, this thesis is part of the H2020 EXFILES project. EXFILES consortium including academics, industry partners and law enforcement agencies from 7 European countries. The work to be achieved within the framework of this thesis, will allow completing the existing Forensic analysis tools.

Download the offer (.zip)

Multi-level specification and verification of cybersecurity properties for critical C programs

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

Laboratoire pour la Sûreté du Logiciel

01-09-2021

SL-DRT-21-0866

virgile.prevosto@cea.fr

Cyber security : hardware and sofware (.pdf)

This topic deals with formal specification and verification of software properties, in particular cybersecurity properties. Deductive verification tools allow their users to mathematically prove that a given software implementation is correct with respect to a set of formally specified properties. This is notably the case with the WP plug-in of the Frama-C framework for C programs and ACSL specifications. Another plug-in, MetAcsl, was recently developed in order to ease expressing and verifying High-level properties, with a focus on cybersecurity-related properties (e.g. memory isolation, confidentiality, or integrity). Notably, MetAcsl allows users to pose constraints on all read or write accesses in the program. In practice, verifying such high level properties on complex industrial software is often hindered by a low success rate of the automated theorem provers over the proof obligations generated by deductive verification tools. This is due to two main reasons. First, such software tends to use low-level operations (e.g. bitwise operators or pointer casts), which are difficult to represent in the logic world, hence rendering the proof much more complex. Second, the sheer quantity and complexity of mostly independent properties, notably invariants of complex data structures, can prevent the automated provers from succeeding. However, it is often the case that each function only has an impact on a tiny part of the properties, leaving most of them untouched. As all the properties must a priori be considered in the proof context, the latter is thus needlessly cluttered. Moreover, in a certain number of cases, proving the preservation of the impacted property could be done much more easily at a more abstract level. In addition, higher-level properties are usually also more easily understandable, thereby easing the task of the validation team. Similarly, an abstract executable model can be animated and evaluated more easily than the real code. The aim of this PhD is to propose a multi-level specification and verification framework for C programs. This will include verifying a part of the properties on an abstract version of the software under analysis. The abstract version will take the form of a simpler C code (abstracting away parts of the concrete system), encoding for instance a transition system, while staying sufficiently representative to let users state their properties of interest. As is the case in existing refinement-based techniques (in particular the B method), the links between the abstract system and the real code will need to be rigorously established in order to ensure the correctness of the whole development. Hence the verification of the real code will be made easier, since it will be sufficient to show that it respects the refinement properties to be able to deduce that the high-level properties stated on the abstract system also hold for the real code. Specification and verification of the refinement properties can take advantage of the work done in the MetAcsl plug-in. For instance, MetAcsl already offers some functionalities for proving more easily that if a function does not modify the footprint of a property (i.e. the locations that are read by the property), then the property is preserved by the function. The first part of the PhD will be dedicated to the definition of a methodology for specifying an abstract representation of a concrete software implementation. In particular, a way to define the links between data structures and function of both systems, as well as their properties, will be defined. In addition, refinement properties assuring that if a property is proved on the abstract system, then its concrete counterpart holds as well will be formally stated, too. The proposed technique must be able to be deployed on complex industrial software (using optimized data structures, with low-level operations and many invariants that need to be preserved), in order to verify cyber-security properties. To ensure that, a bottom-up approach can be followed, starting from an existing concrete implementation and actual properties that need to be proved on this implementation. For instance one might want to prove on an abstract level that a resource handling mechanism (memory allocator, task manager in a micro kernel, ...) respects a given access policy. Again, MetAcsl could be used for proving the refinement properties towards the real code. A second step in the PhD will be dedicated to develop a tool for automating the abstractions and refinements. Again, the tool will be evaluated on concrete case studies, either open-source or done in the context of industrial projects.

Download the offer (.zip)

See all positions