The Division of Network and Systems Engineering at KTH Royal Institute of Technology is offering a postdoctoral research position in the area of formal verification of protocols and secure compilation, funded by the Wallenberg AI, Autonomous Systems and Software Program (WASP). This opportunity is ideal for researchers with a strong background in formal methods for security, particularly those interested in the formal verification of security protocols or secure compilation. The successful candidate will join a dynamic and collaborative research group that includes PhD students, postdocs, and an assistant professor, and is engaged in cutting-edge research published in top-tier conferences such as CAV, CCS, ISCA, SP, and CSF. The research will focus on developing analysis frameworks to evaluate and prove security properties of protocols and programs, establishing end-to-end guarantees across the compilation chain. Candidates should have expertise in formal methods and at least one of the following areas: verification of security and cryptographic protocols, symbolic and computational security analysis, or compiler correctness and preservation of security properties. Experience with proof assistants and automated verification tools (e.g., Coq, Isabelle/HOL, Tamarin, ProVerif) and SMT solvers is highly desirable. The position offers the chance to lead independent research projects, contribute to joint initiatives, and collaborate with both internal and external partners. Applicants must hold a doctoral degree (or equivalent foreign degree) by the time of employment. A strong publication record, ability to communicate scientific results effectively, and comfort working in an international environment are essential. Preferred qualifications include a recent doctoral degree (within the last three years), awareness of diversity and equal opportunity issues, and strong personal skills. The position is full-time, for up to two years, and offers a monthly salary with attractive benefits and good working conditions at KTH. To apply, candidates should submit their application via KTH's recruitment system, including a CV, diplomas and grades (with translations if necessary), and a brief statement of research interests and goals. The application deadline is January 31, 2026. For further information, contact Assistant Professor Hamed Nemati at [email protected].

The School of Electrical Engineering and Computer Science at KTH Royal Institute of Technology invites applications for a PhD position in Computer Science, focusing on verified microarchitectural security. This opportunity is part of the µVerif project, which aims to advance rigorous security analysis of computer microarchitecture. The research addresses critical vulnerabilities in modern processors, such as those introduced by speculative and out-of-order execution, and seeks to bridge the gap between formal program analysis and real hardware security. The successful candidate will join a vibrant research environment, working closely with Associate Professor Roberto Guanciale and Assistant Professor Hamed Nemati. The project involves developing formal models of speculation and microarchitectural information flow, automatically extracting security-relevant models from RTL, and evaluating these techniques on open-source RISC-V processor cores. The long-term goal is to enable scalable, hardware-relevant verification of security properties for real-world systems. Key research areas include formal methods, program analysis, computer architecture, and computer security. The student will design and implement analysis and model-extraction tools using SMT solving and symbolic reasoning, and apply these methods to open-source processor designs. The position offers a dynamic and supportive environment, with access to excellent facilities and a strong network of researchers in system security and formal verification. Applicants must hold a second cycle degree (such as a master's) or have completed at least 240 higher education credits (with at least 60 at the second-cycle level), or possess equivalent qualifications. Proficiency in English (English B/6) is required. Candidates should demonstrate strong backgrounds in formal methods, program analysis, computer architecture, and computer security, as well as programming skills in languages such as Python, OCaml, or C/C++. Experience with SMT solvers, theorem provers, hardware description languages, symbolic execution, model checking, low-level systems programming, and microarchitectural side channels is highly valued. Personal qualities such as goal orientation, perseverance, independence, collaboration, and analytical ability are also important. The position is full-time, with a monthly salary according to KTH's doctoral student salary agreement, and includes employee benefits. The initial contract is for one year, renewable up to four years in total. The application deadline is April 2, 2026. For further information, contact Associate Professor Roberto Guanciale at [email protected]. To apply, submit your application via KTH's recruitment system, including your CV, application letter, diplomas and grades, proof of language requirements, and representative publications or technical reports. KTH is committed to equality, diversity, and providing a creative and dynamic environment for all staff and students.