Power Optimisation for a Verifiably Secure Separation Kernel

For embedded devices more than any other, nonfunctional software properties such as timeliness, safety, and power consumption play a pivotal role. However, these devices are running increasingly complex software stacks including virtualization in order to be usable in mixed-criticality or mixed-certifiability scenarios. We demonstrate how a fully static hypervisor can be retrofitted with a power management module which enables it to react to fluctuations in VM execution load. Our results show a significant reduction in energy consumption, while we maintain the static properties of the codebase which are required for the hypervisor’s formal proof system.