Roberto Guanciale

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

My research focuses on secure and trustworthy computing systems, with an emphasis on building systems that are not only efficient, but also provably correct, predictable, and secure. I work at the intersection of operating systems, programming languages, formal methods, and computer architecture, with a strong interest in how low-level hardware features interact with software 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.