Post-doc Position
1 Project title
PROCRAST: PROvable Complete Runtime-checking for hArdware Security and Trustability
2 Duration
- 12 months
- Starting in September 2017 (or earlier)
3 Institutions
- LTCI / Télécom ParisTech
- LSV / ENS de Cachan
The postdoc will be located at the department COMELEC of Télécom ParisTech, in the 13th district of Paris, France
The project is supported by Labex DigiCosme operated by ANR as part of the program Investissement d'Avenir Idex Paris-Saclay.
4 Principal investigators
5 Project description
5.1 Keywords
Hardware security, hardware trojan horses, side-channel analysis, fault attacks, run-time verification, formal methods, temporal logic, coverage
5.2 Summary
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.
6 Prerequisites
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.
7 Submission
Applications must contain the following documents:
- Curriculum vitae including a list of publications
- Summary of PhD (and/or of your recent research activity)
- 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". Optionally, you may attach up to two of your research papers, if you consider them helpful for the selection process.
There is no deadline for this call. Incoming applications will be examined on the fly. If we find that you are not eligible for this position -- because of missing documents, or if your profile is apparently out of scope -- you will be informed timely.
