Hamburg, Germany, September 15, 2009
SYSGO, leading supplier of software solutions for the world’s most demanding safety and security applications, presents early results of an innovative formal verification technique that applies to its Safe and Secure Virtualization product PikeOS. A research paper describing this process is presented at SAFECOMP 2009, the 28th International Conference on Computer Safety, Reliability and Security, held in Hamburg Germany on September 15th to 18th.
As part of the Verisoft XT project, funded by BMBF (German Ministry of Education and Research), SYSGO initiated the formal verification of its Safe and Secure Virtualization product PikeOS, taking aim at the highest level of security corresponding to today’s Common Criteria EAL 7. In cooperation with the European Microsoft Innovation Center at Aachen and the universities of Koblenz and Saarbrücken, the new innovative technique uses Microsoft’s VCC tool recently released to the public. This technology includes a verifying C compiler used to annotate PikeOS and assembly code with assertions that always hold and that can be proved correct by VCC. The verification extends to both C and assembly code.
Practically, verification relies on (1) adding (computer-readable) logical descriptions of what the code does by a (human) verification engineer and then (2) using a computer-based generation of logical formulas from the code and automatically check that (1) and (2) match (technical specifics: calculus based on Dijkstra’s weakest precondition and a Satisfiability Modulo Theories (SMT) solver, an approach that tightly integrates Boolean reasoning with theory-specific solvers that handle conjunctions of predicates from a given theory). As deductively it can be shown that the code is correct, so this approach is also called deductive code verification. As another part of the Verisoft XT project, the European Microsoft Innovation Center is also using this approach as part of their work on their Hyper-V verification project (see more at vcc.codeplex.com).
For PikeOS, the code verification task fits into a larger separation kernel certification context, to include IEC61508 and/or Common Criteria. This enhanced VCC code verification approach provides:
– memory framing properties, that is, absence of illegitimate memory accesses on some sections of code and
– functional correctness, that is, implementation honoring the formal specification on some parts of the kernel.
“We are very pleased with the progress occurring in this important project”, said Rudolf Fuchsen, Head of Engineering at SYSGO. “When we designed PikeOS, we had in mind not only compliance to the highest level of safety, but also to the highest level of security. We have achieved DO-178B certification in avionics and we are working on corresponding IEC 61508 and EN50128 certifications in the industrial and transportation areas. We knew from the start that in addition to being MILS compliant, the same concepts of modularity, compactness, and traceability would fit with the stringent requirements of the highest level of security as stated in EAL 5, 6 or even 7”.
Within the Verisoft XT project, a model of the PowerPC architecture and assembly language has been generated, with treatment of both entire assembly files and the relatively frequent inline assembly. Milestones that have been reached include the verification of the functional correctness of helper functions (operating on bitmaps, lists, as well as hardware primitives such as the enable/disable interrupt bit) and the verification of first system calls.
For the duration of the project, which runs through mid 2010, the research team is continuing to work on the system calls aiming at complete verification of that layer. Moreover, in an informal adjunct called “PikeOS commentary” it is examined how to insert the formal work into dependability frameworks such as the Common Criteria, ISO/EIC 61508 or DO-178B. Within the Verisoft XT project, SYSGO is partnering with the European Microsoft Innovation Center and the universities of Koblenz and Saarbrücken who are applying the same approach to the hypervisor Hyper-V shipped with Windows 2008.
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
About SafeComp
The SAFECOMP Conference series was established in 1979 by the European Workshop on Industrial Computer Systems, Technical Committee on Reliability, Safety and Security (EWICS TC7). Since then, SAFECOMP regularly contributes to the progress of the state of the art in dependable applications of computer systems. SAFECOMP focuses on state-of-the-art and innovative approaches to risk assessment and management from the safety, security and reliability viewpoints. The scope includes IT systems and infrastructures considered critical within their present or emerging contexts. All aspects of dependability and survivability of critical computer-based systems and infrastructures are included. In particular, SAFECOMP emphasizes multidisciplinary approaches to deal with the nature of complex critical IT systems and applications.
For more information, please visit users.informatik.haw-hamburg.de/~safecomp2009/public/scope.html
About SYSGO
SYSGO excels in providing operating system technology, middleware, and software services for the real-time and embedded device market. A differentiating capability of SYSGO is the secure PikeOS paravirtualization operating system which is built upon a small, fast, and safe microkernel and supports the cohabitation of independent operating system personalities on a single platform, including ELinOS, SYSGO’s embedded Linux development environment. SYSGO supports international customers with services for embedded Linux, real-time capabilities and certification for safety-critical applications. Target markets include Aerospace & Defense, Industrial Automation, Automotive, Transportation and Network Infrastructure. SYSGO customers include Airbus, Honeywell, Thales, Daimler, Raytheon, Rheinmetall, Rockwell-Collins, Siemens and Rohde & Schwarz. Today, the company has six facilities in Europe, including Germany, France and The Czech Republic and offers a global distribution and support network, extending to North America and the Pacific Rim. For more information, please visit www.sysgo.com