Télécom ParisTech is an international and multidisciplinary research centre for digital technology which combines disciplinary expertise at the highest level and a unique capacity for a cross-disciplinary and interdisciplinary approach across all the sectoral areas in direct response to the socio-economic issues of the digital revolution.
Research at Télécom ParisTech relies on 172 faculty members, 14 engineers and technicians on permanent contracts, and 285 PhD students, producing on average each year 625 international publications (journals and conferences) and 20 patents. The school is located at the heart of the 13th district of Paris, France.

The Laboratoire Spécification et Vérification (LSV) is part of the École Normale Supérieur (ENS) in Cachan, in the Paris region. Research at LSV focuses on the verification of computerized systems, of databases and of security protocols. LSV develops the mathematical and algorithmic foundations to the development of tools for automatically proving correctness and detecting flaws.

The offered postdoc position will be located at the department for communication and electronics at Télécom ParisTech.


Assuring the security of electronic systems is a problem that involves several levels of abstraction, ranging from the mathematical properties of cryptographic primitives over the system architecture down to the low-level circuit implementation. Even with strong mathematical security guarantees on the algorithmic levels, secret keys can be extracted using side-channel or fault attacks, exploiting information leaks via power consumption or electromagnetic emanations.

Run-time verification is a technique where so-called hardware checkers are synthesized along with the design in order to monitor important (temporal) properties during the execution. It is also a promising technique for ensuring certain security properties. However, care must be taken when selecting the temporal properties to be implanted into the system. When it comes to fault attacks or hardware Trojan horses, many assumptions on the workings of the design under verification are no longer true.

In this project, we are interested in formal guarantees in the context of run-time monitoring security properties of an integrated circuit. This involves a thorough formalization of the expected attacks as well as new or modified coverage notions in order to estimate the attacks that will be detected.

The candidate will be in charge to revisit the state of the art in the described research field. She or he will help the team during all research activities related to this project, including theoretical foundations, implementation and redaction of conference papers or journal articles.
Candidates profile:
Applicants need to hold a PhD degree in computer science, electrical engineering or a related field, preferably with a focus on formal methods and/or hardware security. Good programming practice will be appreciated. Applicants should master written and spoken English.

Salary range: ≥ 45,000 and < 55,000€ annual gross
Employer:Télécom ParisTech / LSV ENS de Cachan
Workplace: Paris – FRANCE
Skill area: IT, Electronics – Mathematics
Application deadline: 5/15/2017


Applications must contain the following documents: – Curriculum vitae including a list of publications – Summary of PhD – Copy of PhD certificate (or future date of PhD defense) – Names and addresses of two reference persons Please compile the above documents into a single PDF file and send them to Ulrich Kühne ( )with subject “[PROCRAST] application” before May 15th. Feel free to contact us if you need further information.

News Reporter
Dr. Lu