Jobs
All our offers
-
PostDoc
Application of formal methods for interferences management
Within a multidisciplinary technological research team of experts in SW/HW co-design tools by applying formal methods, you will be involved in a national research project aiming at developing an environment to identify, analyze and reduce the interferences generated by the concurrent execution of applications on a heterogeneous commercial-off-the-shelf (COTS) multi-core hardware platform.
-
PostDoc
Design and Implementation of a Neural Network for Thermo-Mechanical Simulation in Additive Manufacturing
The WAAM (Wire Arc Additive Manufacturing) process is a metal additive manufacturing method that allows for the production of large parts with a high deposition rate. However, this process results in highly stressed and deformed parts, making it complex to predict their geometric and mechanical characteristics. Thermomechanical modeling is crucial for predicting these deformations, but...
-
PostDoc
High-performance computing using CMOS technology at cryogenic temperature
Advances in materials, transistor architectures, and lithography technologies have enabled exponential growth in the performance and energy efficiency of integrated circuits. New research directions, including operation at cryogenic temperatures, could lead to further progress. Cryogenic electronics, essential for manipulating qubits at very low temperatures, is rapidly developing. Processors operating at 4.2 K using 1.4 zJ...
-
Fixed term contract
Ingénieur-Chercheur en méthodes formelles et IA pour la cybersécurité logicielle bas niveau F/H
« Rejoignez le CEA pour donner du sens à votre activité, mener et soutenir des projets de R&D nationaux et internationaux, cultiver et faire vivre votre esprit de curiosité. » EN SYNTHESE, QU’EST-CE QUE NOUS VOUS PROPOSONS ? Le Commissariat à l'Énergie Atomique et aux Énergies Alternatives (CEA) recherche un(e) Ingénieur-Chercheur en méthodes formelles et...
-
phD
Physical-attack-assisted cryptanalysis for error-correcting code-based schemes
The security assessment of post-quantum cryptography, from the perspective of physical attacks, has been extensively studied in the literature, particularly with regard to the ML-KEM and ML-DSA standards, which are based on Euclidean lattices. Furthermore, in March 2025, the HQC scheme, based on error-correcting codes, was standardized as an alternative key encapsulation mechanism to ML-KEM....
-
phD
Electron beam probing of integrated circuits
The security of numerical systems relies on cryptographic chains of trust starting from the hardware up to end-user applications. The root of chain of trust is called a “root of trust” and takes the form a dedicated Integrated Circuit (IC), which stores and manipulates secrets. Thanks to countermeasures, those secrets are kept safe from extraction...
-
phD
Implementation of TFHE on RISC-V based embedded systems
Fully Homomorphic Encryption (FHE) is a technology that allows computations to be performed directly on encrypted data, meaning that we can process information without ever knowing its actual content. For example, it could enable online searches where the server never sees what you are looking for, or AI inference tasks on private data that remain...
-
Internship
Backdoor Attack Scalability and Defense Evaluation in Large Language Models H/F
Context: Large Language Models (LLMs) deployed in safety-critical domains face significant threats from backdoor attacks. Recent empirical evidence contradicts previous assumptions about attack scalability: poisoning attacks remain effective regardless of model or dataset size, requiring as few as 250 poisoned documents to compromise models from up to 13B parameters. This suggests data poisoning becomes easier,...
-
Internship
Internship - Secret quorums protecting byzantine reliable broadcast against adaptive adversaries H/F
Context: Modern distributed systems, such as blockchain consensus and secure multiparty computation protocols, relies on a fundamental primitive: byzantine reliable broadcast. It allows a set of processes to agree on a message broadcasted by a dedicated process, even when some of them are malicious (byzantine). It relies on quorum systems to prevent correct processes from delivering two...
-
phD
AI Enhanced MBSE framework for joint safety and security analysis of critical systems
Critical systems must simultaneously meet the requirements of both Safety (preventing unintentional failures that could lead to damage) and Security (protecting against malicious attacks). Traditionally, these two areas are treated separately, whereas they are interdependent: An attack (Security) can trigger a failure (Safety), and a functional flaw can be exploited as an attack vector. MBSE...
-
Internship
Stage en cryptologie H/F
Transciphering is a cryptographic technique that re-encrypts data from one scheme to another without an intermediate decryption step. This process drastically reduces the overhead induced by the size of homomorphic ciphertexts during their transmission and storage. The core idea of transciphering is to convert data encrypted with a classical symmetric encryption scheme into a Homomorphic...
-
phD
Side-Channel based Reverse-Engineering
The characterization of the security of embedded systems in quot;black boxquot; or quot;gray boxquot; against Side-Channel attacks often requires a preparatory phase of Reverse-Engineering, which can be particularly time-consuming, especially on a complex System-on-Chip that can be found in smartphones or in the automotive industry. This phase can, for example, consist of detecting a cryptographic...
-
phD
Learning Mechanisms for Detecting Abnormal Behaviors in Embedded Systems
Embedded systems are increasingly used in critical infrastructures (e.g., energy production networks) and are therefore prime targets for malicious actors. The use of intrusion detection systems (IDS) that dynamically analyze the systemapos;s state is becoming necessary to detect an attack before its impacts become harmful. The IDS that interest us are based on machine learning...
-
PostDoc
Design and implementation of an alternative to representation predicates in Frama-C
Frama-C is a collaborative platform for analysis of C programs. Among the different tools available in Frama-C, WP is dedicated to deductive verification of programs, allowing mathematical proof of functional properties and absence of runtime errors. This tool is used for years in industry. Separation logic is the most promising way to allow verification of...
-
Permanent contract
Ingénieur-Chercheur Evaluateur Conformité & Vérification Formelle H/F
Le laboratoire CESTI est missionné par l’ANSSI (Agence Nationale de la Sécurité des Systèmes d'Information) pour l'évaluation sécuritaire de produits électroniques. Composé actuellement d’environ 30 personnes, évaluateurs en sécurité des TIC de très haut niveau technique, il met en œuvre des bancs de test et techniques d’évaluation à l'état de l'art. Le CESTI Leti a...