University of Limerick
Virtual machine monitor is a hot topic in the embedded community. Apart from high end system, current processors for embedded systems do not have any instructions helping to virtualize an operating system. Based on this fact, most of the current hypervisors for embedded devices use the paravirtualization technique. This is the case of the OKL4 kernel which is based on the L4 micro-kernel and implements among other the Linux kernel as guest OS. The authors introduce their ongoing work for testing the security of OKL4.