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