PhD Position in Systems-Level Security: KU Leuven’s DistriNet research group is offering a fully funded PhD position in the field of mechanized verification, formal methods, and system security. The research will focus on the development of universal contracts for authoritative semantics of Instruction Set Architectures (ISAs), advancing end-to-end system verification techniques. The position is co-supervised by Dominique Devriese and Steven Keuchel.
PhD Research Position in Mechanized Systems-Level Security at KU Leuven
Designation: PhD Researcher
Research Area:
- Mechanized verification
- Formal methods
- System security
- Functional programming
- Program logics
Location: KU Leuven, DistriNet Research Group, Leuven, Belgium
Eligibility/Qualification:
- Academic Master’s degree (or equivalent) in Computer Science, Mathematics, or a closely related field, obtained before the start date of the position.
- Familiarity with, or strong willingness to learn about:
- Statically-typed functional programming (e.g., Haskell, OCaml)
- Monadic programming and constraint generation
- Compiler implementation and programming language semantics
- Proof assistants such as Agda or Coq
- Program logics like Hoare logic or separation logic
- Strong interest in formal methods and security verification
- Excellent command of written and spoken English
Job Description: The successful candidate will contribute to the Katamaran project, which focuses on developing a deductive separation logic-based verifier for ISAs specified in Sail. The main objectives include:
- Scaling up verification of trusted low-level code interacting with untrusted code using universal contracts.
- Developing intermediate representations suited for (semi-)automated verification.
- Exploring the explicit modeling of join points and propagating verification information.
- Lifting verified ISA-level security guarantees to higher abstraction levels.
- Engaging in research activities, disseminating findings at conferences, and collaborating with the DistriNet team.
How to Apply: Interested candidates should submit the following documents via email to both Dominique Devriese and Steven Keuchel (firstname.lastname@kuleuven.be):
- A concise motivation letter
- Academic curriculum vitae
- Transcript of records of previous degrees
- Academic reference (name, function, and email address)
For further inquiries, applicants may contact the supervisors via email.
Last Date to Apply: March 16, 2025
