Dear colleagues, The School of Electrical Engineering and Computer Science at KTH Royal Institute of Technology (Stockholm, Sweden) is seeking a highly motivated PhD student in Computer Science, with a focus on formal verification, hardware/software security, and microarchitectural side-channel analysis.
Full details about the position, eligibility requirements, and how to apply are available here: https://www.kth.se/lediga-jobb/907809 The position is part of the research project µVerif: Rigorous Security Analysis of Computer Microarchitecture, jointly supervised by Associate Professor Roberto Guanciale (https://www.kth.se/profile/robertog) and Assistant Professor Hamed Nemati (https://hnemati.github.io). The successful candidate will be embedded in a strong and collaborative research environment spanning system security, formal methods, and low-level software and hardware verification, and will be affiliated with both research groups. Modern processor architectures rely on aggressive performance optimisations, such as speculative and out-of-order execution, which, while highly effective for performance, introduce subtle and severe security vulnerabilities (e.g., Spectre-class attacks). These vulnerabilities fundamentally challenge the assumption that software-level security guarantees hold on real hardware. The project focuses on securing modern processor microarchitectures. Aggressive optimisations 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 behaviour 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). We are looking for candidates with a strong background in computer science, and a particular interest in formal methods, security, or computer architecture. We would greatly appreciate it if you could share this announcement with potentially interested candidates. Please feel free to contact me for informal inquiries. Best regards, Roberto Guanciale Associate Professor KTH Royal Institute of Technology Stockholm, Sweden [email protected] _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
