SYSGO PikeOS Correctness Presentation at Embedded World
SYSGO will make a technical presentation on operating system correctness at Embedded World 2010 in Nuremberg. For composite systems, high levels of the Common Criteria standard make mandatory the formal verification of the OS layer(s) that interface the user application with the hardware platform. Correctness of this software component is one of the major challenges that embedded solution suppliers are increasingly facing. The presentation will focus on the methods and techniques used in the formal verification process applied to the PikeOS safe and secure virtualization RTOS platform.
The presentation, Ingredients of Operating System Correctness – Lessons Learned in the Formal Verification of PikeOS, will be given by Christoph Baumann, Saarbrücken University, on Tuesday March 2, 15:00 – 15:30.
Reasoning about operating system correctness has for a long time been a rather academic exercise. This is changing today with the emergence of separation kernel implementations, where partitioning analysis is already good practice. In the presentation, SYSGO will show how the CVM “concurrent virtual machines” framework developed by Saarbrücken University applies as a checklist for the correctness of PikeOS.
In particular, a simulation theorem between a top-level abstract model and the system consisting of the kernel and user programs running in alternation on the real machine will be described. Then, based on an example of a typical code trace through the kernel, correctness properties are identified for all components in the trace. These are needed for the overall correctness proof of the microkernel.
The correctness criteria under consideration comprise not only functional correctness properties, i.e. that kernel functionality adheres to its specification, but also invariants on the kernel implementation, e.g. memory separation. While the verification of such crucial security requirements is not easily achieved via traditional testing, formal methods can provide mathematical evidence that the core concepts of a kernel implementation are appropriate to guarantee secure virtualization.
The formal proof of the correctness of PikeOS is conducted using VCC, an automated C verification tool developed by Microsoft Research. This work is being performed in cooperation with the European Microsoft Innovation Center at Aachen and the universities of Koblenz and Saarbrücken, as part of the Verisoft XT BMBF funded project.
More info: SYSGO | Verisoft XT
If you are familiar with RSS feeds, you can also sign up for our free blog feed. Our RSS feed is updated in real-time while our newsletter is updated daily.
