Third-cycle subject: Computer Science
Our research vision is to produce software platforms that have mathematically guaranteed security properties through the use of formal modelling and verification. The past decade has seen impressive progress in this area, where projects such as seL4, CertiKoS and Prosper have demonstrated that a combination of systems compartmentalisation techniques (virtualisation, partitining, containerisation) with modern verification techniques results in very considerable gains in trustworthiness. However, verification of these platforms is complex and expensive. In fact, implementing and verifying low level and optimized code is highly nontrivial. Moreover, the security of the system depends on many hardware details that are found only after many rounds of trial and error.
Our goal is to automate as much as possible the implementation and verification of various types of high performance real-time applications, kernel functionality, and device drivers, and to demonstrate the performance, reliability and security of the developed solutions. Our project aims to improve various aspects of the design and verification of low level platforms. For this reason, the student will be able to contribute to the project in one or more research tasks according to their research interests. These include design and implementation of a new kernel, design of new security techniques, development of new methods for software synthesis, formal modeling and verification.
Supervision: The doctoral student will be placed at the KTH Royal Institute of Technology and supervised by Mads Dam.
More information & Application