[TYPES/announce] [PhD grant] "Speculating about low-level security": A 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 is offering 1 fully-funded Ph.D. position at the crossroad of software security, program analysis and formal methods, in order to develop formal analysis techniques for speculation-based attacks. Interested? Do not hesitate to get in touch with us.

keywords: formal methods, security, micro-architectural attacks, program analysis, speculative execution, automated symbolic reasoning


=== Topic: 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.



=== HOW TO APPLY

Detailed topics are available on demand.

Applications should be sent to sebastien.bardin at cea.fr as soon as possible (first come, first served), and by early July at the latest.
Candidates should send 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) 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.

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/20210628/e2094887/attachment-0001.htm>