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

PhD : selection by topics

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

See all positions [+]

Proved simplification engine for software deductive verification

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

Laboratoire pour la Sûreté du Logiciel

01-09-2020

SL-DRT-20-0396

loic.correnson@cea.fr

Cyber security : hardware and sofware (.pdf)

The Frama-C platform developped at CEA is dedicated to formally establish the absence of bugs in critical sofwares. It is used at an industrial scale in various domains, such as avionics and energy production plants. No asses such waranties on critical sofwares, it is necessary to automate the verfication process with proof assistants (Coq, PVS, HOL) and SMT solvers (Z3, CVC4, Alt-Ergo). However, for these techniques to be applicable on industrial codes, it is necessary to first simplify our proof objectives. Inside Frama-C, we have developped the Qed engine which is precisely in charge of building and simplifying logical formula. This engine was typically responsible for dramatic gains in performance for proving critical codes at Airbus, leading to the adoption of the approach in their production process. Since Qed early developments in 2015 the engine has been extended with many improvements with an increasing complexity. It now becomes difficult to certify that the engine remains sound and only produce valid simplifications. To this end, the subject of the thesis is to completely redesign the Qed engine with the Why-3 proof environment by specifying its simplification algorithms and formally verifying their correctness. Eventually, the extracted code from this Why-3 development will replace the existing engine inside Frama-C.

Download the offer (.zip)

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-2020

SL-DRT-20-0594

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)

Vulnerability study of electronic system against electromagnetic perturbation

Département Systèmes (LETI)

Centre d'Evaluation de la Sécurité des Technologies de l'Information

01-09-2020

SL-DRT-20-0830

Cyber security : hardware and sofware (.pdf)

In the field of electronic system evaluation, the Leti ITSEF evaluates the component resistance against perturbation attacks using classical methods (voltage/clock glitch, glitch, photoelectric perturbation). Usual methods allow the evaluator to inject faults on the target with a high level of precision but require a physical access to the product in order to be very close to the area of the perturbation, which is sometimes unrealistic. Indeed, state of the art equipment used by the leti ITSEF for electromagnetic perturbations usually require to put a wire loop at less than 1mm of the component. The Leti ITSEF wants to develop a novel distant perturbation method based on electromagnetic perturbation. On the other hand, the CEA-DAM of Gramat has a serious experience in electromagnetic susceptibility of electronic system against electromagnetic aggressions. They want to use their technology in order to evaluate the vulnerability of a communicating system against an electromagnetic aggression. Objectives The research will be based on previous studies performed by the CEA-DAM of Gramat on the vulnerability of electronic systems against electromagnetic radiations, which is very effective for permanent or temporarily denial of service. First, it will be necessary to make the link between the Gramat technology that is very effective in term of service denial and the Leti technology, which allows a more precise effect. Then, a laboratory demonstrator will be developed to perform perturbation attacks on a representative target. Execution of the Thesis The first part of the thesis will be dedicated to the bibliography review on the effects of electromagnetic perturbations on electronic systems and the study of different ways to produce such electromagnetic perturbations. In the second part, the technical choice from the previous part will be tested against different representative targets of IoT devices. It will be necessary to measure the perturbation impact on different targets and to compare the results regarding a theoretical model. The last part will be dedicated to the prototype development.

Download the offer (.zip)

Systematic construction and interpretation of electromagnetic leakages models for embedded processors

Département Systèmes (LETI)

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

01-10-2020

SL-DRT-20-0838

maxime.lecomte@cea.fr

Cyber security : hardware and sofware (.pdf)

Side-channel attacks consist in measuring the physical activity emitted by a circuit (processor, microcontroller or cryptographic accelerator) to extract secrets. The consumption of the circuit or the electromagnetic emanation are the most commonly exploited signals. Due to the development of the Internet of Things (IoT), more and more systems are exposed to these attacks. Unfortunately, integrating countermeasures (software or hardware) against such attacks is extremely expensive. Therefore, it is essential to have an accurate idea of side-channel leakages as early as possible in the design phases. On the one hand to target countermeasures on critical areas and on the other hand to have a realistic view of leakages in order to automate the application of countermeasures. The thesis topic is the exploration of electromagnetic leakage models and different ways of interpreting them. The general objective of this work is to model the leakages of a processor based on its state at different abstraction level: Register Transfer Level (RTL), micro-architecture or even instruction set simulator (ISS). The LSOSP laboratory of CEA-LETI where the thesis will take place has a strong experience on physical measurements and has already performed preliminary research on the subject. Therefore, the candidate will start from these results and will perform physical measurements and manipulate different logic models to create a precise leakage model of the targeted processor.

Download the offer (.zip)

Towards efficient post-quantum algorithms. Exploring embedded cyber-security

Département Architectures Conception et Logiciels Embarqués (LIST-LETI)

Laboratoire composants logiciels pour la Sûreté et la Sécurité des Systèmes

01-09-2020

SL-DRT-20-0870

malika.izabachene@cea.fr

Cyber security : hardware and sofware (.pdf)

Progress in Cryptanalysis leads to new attacks on cryptographic algorithms and enforce to augment the key sizes of currently used systems. In addition, the threats of quantum attacks lead to relevant attacks optimizations on some popular asymmetric cryptosystems as RSA. These facts leads to consider a new generation of algorithms called post-quantum algorithms which are resistant against quantum attacks. In 2016, the NIST (National Institute of Standards and Technology) makes a call for new post-quantum cryptographic algorithms . We are currently at the second phase of the analysis process of the candidates for standardization. In this PhD thesis, we will address the possibility to implement post-quantum algorithms in constraint environments i.e. the constraints resources such as memory or computation capabilities. This study will lead us to  consider constant-time implementations in order to resist to timing attacks. Our study will be based on NIST submissions but not only; we will also review variants or other algorithms proposed outside the call. Our focus will be to construct dedicated cryptographic building blocks  for target constraints. And one of our goals will be to build secure quantum algorithms in real world models which captures extended timing and physical attacks.

Download the offer (.zip)

Impact of micro-architecture on side-channel attack countermeasures

Département Architectures Conception et Logiciels Embarqués (LIST-LETI)

Laboratoire Infrastructure et Ateliers Logiciels pour Puces

01-09-2020

SL-DRT-20-0921

nicolas.belleville@cea.fr

Cyber security : hardware and sofware (.pdf)

The context of this thesis is the context of cyber-security for embedded systems and IoT. The thesis addresses the application of countermeasures by compilation against side-channel attacks exploiting power consumption or electromagnetic emissions, which represent a major threat against these systems. A leakage model can be used when applying countermeasures: it models how side-channel leakages are related to the program and the data being manipulated by the processor. An unfaithful model does not allow the countermeasure to be applied effectively. The models currently employed are insufficient since they do not take into account the micro-architecture of the components. Indeed, micro-architecture and in particular elements that are invisible at the assembly level (hidden registers or buffers) can cause leakages. The objective of this thesis is to study the impact of micro-architecture on the automated application of countermeasures against auxiliary channel attacks during compilation. A first axis is to study how to modify the way countermeasures are applied within the compiler to take into account precise leakage models that are micro-architecture aware, for example how to adapt the instruction selection or register allocation in the compiler depending on the leakage model. A second axis is to adapt the countermeasures themselves in order to better take into account the nature of the leakages, with the objective of improving the reduction of information leakage and thus improving the security/performance trade-off.

Download the offer (.zip)

Scalable and Precise Static Analysis of Memory for Low-Level Languages

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

Laboratoire pour la Sûreté du Logiciel

01-10-2020

SL-DRT-20-1088

matthieu.lemerre@cea.fr

Cyber security : hardware and sofware (.pdf)

The goal of the thesis is to develop an automated static analysis (based on abstract interpretation) to verify absence of memory errors in compiled, low-level languages (C, C++, Assembly, Rust). This issue is very important for cybersecurity since most of the software-related security issues come from memory safety (buffer overflows, use-after-free, wrong type punning). The three issues when designing such an automated static analysis is to keep the verification effort low, to handle large and complex systems, and to be precise enough so that the analysis does not report a large amount of false alarms. We draw on the success of a new method using abstract domains parameterized by type invariants, which allowed in particular to fully automatically prove memory safety of an existing industrial microkernel from its machine code, using only 58 lines of annotations, and seek to extend this analysis to larger systems. In particular, the analyzer should be extended to improve scalability (using compositional analysis), to improve precision (using separation logic and SMT/formula-based abstract domains), and to further reduce the amount of annotations (using automatic inference of more precise type invariants).

Download the offer (.zip)

Security Assurance Case for Artificial Intelligence Based Systems

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

Labo.conception des systèmes embarqués et autonomes

01-10-2020

SL-DRT-20-1206

morayo.adedjouma@cea.fr

Cyber security : hardware and sofware (.pdf)

The use of Artificial Intelligence (AI)-based systems is growing rapidly and finding uses in many industries. This is especially true for autonomous systems, where deployments are increasingly targeting important and even critical requirements whose failures would cause undesirable or intolerable consequences. The current state-of-the-art is to perform a tedious certification process for demonstrating that the system is secure. Providing a compelling software security argument as a brick to build assurance cases for system security is a fundamental but challenging part of this demonstration. Part of the problem is providing evidence for low-level argument claims where formal verification techniques such as model-checking may be successfully used for their effective evaluation. There are also difficulties in structuring the argument in a readable and reusable fashion. Moreover, since AI-based systems may still may acquire at operation time new abilities not considered during their development to be able to react properly to changing uncertain and unknown environments, one cannot build assurance case uniquely upon artefacts produced during an adequate development process. In our previous work, we investigated cyber security engineering, validation and evaluation in the context of critical infrastructures, cyber-physical and distributed systems. The main goal of this PhD thesis is to continue this trend of work considering the case where some software components of the previous application domains employs Artificial Intelligence (AI), particularly machine learning algorithms and techniques. The thesis will contribute to this matter by describing a methodological tool support to build and reuse security assurance cases in the form of reusable models in the context of AI-based systems system architecture and security interplay. This will involve developing (1) a design framework to formally specify and verify security in the context of AI-based systems, (2) an argumentation structure for reasoning about the security of these systems and (3) approaches to generate sufficient evidence to support the claims in the argument. Subsequently, this thesis offers guidelines for generating explanations and evidence to be communicated to, understood by, and acceptable to regulatory authorities, certification bodies, and the eventual users of the systems.

Download the offer (.zip)

See all positions