Roberto Guanciale: Formal Verification of Information Flow Security for a Simple ARM-Based Separation Kernel

A separation kernel simulates a distributed environment using a single physical machine by executing partitions in isolation and appropriately controlling communication among them. We present a formal verification of information flow security for a simple separation kernel for ARMv7. We propose an approach where communication between partitions is made explicit and the information flow is analyzed in the presence of such a channel.