Welcome to the Secure and Trustworthy Execution Platforms (STEP) group at KTH!

You can access thesis and publications in the dedicated Publications page.



Congratulations to Pablo Buiras and his co-authors who received the Most Influencial Paper of ICFP’12 award for the paper Addressing Covert Termination and Timing Channels in Concurrenct Information Flow Systems. The work was done while Pablo was at Chalmers.


Anoud Alshnakat and Didrik Lundberg presented their poster on the formalization of the P4 programming language.


The formalization of the Machine-Independent Language (MIL), that captures microarchitectural features, have been released.


The papers “Formally Verified Isolation of DMA,” by Jonas Haglund and Roberto Guanciale, and the paper “Foundations and Tools in HOL4 for Analysis of Microarchitectural Out-of-Order Execution,” by Karl Palmskog, Xiaomo Yao, Ning Dong, Roberto Guanciale, and Mads Dam, were accepted to FMCAD 22!


Ning Dong did his 50% seminar on verified pipelined processors and microarchitectural modelling and verification.


STEP Retreat in Sigtuna.


At SWITS, Anoud Alshnakat presented a formalization of P4, and Henrik Karlsson presented a poster on the design of a separation kernel.


At the CDIS Spring Conference, Roberto Guanciale gave a talk, and Henrik Karlsson presented a poster about the separation kernel project.


Anoud Alshnakat did her 50% seminar on the formalization of P4.


HOL4 formalization of MIL publicly released.