[TYPES/announce] [Postdoc grants] Three fully-funded postdoc positions in software security, program analysis & formal methods @ Université Paris-Saclay, CEA List, France
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] The BINary-level SECurity research group (BINSEC) @ CEA offers 3 fully-funded postdoc positions within the BINSEC team ( https://binsec.github.io ), at the crossroad of binary-level software security, program analysis and formal methods. We are looking for motivated applicants interested in pursuing a postdoc in one of the following topics: POSTDOC-hardening) Hardening software and guaranteeing code security POSTDOC-exploitability) Symbolic execution techniques for exploitability assessment POSTDOC-static) Static analysis techniques for software security To apply for one or several topic(s), candidates should send the topic code(s), a CV, a full list of publications, a cover letter, a transcript of all master-level university results and of all Ph.D. evaluation reports, as well as contact information of three referees to binsec-j...@saxifrage.saclay.cea.fr as soon as possible (first come, first served) and by early July at the latest. Each position is expected to start between October and December 2021 and will have a duration of 2 or 3 years. Detailed topics are available on demand. == 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 (recently: S 2020, NDSS 2021, CCS 2021, ICSE 2021, CAV 2021). 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.
[TYPES/announce] [PhD grants] Two fully-funded PhD positions in software security, program analysis & formal methods @ Université Paris-Saclay, CEA List, France
[ 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: sebastien.bar...@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 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.leme...@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-j...@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
[TYPES/announce] Two positions (one PhD and one Postdoc) in quantum formal verification @ Université Paris-Saclay, CEA List, France
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] The emerging quantum software group @ CEA List, Université Paris-Saclay, offers 2 fully-funded positions at the crossroad of quantum programming, program analysis and formal methods. === OUR GROUP We are an emerging group in formal verification and static analysis of quantum programs, integrated in the Software Safety Laboratory of CEA List, Université Paris-Saclay. Our long term goal is to design and develop formal techniques and tools enabling productive and certified quantum programming. Especially, we develop Qbricks [1], a proof of concept environment for formally verified quantum programming language. See our website at https://qbricks.github.io/ for additional information. === Position#1 (3 years PhD) Probing quantum verification in the NISQ era The goal of this doctoral position is to probe formal verification against first generation of quantum application (NISQ era). Possibilities include, among other: extending Qbricks semantic and proof model to the hybrid paradigm, develop and implement a specification and proof system for error propagation and correction in quantum computing, develop certified ready-to-use NISQ applications. Keywords: quantum programming, formal verification, NISQ, quantum error correction === Position#2 (2 years PostDoc) The goal of this post-doctoral position is to extend formal verification practice to quantum compilation. Possibilities include, among others, error correction mechanisms in certified quantum code, together with specifications and reasoning technique for certifying its reliability, automatized certified optimizer for quantum circuits, hardware agnostic assembly language together with its compiler, Keywords: quantum programming, compilation, optimization, formal verification === HOW TO APPLY Applications should be sent to sebastien.bar...@cea.fr as soon as possible (first come, first served) and by early July 2021 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 references. Each position is expected to start in October 2021. Advisors: Sébastien Bardin (CEA), Christophe Chareton (CEA) Contact: sebastien.bar...@cea.fr [1] C. Chareton, S. Bardin, F. Bobot, V. Perrelle, and B. Valiron. An Automated Deductive Verification Framework for Circuit-building Quantum Programs. ESOP 2021.
[TYPES/announce] Postdoc position at CMU: Verified DSLs for high assurance systems
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] We are looking for a motivated postdoctoral scholar to work on formal methods for the development of high-assurance software and cyber-physical systems. In particular, the project involves the development and enhancement of systems through the composition and verification of programs written in high-level domain-specific languages (DSLs). Potential research problems include: (1) design and implementation of DSLs for high-assurance autonomous systems, (2) compositional verification techniques for the DSLs, and (3) techniques for debugging and repair of DSL programs. You will also be expected to mentor PhD students involved in this project and contribute to the development of a scalable, practical DSL development environment. ** Location ** You will be a member of the Institute for Software Research, School of Computer Science at Carnegie Mellon University in the USA. Pending the evolving situation with COVID-19, you will be expected to work from Pittsburgh, PA. ** Qualifications ** Candidates are expected to have a PhD in Computer Science or related fields, with a strong background and research record in formal methods, software engineering, and/or programming languages. Familiarity with automated verification technologies (e.g., model checkers, SMT solvers) is desirable. ** Timeline ** The position is expected to begin in September 2021 for 1 year, with a possibility of extension. ** Instructions ** To apply, please send a copy of your latest CV and research statement to Eunsuk Kang (esk...@cmu.edu).
