[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
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: [email protected]
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 [email protected] 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.
