HAKarlsson

Projects

S3K - Safe and Secure Separation Kernel

S3K is a separation kernel designed for high-assurance systems, providing strong isolation between partitions to ensure security and reliability. Developed with formal methods, it guarantees correctness and robustness against various types of attacks. S3K’s key differentiating features include formal verification and support for principled dynamic resource management with real-time capabilities.

This project is funded by KTH CDIS and the Intel Cooperations.

This is an ongoing research project. The formal verification component is currently under development.

Related Papers

• H. Karlsson and R. Guanciale, “Partitioning Kernel with Capability Controlled Temporal and Spatial Partitioning,” in 2025 IEEE 46th Real-Time Systems Symposium (RTSS’25), Dec. 2025.
• H. A. Karlsson, “Minimal partitioning kernel with time protection and predictability,” in Proc. IEEE European Symposium on Security and Privacy Workshops (EuroS&PW’24), IEEE, 2024, pp. 234–241.