SYSGO's PikeOS micro-kernel correctness presented at embedded world conference
Mainz - February 22, 2010 A technical presentation on Operating System correctness applying to PikeOS will be given at the upcoming embedded world 2010 event in Nuremberg, as part of the Conference Program. This presentation focuses on the methods and techniques used in the formal verification process applied to PikeOS, the Safe and Secure Virtualization RTOS platform product commercialized by SYSGO.
PikeOS is MILS compliant by design and is already used in major safety-critical projects. Its innovative architecture makes it also suitable for systems requiring the highest level of security. 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.
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 it will be shown 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.
The presentation “Ingredients of Operating System Correctness - Lessons Learned in the Formal Verification of PikeOS” will be given by Christoph Baumann, Saarbrücken University, at the upcoming embedded world 2010 event in Nuremberg, as part of the Conference Program, Session 1.4, Test and Verification II, and will occur on Tuesday March 2, 15:00 – 15:30.
About Verisoft XT
Verisoft XT is a three-year research project funded by the German Federal Ministry of Education and Research (BMBF). Project management agency is the German Aerospace Center (DLR). The main goal of the project is the pervasive formal verification of computer systems. The correct functionality of systems, as they are used, for example, in automotive engineering, in security technology and in the sector of medical technology, is to be mathematically proved. The proofs are computer aided in order to prevent human error by the scientists involved. The knowledge and progress obtained are expected to assist German enterprise in achieving a stable, internationally competitive position in the professional areas mentioned above.
The Verisoft XT project is focused on:
-The creation of methods and tools which would allow the pervasive formal verification of the design of integrated computer systems.
- An increase in industrial productivity and quality.
- The prototypical realization of four concrete, industrial application tasks.
Verisoft XT is the successor project of Verisoft. It is planned over three years and approved by the BMBF. For more information, please visit www.verisoftxt.de/StartPage.html
PikeOS is an innovative product, providing an embedded systems platform where multiple virtual machines can run simultaneously in a secure environment. The Safe and Secure Virtualization (SSV) technology allows multiple operating system APIs, called “Personalities”, to run concurrently on one machine, e.g. an ARINC-653 application together with Linux. The PikeOS microkernel architecture allows it to be used in cost sensitive, resource constrained devices as well as large, complex systems. The simplicity and compactness of the PikeOS design results in real-time performance that competes head-to-head with conventional proprietary RTOS solutions. PikeOS is certifiable to safety standards like DO-178B, IEC 61508 or EN 50128, and is also MILS compliant.
SYSGO provides operating system technology, middleware, and software services for the real-time and embedded market. A differentiating capability of SYSGO is the Safe and Secure Virtualization platform PikeOS, a paravirtualization operating system which is built upon a small, fast, and safe microkernel. It supports the co-existence of independent operating system personalities on a single platform, including ELinOS, SYSGO’s embedded Linux distribution. SYSGO supports international customers with services for embedded Linux, real-time capabilities and certification for safety-critical applications. Markets include Aerospace & Defense, Industrial Automation, Automotive, Transportation and Network Infrastructure. Customers include Airbus, Honeywell, Thales, Daimler, Raytheon, Rheinmetall, Rockwell-Collins, Siemens, and Rohde & Schwarz. SYSGO has facilities in Germany, France, The Czech Republic and North America, and offers a global distribution and support network, including Europe and the Pacific Rim.
For more information please visit www.sysgo.com.
SYSGO, ELinOS, PikeOS, CODEO, and other SYSGO products and services mentioned herein as well as their respective logos are trademarks or registered trademarks of SYSGO. All other product and service names mentioned are the trademarks of their respective companies.