Proving Memory Separation in a Microkernel by Code Level Verification
Often, an integrated mixed-criticality system is built in an environment which provides separation functionality for available on-board resources. In this paper we treat such an environment: the PikeOS separation kernel—a commercial real-time embedded operating system. PikeOS allows applications with different safety and security levels to run on the same hardware. Obviously, a mixed-criticality system built on PikeOS relies on the correct implementation of the separation mechanisms. In the context of the Verisoft XT and TECOM projects we apply deductive formal software verification to the PikeOS separation mechanisms in order to validate this security requirement.