[TYPES/announce] [PhD grants] Two fully-funded PhD positions in software security, program analysis & formal methods @ Université Paris-Saclay, CEA List, France

[BARDIN Sébastien]

The BINary-level SECurity research group (BINSEC) @ CEA offers 2 fully-funded Ph.D. positions at the crossroad of software security, program analysis and formal methods.
We are looking for motivated applicants, interested in pursuing a Ph.D. degree in one of the following topics:


=== Topic#1 Speculating About Low-level Security

Recent micro-architectural attacks take advantage of subtle behaviours at the micro-architectural levels, typically speculative behaviours introduced in modern architectures for efficiency, in order to bypass protections and leak sensitive data [4]. These vulnerabilities are extremely hard to find by a human expert, as they require to reason at a very low-level, on an exponential number of otherwise-hidden speculative behaviours, and on complex security properties (leaks and data interference, rather than standard memory corruptions). The goal of this doctoral work is to understand how automated symbolic verification methods (especially but not limited to, symbolic execution [2]) can be efficiently lifted to the case of speculative micro-architectural attacks, with the ultimate goal of securing essential security primitives in cryptographic libraries and OS kernels.

Keywords: micro-architectural attacks, binary-level analysis, speculative executions, information leaks, symbolic execution

Advisor: Sébastien Bardin (CEA), Tamara Rezk (Inria)

Prior results: preliminary results on side channels and Spectre attacks published in top-tiers security conferences [1,3]

Contact: sebastien.bardin at cea.fr

References

[1] Lesly-Ann Daniel, Sébastien Bardin, Tamara Rezk.  Binsec/Rel: Efficient Relational Symbolic Execution for Constant-Time at Binary-Level. In S&P 2020

[2] Cristian Cadar, Koushik Sen: Symbolic execution for software testing: three decades later. Commun. ACM 56(2):82-90 (2013)

[3] Lesly-Ann Daniel, Sébastien Bardin, Tamara Rezk. Hunting the Haunter: Efficient Relational Symbolic Execution for spectre with Haunted RelSE. In NDSS 2021

[4] Jo Van Bulck, Michael Schwarz et al. A Systematic Evaluation of Transient Execution Attacks and Defenses, in USENIX Security Symposium, 2019.


=== Topic#2 Binary-level static verification of embedded operating systems security

Systems software need systems programming languages, like C, C++, or assembly, that gives programmers low-level control over resource
management at the expense of safety. The goal of the PhD thesis is to design and implement a scalable sound static analysis [5] for systems
software, targeting in particular OS kernels and hypervisors, that can efficiently verify advanced security properties directly from machine
code [6] while requiring only a low amount of annotations.

Keywords: abstract interpretation, advanced type systems, low-level code, operating systems, cybersecurity

Advisor: Matthieu Lemerre (CEA), Mihaela Sighireanu (ENS Paris-Saclay)

Prior results: preliminary results on scalable static analysis and kernel verification published in formal methods and systems conferences [1,2]

Contact: matthieu.lemerre at cea.fr

References

[5] H. Illous, M. Lemerre, and X. Rival. Interprocedural shape analysis using separation logic-based transformer summaries. SAS, 2020.

[6] O. Nicole, M. Lemerre, S. Bardin, and X. Rival. No Crash, No Exploit: Automated Verification of Embedded Kernels RTAS, 2021. (outstanding paper award)


=== HOW TO APPLY

Detailed topics are available on demand.

Applications should be sent to binsec-jobs at saxifrage.saclay.cea.fr as soon as possible (first come, first served) and by the end of June 2021 at the latest.
Candidates should send the topic code(s) they are interested in, a CV, a cover letter, a transcript of all their university results, as well as contact information of two referees. Each Ph.D. position is expected to start in October 2021 and will have a duration of 3 years.


== The BINSEC team @ CEA

The BINary-level SECurity research group (BINSEC) of CEA List is a dynamic team of 4 senior researchers focusing on developing low-level program analysis tailored to security needs. The group has frequent publications in top-tier security, formal methods and software engineering conferences. We work in close collaboration with other French and international research teams, industrial partners and national agencies. The team is part of Université Paris-Saclay, the world’s 14th and European Union’s 1st university, according to Shanghai ARWU Ranking 2020. We have developed a high-level expertise in several binary-level code analysis approaches, namely formal methods, symbolic execution, abstract interpretation and fuzzing. We apply these techniques to low-level software security problems, covering notably vulnerability detection, malware analysis, code hardening and patching, criticality assessment and formal verification.

See https://binsec.github.io/ for additional information.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20210531/32086700/attachment-0001.htm>