A research group at the School of Electrical Engineering and Computer Science, KTH Royal Institute of Technology, Stockholm · led by Hamed Nemati
We work on the gap between what a program is proved to do and what the hardware running it actually does. That means microarchitectural attacks and defenses, machine-checked proofs about binaries, leakage contracts that compilers can be held to, and verification of the cryptographic protocols underneath real systems.
Microarchitectural security
Speculative execution and side-channel attacks, what the hardware really leaks, and defenses that can be stated precisely rather than hoped for.
Formal verification of low-level code
Machine-checked proofs about binaries and systems software, so guarantees survive all the way down to the instructions that execute.
Secure compilation
Whether the compiler preserves the security property you wrote the source to have — constant-time code that survives optimization.
Protocol verification
Symbolic analysis of cryptographic protocols as they are actually implemented and compiled, not only as they are specified.
People
The group brings together formal methods, computer architecture and systems security — most projects sit between at least two of them.
Loading people…
News
Papers, talks, awards and openings in the group.
Loading news…
Projects & Tools
Everything we build is open source. These are the tools the group maintains and the artefacts behind our papers.
Loading projects…
Publications
Selected work from the group, newest first.
Loading publications…
Join us
We are looking for people who like hard, low-level problems
We regularly have openings for PhD students, postdocs and research engineers. A good fit usually has a background in at least one of formal verification, microarchitectural security, program analysis or compiler design — and the patience to learn the others here.
Even when nothing is advertised, get in touch if the work above is what you want to spend a few years on. Master's students at KTH looking for a thesis project are welcome too.