Enhancing Fuzzing Technique for OKL4 Syscalls Testing

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 Para virtualization 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. We introduce our ongoing work for testing the security of OKL4. We have chosen to focus on the most low level OKL4 interface usable from an external actor: the system call API. Because all operating system components use directly or indirectly these system calls, a minor flaw at this level can impact in chain the entire system including a virtualized kernel. We have developed a model describing the OKL4 system calls. This model also contains all constraints applicable to a system call. Based on these models, we are working on a tool using the constraints to compute a reduced set of system call input values which are highly likely to generate flaws in OKL4 if they are not fully checked by the hypervisor.