The HiPEAC conference is the premier European forum for experts in computer architecture, programming models, compilers and operating systems for embedded and general-purpose systems. The 10th HiPEAC conference took take place in Amsterdam, The Netherlands from the 19th to the 21st of January 2015.
During the MILS workshop, Stéphane Lescuyer from Prove & Run presented the design of ProvenCore, our formally proven, POSIX compliant microkernel compatible with the ARM and x86 architectures. ProvenCore is designed to be used as the trusted foundation of the security architecture of a device, and can be used to build a trusted operating system. This presentation is based on the following research article.