Doctoral student in Computer Science – Verified Microarchitectural Security Full-time

Doctoral Student In Computer Science – Verified Microarchitectural Security

The School of Electrical Engineering and Computer Science at KTH Royal Institute of Technology is seeking a highly motivated PhD student in Computer Science with a focus on formal verification, hardware/software security, and microarchitectural side-channel analysis.

The PhD student will work within the research project µVerif: Rigorous Security Analysis of Computer Microarchitecture, jointly supervised by Associate Professor Roberto Guanciale and Assistant Professor Hamed Nemati. The student will be part of both research groups and embedded in a strong research environment in system security, formal methods, and low-level software and hardware verification.

The project focuses on securing modern processor microarchitectures. Aggressive optimizations such as speculative and out-of-order execution, which significantly improve performance, introduce serious security vulnerabilities (e.g., Spectre-like attacks). These vulnerabilities break the traditional assumption that security properties verified at the software level hold on real hardware.

This project aims to bridge the gap between formal program analysis and security on real hardware by: Developing formal models of speculation and microarchitectural information flow; Automatically extracting security-relevant models from RTL; Evaluating the techniques on open-source RISC-V processor cores. The long-term goal is to enable scalable, rigorous, and hardware-relevant verification of security properties for real-world systems.

The PhD student is expected to:

• Conduct research in formal methods and computer security.
• Develop formal models of microarchitectural behavior and speculation.
• Design and implement analysis and model-extraction tools based on SMT solving and symbolic reasoning.
• Apply the developed techniques to open-source processor designs (e.g., RISC-V).

Supervision: Main supervisor Roberto Guanciale, Co-supervisor Hamed Nemati

To be admitted to postgraduate education, the applicant must have basic eligibility in accordance with either of the following:

• passed a second cycle degree (for example a master's degree), or
• completed course requirements of at least 240 higher education credits, of which at least 60 second-cycle higher education credits, or
• acquired, in some other way within or outside the country, substantially equivalent knowledge

In addition to the above, there is also a mandatory requirement for English equivalent to English B/6.

In order to succeed as a doctoral student at KTH you need to be goal oriented and persevering in your work. During the selection process, candidates will be assessed upon their ability to:

• independently pursue his or her work
• collaborate with others,
• have a professional approach and
• analyze and work with complex issues.
• Strong background in the following areas: Formal methods, Program analysis, Computer architecture, Computer security
• Programming skills (e.g., Python, OCaml, C/C++, or similar).
• Experience in one or more of the following areas:
• SMT solvers and theorem provers.
• Hardware description languages.
• Symbolic execution or model checking.
• Low-level systems programming.
• Microarchitectural side channels and speculative execution.
• interest in combining theory with practical system-level work.

After the qualification requirements, great emphasis will be placed on personal skills.

Target degree: Doctoral degree