 | Researching and applying formal software verification
Verisoft (XT) is a long-term research project funded by the German Federal Ministry of Education and Research (BMBF). The main goal of the project is the pervasive formal verification of computer systems: To use mathematical methods to prove the correct functionality of complex systems, as they are used, for example, in automotive engineering, security technology, or the sector of medical technology. The verification process is computer aided to manage the size and complexity of the tasks and to prevent human error by the verification engineers. The knowledge and progress obtained from the Verisoft project are expected to assist German enterprise in achieving a stable, internationally competitive position in the area of formal software verification. |
Verisoft (XT) has two major areas of work: The creation of methods and tools which allow the pervasive formal verification of the design of integrated computer systems; thus leading to an increase in industrial productivity and quality. The prototypical realization of four concrete application tasks, three of which are contributed from industrial partners. Verisoft and its successor project Verisoft XT range over seven years and approved by the BMBF (periods of validity: 01.07.2003–30.06.2007 and 01.07.2007–30.06.2010). See www.verisoftxt.de
The contribution of the European Microsoft Innovation Center (EMIC):The Verisoft XT project is unique in its application of formal software verification to real, industrial scale systems. One of these systems is the Microsoft Hyper-V virtualization product that is shipped as a component of Windows Server 2008.
In close collaboration with the University of Saarbrücken and Microsoft Research Redmond, EMIC develops verification methodology and tools with the aim of verifying the Microsoft Hyper-V hypervisor kernel, which is, in essence, a small multi-processor operating system micro kernel with memory and thread management but without device drivers. The implementation of this kernel consists of roughly 60 thousand lines of highly optimized C and x64 assembler code.
Such low-level system code has long been recognized as a fruitful target for formal software verification, and several research projects have verified small operating systems. However, such projects left open two gaps to a practical methodology for verifying real systems.
The first gap had been in the verification targets. Existing verifications target sequential code (or locking disciplines that allow sequential reasoning about code) written in clean programming languages. In contrast, modern system code is typically multithreaded, racy, written in C and assembler (leveraging features such as address arithmetic and unions), compiled with aggressive optimizing compilers, and run on modern processors with architecturally visible caches and incoherent memory. All of these factors contribute to a semantic gap between the naive and actual semantics of the code being verified.
The second gap had been in the methodology. Existing methodologies for system code verification depend on embedding the code, operational semantics, and hardware semantics within interactive theorem provers, with the verification driven by an expert user of the prover. However, we are trying to shape a methodology in which proofs might someday be maintained by developers (at least through routine code changes), which typically requires operationally meaningful annotations added directly to the code.
The goal of EMIC’s effort is to bridge these gaps in a verification methodology being developed to verify the Microsoft Hypervisor. | |
