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.
Portable GPU-based parallel algorithms for nuclear fuel simulation on exascale supercomputers
In a context where the standards of high performance computing (HPC) keep evolving, the design of supercomputers includes always more frequently a growing number of accelerators or graphics processing units (GPUs) that provide the bulk of the computing power in most supercomputers. Due to their architectural departures from CPUs and still-evolving software environments, GPUs pose profound programming challenges. GPUs use massive fine-grained parallelism, and thus programmers must rewrite their algorithms and code in order to effectively utilize the compute power.
CEA has developed PLEIADES, a computing platform devoted to simulating nuclear fuel behavior, from its manufacture all the way to its exploitation in reactors and its storage. PLEIADES can count on an MPI distributed memory parallelization allowing simulations to run on several hundred cores and it meets the needs of CEA's partners EDF and Framatome. Porting PLEIADES to use the most recent computing infrastructures is nevertheless essential. In particular providing a flexible, portable and high-performance solution for simulations on supercomputers equipped with GPUs is of major interest in order to capture ever more complex physics on simulations involving ever larger computational domains.
Within such a context the present thesis aims at developing and evaluating different strategies for porting computational kernels to GPUs and at using dynamic load balancing methods tailored to current and upcoming GPU-based supercomputers. The candidate will rely on the tools developed at CEA such as the thermo-mechanical solver MFEM-MGIS [1,2] or MANTA [3]. The software solutions and parallel algorithms proposed with this thesis will eventually enable large 3D multi-physics modeling calculations of the behavior of fuel rods on supercomputers comprising thousands of computing cores and GPUs.
The candidate will work at the PLEIADES Fuel Scientific Computing Tools Development Laboratory (LDOP) of the department for fuel studies (DEC - IRESNE, CEA Cadarache). They will be brought to evolve in a multidisciplinary team composed of mathematicians, physicists, mechanicians and computer scientists. Ultimately, the contributions of the thesis aim at enriching the computing platform for nuclear fuel simulations PLEIADES.
References :[1] MFEM-MGIS - https://thelfer.github.io/mfem-mgis/[2]; Th. Helfer, G. Latu. « MFEM-MGIS-MFRONT, a HPC mini-application targeting nonlinear thermo-mechanical simulations of nuclear fuels at mesoscale ». IAEA Technical Meeting on the Development and Application of Open-Source Modelling and Simulation Tools for Nuclear Reactors, June 2022, https://conferences.iaea.org/event/247/contributions/20551/attachments/10969/16119/Abstract_Latu.docx, https://conferences.iaea.org/event/247/contributions/20551/attachments/10969/19938/Latu_G_ONCORE.pdf; [3] O. Jamond et al. «MANTA : un code HPC généraliste pour la simulation de problèmes complexes en mécanique », https://hal.science/hal-03688160
Dynamic Assurance Cases for Autonomous Adaptive Systems
Providing assurances that autonomous systems will operate in a safe and secure manner is a prerequisite for their deployment in mission-critical and safety-critical application domains. Typically, assurances are provided in the form of assurance cases, which are auditable and reasoned arguments that a high-level claim (usually concerning safety or other critical properties) is satisfied given a set of evidence concerning the context, design, and implementation of a system. Assurance case development is traditionally an analytic activity, which is carried out off-line prior to system deployment and its validity relies on assumptions/predictions about system behavior (including its interactions with its environment). However, it has been argued that this is not a viable approach for autonomous systems that learn and adapt in operation. The proposed PhD will address the limitations of existing assurance approaches by proposing a new class of security-informed safety assurance techniques that are continually assessing and evolving the safety reasoning, concurrently with the system, to provide through-life safety assurance. That is, safety assurance will be provided not only during initial development and deployment, but also at runtime based on operational data.
Assisted generation of complex computational kernels in solid mechanics
The behavior laws used in numerical simulations describe the physical characteristics of simulated materials. As our understanding of these materials evolves, the complexity of these laws increases. Integrating these laws is a critical step for the performance and robustness of scientific computations. Therefore, this step can lead to intrusive and complex developments in the code.
Many digital platforms, such as FEniCS, FireDrake, FreeFEM, and Comsol, offer Just-In-Time (JIT) code generation techniques to handle various physics. This JIT approach significantly reduces the time required to implement new simulations, providing great versatility to the user. Additionally, it allows for optimization specific to the cases being treated and facilitates porting to various architectures (CPU or GPU). Finally, this approach hides implementation details; any changes in these details are invisible to the user and absorbed by the code generation layer.
However, these techniques are generally limited to the assembly steps of the linear systems to be solved and do not include the crucial step of integrating behavior laws.
Inspired by the successful experience of the open-source project mgis.fenics [1], this thesis aims to develop a Just-In-Time code generation solution dedicated to the next-generation structural mechanics code Manta [2], developed by CEA. The objective is to enable strong coupling with behavior laws generated by MFront [3], thereby improving the flexibility, performance, and robustness of numerical simulations.
The doctoral student will benefit from guidance from the developers of MFront and Manta (CEA), as well as the developers of the A-Set code (a collaboration between Mines-Paris Tech, Onera, and Safran). This collaboration within a multidisciplinary team will provide a stimulating and enriching environment for the candidate.
Furthermore, the thesis work will be enhanced by the opportunity to participate in conferences and publish articles in peer-reviewed scientific journals, offering national and international visibility to the thesis results.
The PhD will take place at CEA Cadarache, in south-eastern France, in the Nuclear Fuel Studies Department of the IRESNE Institute [4]. The host laboratory is the LMPC, whose role is to contribute to the development of the physical components of the PLEIADES digital platform [5], co-developed by CEA and EDF.
[1] https://thelfer.github.io/mgis/web/mgis_fenics.html
[2] MANTA : un code HPC généraliste pour la simulation de problèmes complexes en mécanique. https://hal.science/hal-03688160
[3] https://thelfer.github.io/tfel/web/index.html
[4] https://www.cea.fr/energies/iresne/Pages/Accueil.aspx
[5] PLEIADES: A numerical framework dedicated to the multiphysics and multiscale nuclear fuel behavior simulation https://www.sciencedirect.com/science/article/pii/S0306454924002408
CCA-secure constructions for FHE
Fully Homomorphic Encryption (FHE) is a corpus of cryptographic techniques that allow to compute directly over encrypted data. Since its inception around 15 years ago, FHE has been the subject of a lot of research towards more efficiency and better practicality. From a security perspective, however, FHE still raises a number of questions and challenges. In particular, all the FHE used in practice, mainly BFV, BGV, CKKS and TFHE, achieve only CPA-security, which is sometimes referred to as security against passive adversaries.
Over the last few years, a number of works have investigated the security of FHE in the beyond-CPA regime with new security notions (CPAD, FuncCPA, vCCA, vCCAD, and others) being proposed and studied, leading to new attacks and constructions and, overall, a better understanding of FHE security in that regime.
With respect to CCA security, recent works (2024) have defined new security notions, which are stronger than CCA1 and shown to be achievable by both exact and approximate FHE schemes. Leveraging on these advances, the present thesis will aim to design practical FHE-style malleable schemes enforcing CCA security properties, at least for specific applications.
Hardware-aware Optimizations for Efficient Generative AI with Mamba Networks
Generative AI has the potential to transform various industries. However, current state-of-the-art models like transformers face significant challenges in computational and memory efficiency, especially when deployed on resource-constrained hardware. This PhD research aims to address these limitations by optimizing Mamba networks for hardware-aware applications. Mamba networks offer a promising alternative by reducing the quadratic complexity of self-attention mechanisms through innovative architectural choices. By leveraging techniques such as sparse attention patterns and efficient parameter sharing, Mamba networks can generate high-quality data with significantly lower resource demands. The research will focus on implementing hardware-aware optimizations to enhance the efficiency of Mamba networks, making them suitable for real-time applications and edge devices. This includes optimizing training and inference times, as well as exploring potential hardware accelerations. The goal is to advance the practical deployment of generative AI in resource-constrained domains, contributing to its broader adoption and impact.
Exploration of unsupervised approaches for modeling the environment from RADAR data
Radar technologies have gained significant interest in recent years, particularly with the emergence of MIMO radars and "Imaging Radars 4D". This new generation of radar offers both opportunities and challenges for the development of perception algorithms. Traditional algorithms such as FFT, CFAR, and DOA are effective for detecting moving targets, but the generated point clouds are still too sparse for precise environment model. This is a critical issue for autonomous vehicles and robotics.
This thesis proposes to explore unsupervised Machine Learning techniques to improve environment model from radar data. The objective is to produce a richer model of the environment to enhance data density and scene description, while controlling computational costs for real-time computing. The thesis will address the question of which types of radar data are best suited as inputs for algorithms and for representing the environment. The candidate will need to explore non-supervised algorithmic solutions and seek computational optimizations to make these solutions compatible with real-time execution.
Ultimately, these solutions must be designed to be embedded as close as possible to the sensor, allowing them to be executed on constrained targets.
CORTEX: Container Orchestration for Real-Time, Embedded/edge, miXed-critical applications
This PhD proposal will develop a container orchestration scheme for real-time applications, deployed on a continuum of heterogeneous computing resources in the embedded-edge-cloud space, with a specific focus on applications that require real-time guarantees.
Applications, from autonomous vehicles, environment monitoring, or industrial automation, applications traditionally require high predictability with real-time guarantees, but they increasingly ask for more runtime flexibility as well as a minimization of their overall environmental footprint.
For these applications, a novel adaptive runtime strategy is required that can optimize dynamically at runtime the deployment of software payloads on hardware nodes, with a mixed-critical objective that combines real-time guarantees with the minimization of the environmental footprint.
Securing Against Side-Channel Attacks by Combining Lightweight Software Countermeasures
Side-channel attacks, such as analyzing a processor's electrical consumption or electromagnetic emissions, allow for the recovery of sensitive information, including cryptographic keys. These attacks are particularly effective and pose a serious threat to the security of embedded systems.
This thesis focuses on combining low-impact software countermeasures to strengthen security against side-channel attacks, an idea that remains poorly explored in the current state of the art. The goal is to identify synergies and incompatibilities between these countermeasures to create more effective and lightweight solutions. In particular, low-entropy masking countermeasures will be considered.
These ideas will be applied on cryptography algorithm, with a particular focus on post-quantum cryptography algorithms.
The thesis aims to develop new ways to secure software, offering better trade-offs between security and performance than existing approaches.