Press Releases

PikeOS meets the requirements of functional safety and is already used in large safety-critical projects. The system design of PikeOS also complies with the MILS standard (Multiple Level of Security) and thus simultaneously takes into account the security requirements of embedded systems. For high security levels, the Common Criteria standard demands a formal verification of the operating system layer(s) that connect the applications with the hardware in complex systems. The correctness of these software components is one of the biggest challenges that embedded system providers are increasingly facing.

For a long time, thinking about the correctness of operating systems was more of an academic exercise. This is changing nowadays with the increasing use of so-called separation kernels, where partition analysis is a common practise. The presentation shows how the framework CVM (Concurrent Virtual Machines) developed by the University of Saarbrücken can be used as a checklist for the correctness of PikeOS.

For the formal proof of the correctness of the microkernel, a simulation theorem between an abstract model and the system consisting of a kernel and user programs running alternately on a real machine is first described. Then, using a typical code trace as an example, the correctness properties for all components of the trace are identified.

The correctness criteria considered include not only properties of functional correctness, i.e. that the functionalities of the kernel conform to the specification. They also include the invariants of the kernel implementation, such as memory separation. Since verification of critical security requirements cannot be easily achieved by conventional testing methods, formal methods can provide mathematical proof that the core concepts of a kernel implementation are suitable to guarantee secure virtualisation.

The formal proof of correctness of PikeOS is conducted using VCC, an automated C verification tool developed by Microsoft Research. This work is carried out in cooperation with the European Microsoft Innovation Center in Aachen and the Universities of Koblenz and Saarbrücken and is part of the BMBF-funded Verisoft XT project.

Christoph Baumann, University of Saarbrücken, gives the presentation "Ingredients of Operating System Correctness - Lessons Learned in the Formal Verification of PikeOS" during the embedded world conference 2010 in Nuremberg. The presentation is part of the conference programme, session 1.4, Test and Verification II. It will take place on Tuesday, 2 March, 15:00 - 15:30 h.

The Verisoft XT Project

Verisoft XT is a three-year research project funded by the German Federal Ministry of Education and Research (BMBF). The project executing agency is the German Aerospace Center (DLR). The ambitious project goal is the consistent, formal verification of computer systems: The correct functioning of systems, such as those used in automotive engineering, security technology and the medical technology sector, is to be mathematically proven. The proofs are computer-aided in order to exclude human error on the part of the scientists involved as far as possible. The knowledge gained and the progress made should help German companies in these sectors to create lasting international competitive advantages.

The guiding vision of the Verisoft XT project is:

• to create the methods and tools that allow the design of integrated computer systems to be formally verified throughout,
• thereby generating a productivity and quality boost for industry, and
• to realise this prototypically in four concrete, industrial application scenarios.

Verisoft XT is the successor project to Verisoft. It is scheduled to run for three years and has been approved by the BMBF. Further information is available at www.verisoft.de

About PikeOS

PikeOS is a virtualisation platform and operating system for embedded systems that enables multiple virtual machines to run simultaneously in a secure environment. The SSV (Safe and Secure Virtualization) technology offers multiple operating system interfaces, so-called "personalities", which can run simultaneously on one hardware, e.g. a safety-critical ARINC 653 application together with Linux. Due to its microkernel architecture, PikeOS can be used in price-sensitive devices with limited resources as well as in large, complex systems. The compactness and clarity of PikeOS's system design provides real-time performance equivalent to conventional real-time operating systems. PikeOS is MILS compliant and certifiable to safety standards such as DO-178B, IEC 61508 or EN 50128.

More information at www.sysgo.com/pikeos