The VERISOFT XT Project
Verisoft XT was a three-year research project funded by the German Federal Ministry of Education and Research (BMBF). Project management agency was the German Aerospace Center (DLR). The main goal of the project was 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, had to be mathematically proved. The proofs were computer aided in order to prevent human error by the scientists involved.
As part of this project, SYSGO initiated the formal verification of its Safe and Secure Virtualization product PikeOS, taking aim at the highest level of security. In cooperation with the European Microsoft Innovation Center at Aachen and the universities of Koblenz and Saarbrücken and the Karlsruhe Institute
of Technology, the new innovative technique has used 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.
The following major project results have been obtained with SYSGO involvement:
- Verification of the kernel interface (system call) by a VCC (Verifying C Compiler, Microsoft Research): the necessary part of the PowerPC hardware has been simulated in VCC, so that by using a minimal kernel model, a complete system call (kernel entry) has been verified. [BBBB09b]
- Verification of the memory separation property: VCC has been used to verify the correctness of the PikeOS partition-local memory managers as most low-level resource management system. [BBBT11]
Moreover, SYSGO has participated in European meetings of the RTCA to work on the "Formal Methods Supplement" that is part of DO-178C from spring 2009 until it was stable (voted through plenary) in 2010.
For more information, please go to: www.verisoftxt.de
[BBBB09b] Christoph Baumann, Bernhard Beckert, Holger Blasum, and Thorsten Bormer. Formal verification of a microkernel used in dependable software syst ems. In Bettina Buth, Gerd Rabe, and Till Seyfarth, editors, Computer Safety, Reliability and Security - 28th International Conference SAFECOMP 2009, volume 5775 of Lecture Notes in Computer Science, pages 187-200. Springer, 2009.
[BBBT11] Christoph Baumann, Thorsten Bormer, Holger Blasum, and Sergey Tverdyshev. Proving memory separation in a microkernel by code level verification. In Object/Component/Service-Oriented Real-Time Distributed Computing Workshops (ISORCW), 2011 14th IEEE International Symposium on, pages 25-32. IEEE, 2011