Combining over and underapproximation of memory abstractions for low-level code analysis
Rice's theorem stating that no method can automatically tell whether a property of a program is true or not has led to the separation of verification tools into two groups: sound tools operating by over-approximation, such as abstract interpretation, are able to automatically prove that certain properties are true, but are sometimes unable to conclude and produce alarms; conversely, complete tools operating by under-approximation, such as symbolic execution, are able to produce counter-examples, but are unable to demonstrate whether a property is true.
*The general aim of the thesis is to study the combination of sound and complete methods of programanalysis, and in particular static analysis by abstract interpretation and the generation of underapproximated formulae by symbolic execution*.
We are particularly interested in the combination of over- and sub-approximating abstractions, especially for memory. The priority applications envisaged concern the analysis of code at the binary level, as achieved by the combination of the BINSEC and CODEX analysis platforms, so as to automatically discover new security vulnerabilities, or prove their absence.
Study and evaluation of silicon technology capacities for applications in infrared bolometry
Microbolometers currently represent the dominant technology for the realization of uncooled infrared thermal detectors. These detectors are commonly used in the fields of thermography and surveillance. However, the microbolometer market is expected to grow explosively in the coming years, particularly with their integration into automobiles and the proliferation of connected devices. The CEA Leti LI2T, a recognized player in the field of infrared thermal detectors, has been transferring successive microbolometer technologies to the industrial partner Lynred for over 20 years. To remain competitive in this growing market for microbolometers, the laboratory is working on breakthrough microbolometers incorporating CMOS components as the sensitive element. In this context, the laboratory has initiated studies focusing on temperature-dependent silicon technology capabilities, with promising initial results not reported in the literature. The thesis topic fits into this context and aims to demonstrate the interest of these components for microbolometric applications. It will therefore cover the analytical modeling of these components and their associated physical effects, as well as the reading of such a component in a microbolometer imager approach. A reflection on technological integration will also be conducted. The student will benefit from several already realized technological lots to experimentally characterize the physical effects and familiarize themselves with the subject. To understand the encountered phenomena, the student will have access to the laboratory's entire test set-ups (semiconductor parameter tester, noise analyzer, optical bench, etc.) as well as the numerical analysis Tools (Matlab/Python, TCAD simulations, SPICE simulations, Comsol, etc.). By the end of the thesis, the student will be able to address the question of the interest of these components for microbolometric applications.
Characterization of motor recovery in stroke patients during a BCI-guided rehabilitation
Brain-computer interfaces (BCIs) make it possible to restore lost functions by allowing individuals to control external devices through the modulation of their brain activity. The CEA has developed a BCI technology based on the WIMAGINE implant, which records brain activity using electrocorticography (ECoG), along with algorithms for decoding motor intentions. This technology was initially tested for controlling robotic effectors such as exoskeletons and spinal cord stimulation devices to compensate for severe motor impairments. While this initial paradigm of substitution and compensation is promising, a different application potential is now emerging: functional recovery through BCI-guided rehabilitation. Current literature suggests that BCIs, when used intensively and in a targeted manner, can promote neural plasticity and, in turn, improve residual motor abilities. In particular, ECoG-based implanted BCIs could offer significant therapeutic outcomes. The objective of this thesis is therefore to assess the potential of CEA's BCI technology to enhance patients' residual motor functions through neural plasticity.
This work will be approached through a rigorous and multidisciplinary scientific methodology, including a comprehensive review of the scientific literature, the setup and execution of experimentations with patients, the algorithmic development of tools for monitoring and analyzing patient progress, and the publication of significant results in high-level scientific journals.
This PhD is intended for a student specializing in biomedical engineering, with expertise in signal processing and the analysis of complex physiological data, as well as experience in Python or Matlab. A strong interest in clinical experimentation and neuroscience will also be required. The student will work within a multidisciplinary team at CLINATEC, contributing to cutting-edge research in the field of BCIs.
Development of algorithms and modeling tools of Low-Energy Critical Dimension Small Angle X-ray Scattering
This PhD will take place at the CEA–LETI, a major European actor in the semiconductor industry, and more precisely, at the Nanocharacterization platform of the CEA–LETI witch offer world-class analytical techniques and state-of-the-art instruments. Our team aims to accompany the industry in the development of new characterization tools and so to meet the metrological needs of future technological nodes. Over the past few years, pioneer developments on a new metrology technique based on hard x-ray scattering called CD-SAXS were done at the PFNC. This technique is used to reconstruct the in-plane and out-of-plane structure of nanostructured thin-films with a sub-nm resolution. In this project, we are looking to extend the CD-SAXS approach leveraging the recent breakthrough in the development of low-energy x-ray sources (A. Lhuillier et al. 1988, Nobel prize 2023) called High Harmonics Generation (HHG) sources. Therefore, you will participate in the development of a new and promising characterization methods called Low-energy critical dimension small angle x-ray scattering. The very first proof of concept of this new measurement was conducted in November 2023.
Mission:
In order to include in the data reduction the measurement specificities of this new approach (multi-wavelength, low energy, …) your mission will focus on several aspects to explore in parallel:
- Develop new modeling tools to analyze the data:
o Finite element simulations with Maxwell solver
o Analytical Fourier Transform (similar to standard CD-SAXS) vs dynamical theory
o Comparison between the two approaches
- Build new models dedicated to lithography problematic (CD, overlay, roughness)
- Define the limitations of the technique through the simulation (in term of resolution (nm), uncertainty)
This work will support the development of CD-SAXS measurements with a laboratory HHG (High Harmonic Generation) source lead by a Postdoctoral fellow.
Accelerating thermo-mechanical simulations using Neural Networks --- Applications to additive manufacturing and metal forming
In multiple industries, such as metal forming and additive manufacturing, the discrepancy between the desired shape and the shape really obtained is significant, which hinders the development of these manufacturing techniques. This is largely due to the complexity of the thermal and mechanical processes involved, resulting in a high computational simulation time.
The aim of this PhD is to significantly reduce this gap by accelerating thermo-mechanical finite element simulations, particularly through the design of a tailored neural network architecture, leveraging theoretical physical knowledge.
To achieve this, the thesis will benefit from a favorable ecosystem at both the LMS of École Polytechnique and CEA List: internally developed PlastiNN architecture (patent pending), existing mechanical databases, FactoryIA supercomputer, DGX systems, and 3D printing machines. The first step will be to extent the databases already generated from finite element simulations to the thermo-mechanical framework, then adapt the internally developed PlastiNN architecture to these simulations, and finally implement them.
The ultimate goal of the PhD is to demonstrate the acceleration of finite element simulations on real cases: firstly, through the implementation of feedback during metal printing via temperature field measurement to reduce the gap between the desired and manufactured geometry, and secondly, through the development of a forging control tool that achieves the desired geometry from an initial geometry. Both applications will rely on an optimization procedure made feasible by the acceleration of thermo-mechanical simulations.
Physics of perovskite materials for medical radiography: experimental study of photoconduction gain
X-rays is the most widely used medical imaging modality. It is used to establish diagnostics, monitor the evolution of pathologies, and guide surgical procedures.
The objective of this thesis is to study a perovskite type semiconductor material for its use as a direct X-ray sensor. Perovskite-based matrix imagers demonstrate improved spatial resolution and increased signal, and can thus help improve patient treatment. Prototype X-ray imagers manufactured at the CEA already provide radiographic images but their performances are limited by the instability of the sensor material.
You job will be to study the mechanisms responsible for the photoconduction gain and photocurrent drift of thick perovskite layers from both a theoretical and an experimental standpoint. To this end, you will adapt the electro-optical characterization benches of the laboratory, conduct experiments and analyze the data collected. You will also have the opportunity to perform advanced characterizations with specialized laboratories within the framework of national and international collaborations. The results of this thesis will provide a better understanding of the material properties and guide its ellaboration to produce high-performance X-ray imagers.
Thermomechanical study of heterostructures according to bonding conditions
For many industrial applications, the assembly of several structures is one of the key stages in the manufacturing process. However, these steps are generally difficult to carry out, as they lead to significant increases in warpage. Controlling stresses and strains generated by heterostructures is however imperative. We proposes to address this subject using both experimental exploration and simulation through thermomechanical studies in order to predict and anticipate problems due to high deformations.
Optimisation of advanced mask design for sub-micrometer 3D lithography
With the advancement of opto-electronic technology, 3D patterns with sub micrometer dimensions are more and more integrated in the device, especially on imaging and AR/VR systems. To fabricate such 3D structures using standard lithography technique requires numerous process steps: multiple lithography and pattern transfer, which is time and resource consuming.
With optical grayscale lithography, such 3D structures can be fabricated in single lithography step, therefore reducing significantly the number of process steps required in standard lithography. For high volume manufacturing of such 3D patterns, optical grayscale lithography with Deep-UV (DUV), 248nm and 193nm are the most relevant, as it is compatible with industrial production line. This technique of 3D lithography is however more complex than it seems, which requires advance lithography model and data-preparation flow to design optical mask corresponding to the desired 3D pattern.
Design and fabrication of neuromorphic circuit based on lithium-iontronics devices
Neural Networks (NNs) are inspired by the brain’s computational and communication processes to efficiently address tasks such as data analytics, real time adaptive signal processing, and biological system modelling. However, hardware limitations are currently the primary obstacle to widespread adoption. To address this, a new type of circuit architecture called "neuromorphic circuit" is emerging. These circuits mimic neuron behaviour by incorporating high parallelism, adaptable connectivity, and in memory computation. Ion gated transistors have been extensively studied for their potential to function as artificial neurons and synapses. Even if these emerging devices exhibit excellent properties due to their ultra low power consumption and analog switching capabilities, they still need to be validated into larger systems.
At the RF and Energy Components Laboratory of CEA-Leti, we are developing new lithium-gated transistors as building blocks for deploying low-power artificial neural networks. After an initial optimization phase focused on materials and design, we are ready to accelerate the pace of development. These devices now need to be integrated into a real system to assess their actual performance and potential. In particular, both bio-inspired circuits and crossbar architectures for accelerated computation will be targeted.
During this 3-year PhD thesis, your (main) objective will be to design, implement, and test neural networks based on lithium-gated transistor crossbars (5x5, 10x10, 20x20) and neuromorphic circuits , along with the CMOS read and write logic to control them. The networks might be implemented using different algorithms and architectures, including Artificial Neural Network, Spiking Neural Networks and Recurrent Neural Networks, which will be then tested by solving spatial and/or temporal pattern recognition problems and reproduce biological functions such as pavlovian conditioning.
Embedded local blockchain on secure physical devices
The blockchain is based on a consensus protocol, the aim of which is to share and replicate ordered data between peers in a distributed network. The protocol stack, embedded in the network's peer devices, relies on a proof mechanism that certifies the timestamp and ensures a degree of fairness within the network.
The consensus protocols used in the blockchains deployed today are not suitable for embedded systems, as they require too many communication and/or computing resources for the proof. A number of research projects, such as IOTA and HashGraph, deal with this subject and will be analysed in the state of the art.
The aim of this thesis is to build a consensus protocol that is frugal in terms of communications and computing resources, and whose protocol stack will be implemented in a secure embedded device. This protocol must be based on the proof of elapsed time from our laboratory's work, which is also frugal, called Proof-of-Hardware-Time (PoHT), and must satisfy the properties of finality and fairness. The complete architecture of a peer node in the network will be designed and embedded on an electronic board including a microprocessor and several hardware security components, in such a way that the proof resource cannot be parallelized. Communication between peers will be established in a distributed manner.