Archive notice: This article was originally published on July 9, 2007. Links and embedded videos are preserved as part of the historical record.
Reliably functioning and secure software is not only a competitive advantage for companies, however, but also a prerequisite for safe applications in cars, medicine or safety technology, for example.
The Federal Ministry of Education and Research is therefore funding the VERISOFT XT research project with around 12 million euros over the next three years. The aim is to develop a “Verified in Germany” quality seal. For this, methods and tools for the formal verification of the design of integrated computer systems are to be created. This means providing mathematical and machine-checked proof that the computer systems under consideration contain zero errors in the design. While the mathematical foundations for this were developed in the predecessor project, VERISOFT XT is concerned with exemplary industrial applications. Here, programs with tens of thousands of lines of code must be verified.
In the project consortium, ten partners from industry, – small and large companies -, as well as seven universities are working together under the consortium leadership of the German Research Center for Artificial Intelligence (DFKI). The project is being carried out within the framework of the BMBF program ICT 2020 – Research for Innovations.
One application example comes from the automotive sector. A vehicle today contains an average of 50 control units (ABS, EPS etc.), each consisting of around 300 electronic components. If the failure rate of each of these 15,000 components due to production, design or operating errors is one in a million, then this seemingly low risk accumulates to a failure rate of 1.5% for the entire electronics. With the proportion of electronics in vehicles expected to double and mechanical fallback levels being eliminated, this problem is exacerbated accordingly. In VERISOFT XT, the function and real-time behavior of a complete microcontroller system in a control unit that implements a safety-critical function in the chassis of an upper-class vehicle is therefore to be formally verified.
The operating convenience and wealth of functionality of modern operating systems simultaneously lead to security gaps and attack points that hackers use to obtain confidential data illegally. Smaller operating systems do exist that remain more manageable and therefore more trustworthy due to their size. However, these do not offer the convenience that one would expect from one’s home banking software, for example. The hypervisor represents a solution to this dilemma. Put simply, it is an operating system for operating systems and ensures that there is no unauthorized memory-access between individual operating systems. With VERISOFT XT, a concrete example is intended to show that even malicious users have no chance of outwitting the verified hypervisor.
