The Provably Secure Execution Platforms for Embedded Systems (PROSPER) project aims to build the next generation framework for fully verified, secure hypervisors for embedded systems. It thus focuses on:
In this year's security seminar at SICS ("Securing infrastructures, the Smart GRID and the Things", Kista, 8th of April 2014) Oliver Schwarz will talk about formal verification within the PROSPER project.
In the context of a Crosstalks debate Mads Dam talked with KTH News about our project. Subsequently, Elektroniktidningen, IDG and others reported about PROSPER.
On February 28th Mads Dam was invited to speak at the Irisa-DGA seminar "méthodes formelles et sécurité" in Rennes, France. The 1-hour-talk with the title "Formal verification of information flow security for a simple ARM-based separation kernel" is available online.