Roberto Guanciale

I am an Associate Professor atKTH Royal Institute of Technology, in theDivision of Theoretical Computer Science at the School of Electrical Engineering and Computer Science (EECS).

I'm leading the STEP (Secure and Trustworthy Execution Platform) research group.

My research focuses onsecure and trustworthy computing systems, with an emphasis on building systems that are not only efficient, but alsoprovably correct, predictable, and secure. I work at the intersection ofoperating systems, programming languages, formal methods, and computer architecture, with a strong interest in how low-level hardware features interact with software security.

 

Opening Positions

• Doctoral student in Computer Science - Verified Microarchitectural Security

 

Research

My main research interests include:

High-assurance operating systems and separation kernels

• S3k:separation kernel with real time guarantees
• Prosper hypervisor Hypervisor for ARMv7

Formal verification of binary code

• HOLBA Formal analysis tool for binary code integrated with Interactive Theorem Prover

Timing predictability and side-channel resistance

• Scam-V Relational testig for identification of side channels on microprocessors

Software Defined Netorking

• HOL4P4 Formal analysis tool for P4 code integrated with Interactive Theorem Prover

A recurring theme in my work is bridging theory and practice: using formal methods to reason about real systems, while ensuring that the resulting designs remain practical and performant. I collaborate closely with industrial partners (e.g. in aerospace and embedded systems) as well as academic groups across Europe.

Projects & Collaboration

Current and recent projects include work on:

• Secure and predictable separation kernels
• Verified system software for embedded and real-time platforms
• Side-channel analysis and mitigation
• Formal reasoning about hardware-software interfaces

I am always happy to discuss potential collaborations, student projects, or research ideas.

 

Centers

I am involved in the following initiatives.

• CDIS
• Digital Futures
• WASP

Current PhD students and Postdocs

• PhD student: Anoud Alshnakat (P4 verification) funded by WASP

• PhD student: Henrik Karlsson (s3k separation kernel) funded by CDIS

• PhD student: Antonio Napoli (Analysys of microarchitectures) funded by WASP

• Industrual PhD student: Janos Kövér (Network side channels) funded by WASP and Ericsson

• Postdoc: Can Aknesil (LLVM side channel analysis) funded by WALP

Graduated PhD students

• 2023 Jonas Haglund (Veritication of DMA devices) funded by Digital Futures

• 2023 Andreas Lindner (HOLBA) funded by SSF

• 2024 Ning Dong (Processor verification) CSC Scholarships

• 2025 Didrik Lundberg (P4 verification) funded by SSF and Saab