I am currently involved with the following projects.
Trustworthy COTS Hardware is examining how to improve the
trustworthiness of a verified kernel running on potentially
unreliable commercial off-the-shelf hardware.
(secure embedded L4) project's goal is to provide a reliable and
secure microkernel-based platform for future embedded
systems. Embedded systems are becoming increasingly complex -
microkernels are an approach to reliably and securing integrating
software components in embedded systems. The main challenges involve
researching a principled and systematic in-kernel resource management
approach, and developing the new microkernel in a way that is readily
amenable to formal verification.
I am also involved with
project. The project aims to formally verify both a model and the
complete implementation of the seL4 microkernel.